Program

• [8:45-9:00am] Introduction and Welcome
• [9:00am-10:00am] Session I
  • Invited Talk: Natarajan Shankar (SRI). Modularity in Inference Systems
• [10:00am-10:30am] Coffee Break
• [10:30am-11:45pm] Session II
  • [10:30am-10:55am] Shuvendu Lahiri and Madanlal Musuvathi. An Efficient Nelson-Oppen Decision Procedure for Difference Constraints over Rationals
  • [10:55am-11:20am] Amir Pnueli, Ofer Strichman. Reduced Functional Consistency of Uninterpreted Functions
  • [11:20am-11:45am] Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Anders Franzen, Ziyad Hanna, Zurab Khasidashvili, Amit Palti, Roberto Sebastiani. Encoding RTL Constructs for MATHSAT: a Preliminary Report
• [11:45am-12:30am] Session III
  • Invited Presentation: Clark Barrett, Leonardo de Moura, Aaron Stump. Report on the 1st Satisfiability Modulo Theory Competition (SMT-COMP)
• [12:30am-2:00pm] Lunch Break
• [2:00pm-2:45pm] Session IV
  • Invited Talk: Eli Singerman (Intel). Challenges in making decision procedures applicable to industry
• [2:45pm-3:35pm] Session V
  • [2:45pm-3:10pm] Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz. Big proof engines as little proof engines: new results on rewrite-based satisfiability procedures (Extended abstract). New: The set of problems used for the experiments (both in CVC and TPTP syntax) is available here.
  • [3:10pm-3:35pm] Ian Wehrman and Aaron Stump. Mining Propositional Simplification Proofs for Small Validating Clauses
• [3:35pm-4:00pm] Coffee Break
• [4:00pm-5:45pm] Session VI
  • [4:00pm-4:25pm] Peter Koppensteiner, Helmut Veith. A Novel SAT Procedure for Linear Real Arithmetic
  • [4:25pm-4:50pm] Sean McLaughlin, Clark Barrett, Yeting Ge. Cooperating Theorem Provers: A Case Study Combining CVC Lite and HOL-Light
  • [4:50pm-5:15pm] Tjark Weber. Using a SAT Solver as a Fast Decision Procedure for Propositional Logic in an LCF-style Theorem Prover
  • [5:15pm-5:40pm] Jim Grundy, Tom Melham, Sava Krstic, Sean McLaughlin. Tool Building Requirements for an API to First-Order Solvers
• [5:40pm-6:00pm] Business Meeting