SMT 2011

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

Invited Speakers

Software Construction using Executable Constraints
Viktor Kuncak (EPFL)
Constructing software that satisfies the desired properties can greatly benefit from solvers based on satisfiability modulo theories (SMT) paradigm. We propose a research program in which software construction and SMT technology become even more interconnected than today. Instead of checking properties of low-level legacy programs, new generations of SMT solvers could focus on constructing programs and values within compilers and run-time systems of declarative programming languages designed with constraint solving in mind. This agenda has implications on both theories and interfaces of future SMT solvers.

The theories of interest come in part from functional programming languages and from data structure libraries. They include algebraic data types (term algebras), arrays, maps, sets, and multisets, extended with recursively defined functions. New interfaces for SMT solvers are driven by their extended role: in addition to yes/no satisfiability answers, we need synthesis of values and programs. To answer declarative queries at run-time, we need efficient generation and fair enumeration of models, as well as their mapping to programming language values. To support the compilation of implicit specifications, we need SMT solvers that can solve parameterized problems and perform constraint simplification. Ultimately, SMT solvers can become virtual machines for constraint programming, working with data structures directly manipulated by programs, and performing selective specialization of frequently invoked constraint solving paths. This is joint work with: Barbara Jobstmann, Ali Sinan Koeksal, Ruzica Piskac, and Philippe Suter. More information at http://lara.epfl.ch/w/impro and http://richmodels.org.

When Biology Meets (Symbolic) Computing: Algebra, Biology, Computability and Diophantus
Bud Mishra (NYU)
In this talk, I will introduce a new approach to compositional and hierarchical modeling of biological systems and its relations to certain problems in algebra and algorithmics: namely, decision procedures for systems of linear diophantine equations and inequalities, whose coefficients range over algebraic numbers and intervals. The questions, addressed here, are central to the success of the emerging field of systems biology and relate to questions in decidability theory, algorithmic algebra, hybrid automata models, etc.

Fonts via Kernest | Contact the Webmaster