Monday, 29 Aug 2016

08:45am - 09:10am

Registration

09:10am - 09:15am

Opening Remarks

09:15am - 10:00am

An empirical understanding of conflict-driven clause-learning SAT solvers (PDF)
Vijay Ganesh, University of Waterloo, Canada

10:00am - 10:45am

QBF solving and certification
Roland Jiang, National Taiwan University, Taiwan

10:45am - 11:15am

--- Group Photo & Coffee Break ---

11:15am - 12:15pm

Tutorial: Interpolation algorithms and their applications in model checking I (PDF)
Georg Weissenbacher, Technische Universität Wien, Austria

12:15pm - 02:00pm

--- Lunch Break ---

02:00pm - 03:00pm

Tutorial: Interpolation algorithms and their applications in model checking II (PDF)
Georg Weissenbacher, Technische Universität Wien, Austria

03:00pm - 03:30pm

--- Coffee Break ---

03:30pm - 04:30pm

Tutorial: Programming constraint services with Z3 I
Nikolaj Bjorner, Microsoft Research, USA

04:30pm - 05:00pm

Interpolants from SAT solving certificates (PDF)
Adrian Rebola Pardo, Technische Universität Wien, Austria

05:00pm - 05:30pm

Rational and irrational interpolants for polytopes
Dmitry Chistikov, University of Oxford, UK

Tuesday, 30 Aug 2016

09:00am - 09:15am

Registration

09:15am - 10:15am

Tutorial: Programming constraint services with Z3 II
Nikolaj Bjorner, Microsoft Research, USA

10:15am - 10:45am

Nested antichains for WS1S (PDF)
Ondrej Lengal, Brno University of Technology, Czech Republic

10:45am - 11:15am

--- Coffee Break ---

11:15am - 12:15pm

Tutorial: Symbolic Automata and Monadic second-order logic on finite sequences I
Margus Veanes, Microsoft Research, USA

12:15pm - 02:00pm

--- Lunch Break ---

02:00pm - 03:00pm

Tutorial: Symbolic Automata and Monadic second-order logic on finite sequences II
Margus Veanes, Microsoft Research, USA

03:00pm - 03:45pm

Bounded rigid E-unification
Philipp Ruemmer, Uppsala University, Sweden

03:45pm - 04:15pm

--- Coffee Break ---

04:15pm - 05:00pm

The interplay between word equations with rational constraints and graph querying with path comparisons
Pablo Barcelo, Universidad de Chile, Chile

05:00pm - 05:30pm

String solving with word equations and transducers: towards a logic for analysing mutation XSS
Anthony Widjaja Lin, Yale-NUS College and National University of Singapore

06:30pm - 07:30pm

YALE-NUS Presidential Seminar: Humans, Machines, and Work: The Future is Now
Speaker: Moshe Y. Vardi, Rice University, USA

Venue: Performance Hall, Yale-NUS College, 18 College Avenue West 138528

Wednesday, 31 Aug 2016

09:00am - 09:15am

Registration

09:15am - 10:15am

Tutorial: Constrained validity and querying uncertain data: exact and approximate solutions I (PDF)
Leonid Libkin, University of Edinburgh, UK

10:15am - 10:45am

--- Coffee Break ---

10:45am - 11:45am

Tutorial: Constrained validity and querying uncertain data: exact and approximate solutions II (PDF)
Leonid Libkin, University of Edinburgh, UK

11:45am - 12:30pm

String constraints for verification (PDF)
Lukas Holik, Brno Unversity of Technology, Czech Republic

12:30pm - 02:00pm

--- Lunch Reception at IMS ---

Excursion (Volunteer and self-paid)

Thursday, 1 Sep 2016

09:00am - 09:15am

Registration

09:15am - 10:00am

The commutativity problem of MapReduce programs
Yu-Fang Chen, Academia Sinica, Taiwan

10:00am - 10:45am

Verification problems in SPARK programs (PDF)
Bow-Yaw Wang, Academia Sinica, Taiwan

10:45am - 11:15am

--- Coffee Break ---

11:15am - 12:00nn

Refinement types and higher-order constrained horn clauses
Steven Ramsay, University of Oxford, UK

12:00nn - 12:30pm

Automated verification of safety hyperproperties
Marcelo Sousa, University of Oxford, UK

12:30pm - 02:00pm

--- Lunch Break ---

02:00pm - 02:45pm

Byte-precise verification of low-level list manipulation (PDF)
Tomas Vojnar, Brno University of Technology, Czech Republic

02:45pm - 03:15pm

Satisfiability modulo heap-based programs (PDF)
Quang Loc Le, Singapore University of Technology and Design

03:15pm - 03:45pm

--- Coffee Break ---

03:45pm - 04:30pm

Intruder deduction in sequent calculus
Alwen Tiu, Nanyang Technological University

04:30pm - 05:15pm

Formalisation and static analysis of CSS3 selectors
Matthew Hague, Royal Holloway, University of London, UK

05:15pm - 05:20pm

Closing Remarks

06:30pm - 07:30pm

Public Lecture: The Automated-Reasoning Revolution: From Theory to Practice and Back

Speaker: Moshe Y. Vardi, Rice University, USA

Venue: Lecture Theatre 31, National University of Singapore
           Block S16, Level 3, 6 Science Drive 2, Singapore 117546