VS3 (Verification and Specification using SMT Solvers)

SMT Solvers 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 (opens in new tab), who is leading work on this project in the context of software systems for his Phd dissertation, has maintained a more detailed webpage here (opens in new tab).