VS3 Verification and Synthesis using SMT Solvers

Introduction

SMT Solvers (or Theorem Provers) have traditionally been used for verifying correctness of systems that have been annotated with relevant inductive invariants. Such an annotation usually is an undesirable burden on the user. This project explores techniques for using SMT solvers to automatically discover inductive invariants for proving given safety properties of systems. Additionally, this project also explores techniques for using SMT solvers to synthesize systems in the first place given enough specifications.

Saurabh Srivastava, who is leading work on this project in the context of software systems for his Phd dissertation, has maintained a more detailed webpage here.

Papers

• VS3: SMT Solvers for Program Verification, Tools Paper, CAV 2009, Saurabh Srivastava, Sumit Gulwani, and Jeffrey Foster [abstract |ps |pdf]
• Program Verification using Templates over Predicate Abstraction , PLDI 2009, Saurabh Srivastava and Sumit Gulwani [abstract |ps |pdf]
  This paper describes how to discover quantified invariants over a given set of predicates and templates (in order to prove given safety assertions) using SMT solvers. Additionally, it also describes how to discover quantified pre-conditions that ensure validity of given safety assertions, in case the safety assertions do not always hold.
• Constraint-based Invariant Inference over Predicate Abstraction, VMCAI 2009, Sumit Gulwani, Saurabh Srivastava, and Ramarathnam Venkatesan [abstract |ps |pdf]
  This paper describes how to discover invariants over predicate abstraction (for verification of safety properties) using SMT solvers.
• Synthesizing Switching Logic using Constraint Solving, VMCAI 2009, Ankur Taly, Sumit Gulwani, and Ashish Tiwari, [abstract |ps |pdf]
  This paper describes how to synthesize the switching logic in hybrid systems using SMT solvers.
• Constraint-based Approach for Analysis of Hybrid Systems, CAV 2008, Sumit Gulwani and Ashish Tiwari, [abstract |pdf]
  This paper describes how to discover polynomial invariants (for verification of safety properties) in hybrid systems using SMT solvers.
• Program Analysis as Constraint Solving, PLDI 2008, Sumit Gulwani, Saurabh Srivastava, and Ramarathnam Venkatesan, [abstract |ps] |pdf |ppt]
  This paper describes how to discover disjunctive linear invariants using bit-vector reasoning of SMT solvers.

• Sumit Gulwani (MSR Redmond)
• Saurabh Srivastava (Univ. of Maryland)
• Ashish Tiwari (SRI)
• Ramarathnam Venkatesan (MSR Redmond)