Invited Talk

Koen Claessen
Exploiting the Dual View verification (Slides)

Chao Wang, Aarti Gupta, and Malay Ganai
Predicate Learning and Selective Theory Deduction for Solving Difference Logic (Slides)

Behzad Akbarpour, Lawrence Paulson
Towards Automatic Proofs of Inequalities Involving Elementary Functions (Slides)

Swen Jacobs, Viorica Sofronie-Stokkermans
Applications of hierarchical reasoning in the verification of complex systems (Slides)

Sava Krstic, Robert Jones, and John O'Leary
Mothers of Pipelines (Slides)

Geoffrey Brown, Lee Pike
Easy Parameterized Verificaton of Biphase Mark and 8N1 Protocols (Slides)

Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, and Daniele Zucchelli
Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies (Slides)

Clark Barrett, Igor Shikanian, and Cesare Tinelli
An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types (Slides)

Ofer Strichman, Daniel Kroening
A Framework for Eager Encoding (Slides)

Maria Paola Bonacina, Mnacho Echenim
Rewrite-Based Satisfiability Procedures for Recursive Data Structures (Slides)

Silvio Ranise, Christophe Ringeissen, and Duc-Khanh Tran
Producing Conflict Sets for Combinations of Theories (Slides)