| SSPV'06 | Satisfiability Solvers and Program Verification Seattle, August 10 - 11, 2006 |
Overview
Formal verification uses mathematical techniques to guarantee the correctness of a software program (or hardware design) for the specified behavior. Formal-verification tools have enjoyed a substantial and growing use over the last few years, showing ability to discover very subtle flaws. The impact of such tools has encouraged computer scientists to search deeper into mathematical logic for techniques that will work for larger and more complex software. At the same time, researchers have been trying to come up with a theoretical understanding for the success of certain algorithms that have been particularly effective in practice.
To extend the applicability of formal verification, it is crucial to recognize that numerous problems in verification are specific instances of constraint satisfaction, a canonical form of which is the satisfiability problem of propositional logic. Indeed, satisfiability is also a dramatic example of the symbiotic relationship between theory and practice in this field. Throughout the 1990s, applied researchers made dramatic improvements in the performance and scalability of satisfiability solvers, enabling the use of satisfiability as a viable alternative in increasingly non-trivial contexts. This, in turn, motivated renewed theoretical interest in propositional satisfiability and a plethora of new results. Satisfiability-based program verification has emerged as a rapidly advancing area.
Program
Invited Talks
-
Thursday, August 10th, 09:45‑10:30
Ed Clarke (Carnegie Mellon University)
Bounded and Unbounded Model Checking using SAT [ppt] -
Thursday, August 10th, 11:00‑11:45
Ken McMillan (Cadence Labs)
SAT, interpolants, and software model checking [ppt] -
Thursday, August 10th, 11:45‑12:30
Shuvendu Lahiri (Microsoft Research)
Efficient SAT-based Techniques for Predicate Abstraction [ppt] -
Thursday, August 10th, 14:00‑14:45
Carla Gomes (Cornell University)
Beyond Satisfiability: Model Counting, Quantification, and Randomization [ppt] -
Thursday, August 10th, 14:45‑15:30
Daniel Kroening (ETH Zurich)
SAT-based methods for proving properties in Reynolds/O'Hearn Separation Logic [ppt] -
Thursday, August 10th, 16:00‑16:45
Alex Aiken (Stanford University)
Scalable Program Analysis Using Boolean Satisfiability [pdf] -
Friday, August 11th, 09:45‑10:30
Orna Grumberg (Technion)
Hybrid BDD and All-SAT Method for Model Checking [ppt] -
Friday, August 11th, 11:00‑11:45
Aarti Gupta (NEC Labs)
Verifying C Programs using SAT-based model checking [pdf] -
Friday, August 11th, 11:45‑12:30
Ofer Strichman (Technion)
Decision Heuristics based on an Abstraction/Refinement model [ppt] -
Friday, August 11th, 14:00‑14:45
Sharad Malik (Princeton University)
Optimization and Relaxation in SAT Search [pdf] -
Friday, August 11th, 14:45‑15:30
Alessandro Cimatti (IRST)
Reasoning about Bit Vector programs with Decision Procedures [ppt] -
Friday, August 11th, 16:00‑16:45
Robert Nieuwenhuis (Technical University of Catalonia)
The new architecture and solvers in the Barcelogic tool for SAT modulo theories [pdf]
Organizers
Sponsor
