| Time | Title | Place |
|---|
| 9:00-10:00 |
Session 5: Invited Talk |
Maria Paola Bonacina |
| 9:00-10:00 |
Logical Interpretation: Static Program Analysis using Theorem Proving |
Ashish Tiwari |
| 10:00-10:30 |
Coffee Break |
|
| 10:30-12:30 |
Session 6: Satisfiability Modulo Theories |
Albert Oliveras |
| 10:30-11:00 |
Solving Quantified Verification Conditions using Satisfiability Modulo Theories |
Yeting Ge, Clark Barrett, Cesare Tinelli |
| 11:00-11:30 |
Efficient Incremental E-matching for SMT Solvers |
Leonardo de Moura, Nikolaj Bjorner |
| 11:30-12:00 |
T-decision by decomposition |
Maria Paola Bonacina, Mnacho Echenim |
| 12:00-12:30 |
Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic |
Viktor Kuncak, Martin Rinard |
| 12:30-14:00 |
Lunch Break |
|
| 14:00-15:30 |
Session 7: Induction, Rewriting, and Polymorphism |
John Harrison |
| 14:00-14:30 |
Improvements in Formula Generalization |
Markus Aderhold |
| 14:30-15:00 |
On the Normalization and Unique Normalization properties of Term Rewrite Systems |
Guillem Godoy, Sophie Tison |
| 15:00-15:30 |
Handling Polymorphism in Automated Deduction |
Stephane Lescuyer, Jean-Francois Couchot |
| 15:30-16:00 |
Coffee Break |
|
| 16:00-18:00 |
Session 8: First-Order Logic |
Andrei Voronkov |
| 16:00-16:30 |
Automated Reasoning in Kleene Algebra |
Peter Hoefner, Georg Struth |
| 16:30-17:00 |
Labelled Clauses |
Tal Lev-Ami, Christoph Weidenbach, Mooly Sagiv, Thomas Reps |
| 17:00-17:30 |
Automatic Decidability and Combinability Revisited |
Christopher Lynch, Duc-Khanh Tran |
| 17:30-18:00 |
CASC Results |
Geoff Sutcliffe |