Program

All sessions will take place in Metropolitan B unless otherwise indicated.

Monday, August 21st

Monday's program is also available with abstracts or side by side with other meetings.

09:30‑10:30  Session 1

09:30

Peter O'Hearn (Queen Mary, University of London) Proof Procedures for Separated Heap Abstractions

10:30‑11:00  Break

11:00‑12:30  Session 2

11:00	Sava Krstic , Robert Jones and John O'Leary Mothers of Pipelines
11:30	Swen Jacobs and Viorica Sofronie-Stokkermans Applications of hierarchical reasoning in the verification of complex systems
12:00	Ofer Strichman and Daniel Kroening A Framework for Decision Procedures in Program Verification
12:15	Geoffrey Brown and Lee Pike Easy Parameterized Verificaton of Biphase Mark and 8N1 Protocols

12:30‑14:00  Lunch break

14:00‑15:30  Session 3

14:00	Koen Claessen (Chalmers University of Technology and Jasper Design Automation) The Power of Finite Model Finding [ppt]
15:00	Chao Wang , Aarti Gupta and Malay Ganai Predicate Learning and Selective Theory Deduction for Solving Difference Logic
15:15	Silvio Ghilardi , Enrica Nicolini, Silvio Ranise and Daniele Zucchelli Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies

15:30‑16:00  Break

16:00‑17:45  Session 4

16:00	Behzad Akbarpour and Lawrence Paulson Towards Automatic Proofs of Inequalities Involving Elementary Functions
16:30	Maria Paola Bonacina and Mnacho Echenim Rewrite-Based Satisfiability Procedures for Recursive Data Structures
17:00	Clark Barrett , Igor Shikanian and Cesare Tinelli An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types
17:30	Silvio Ranise , Christophe Ringeissen and Duc-Khanh Tran Producing Conflict Sets for Combinations of Theories

17:45‑18:30  Discussion

17:45

Discussion