Accepted Papers

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

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

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

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

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

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

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

Ofer Strichman, Daniel Kroening
A Framework for Decision Procedures in Program Verification

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

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