|
VS3
Template-based 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
- From Program Verification to Program Synthesis, POPL 2010,
Saurabh Srivastava, Sumit Gulwani, and Jeffrey Foster
[abstract
|ps
|pdf
|ppt slides]
This paper describes how to use program verification tools in an almost off-the-shelf manner to not only verify programs against their specifications, but also to synthesize them in the first place given their full-functional specifications. We can automatically synthesize several algorithms from undergraduate textbooks such as sorting algorithms, dynamic programming algorithms, and some numerical algorithms such as Strassen's sub-cubic matrix multiplication.
- VS3: SMT Solvers for Program Verification, Tools Paper, CAV 2009,
Saurabh Srivastava, Sumit Gulwani, and Jeffrey Foster
[abstract
|ps
|pdf
|ppt slides]
- Program Verification using Templates over Predicate Abstraction , PLDI 2009,
Saurabh Srivastava and Sumit Gulwani
[abstract
|ps
|pdf
|ppt slides]
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
|pdf slides]
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
|pdf slides]
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
|pdf slides]
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 slides]
This paper describes how to discover disjunctive linear invariants using bit-vector reasoning of SMT solvers.
People Involved