SMT 2011

9th International Workshop on Satisfiability Modulo Theories (SMT) 2011
Co-located with Computer-Aided Verification (CAV) 2011
July 14-15
Snowbird, Utah


July 14
8:45am-8:55am (Welcome)
Shuvendu Lahiri and Sanjit Seshia.
9am-10am (Invited Talk) Chair: Shuvendu Lahiri
Viktor Kuncak. Software Construction using Executable Constraints.
10:30am-12pm (Interpolants) Chair: Bruno Dutertre
Maria Paola Bonacina and Moa Johansson. Towards interpolation in an SMT solver with integrated superposition.
Amit Goel, Sava Krstic, Rupak Majumdar and Sai Deep Tetali. Quantified Interpolation for SMT.
Andrew Reynolds, Cesare Tinelli and Liana Hadarean. Certified Interpolant Generation for EUF.
Lunch Break
2pm-3pm (Decision Procedures I) Chair: Clark Barrett
David Deharbe, Pascal Fontaine, Stephan Merz and Bruno Woltzenlogel Paleo. Exploiting symmetry in SMT problems (presentation only).
Ruzica Piskac and Thomas Wies. Decision Procedures for Automating Termination Proofs (presentation only).
3:30pm-5pm (Decision Procedures II) Chair: Maria Bonacina
Thomas Wies, Marco Muniz and Viktor Kuncak. An Efficient Decision Procedure for Imperative Tree Data Structures (presentation only).
Dejan Jovanovic and Leonardo De Moura. Cutting to the Chase: Solving Linear Integer Arithmetic (presentation only).
Duckki Oe and Aaron Stump. Extended Abstract: Combining a Logical Framework with an RUP Checker for SMT Proofs.
5pm-6pm (SMT Business Meeting)

July 15
9am-10am (Invited Talk) Chair: Shuvendu Lahiri
Bud Mishra. When Biology Meets (Symbolic) Computing: Algebra, Biology, Computability and Diophantus (Slides).
10:30am-12pm (Model Checking and Synthesis) Chair: Vijay Ganesh
Hyondeuk Kim, Fabio Somenzi and Hoonsang Jin. Selective SMT Encoding for Hardware Model Checking.
Timothy King and Clark Barrett. Exploring and Categorizing Error Spaces using BMC and SMT.
Steve Haynal and Heidi Haynal. Generating and Searching Families of FFT Algorithms (presentation only).
Lunch Break
2pm-3pm (SMT for Software) Chair: Ofer Strichman
Arie Gurfinkel, Sagar Chaki and Samir Sapra. Efficient Predicate Abstraction of Program Summaries (presentation only).
Mahmoud Said, Chao Wang, Zijiang Yang and Karem Sakallah. Generating Data Race Witnesses by an SMT-based Analysis (presentation only).
3:30pm-4pm (SMT for Software) Chair: Ofer Strichman
Stephan Falke, Florian Merz and Carsten Sinz. A Theory of C-Style Memory Allocation.
4pm-6pm (SMTLIB initiative and SMTCOMP)
Clark Barrett and Morgan Deters.

Fonts via Kernest | Contact the Webmaster