Abstract

We present VS³, a tool that automatically verifies complex properties of programs and infers maximally weak preconditions and maximally strong postconditions by leveraging the power of SMT solvers. VS³ discovers program invariants with arbitrary, but prespecified, quantification and logical structure. The user supplies VS³ with a set of predicates and invariant templates. VS³ automatically finds instantiations of the unknowns in the templates as subsets of the predicate set. We have used VS³ to automatically verify \forall\exists properties of programs and to infer worst case upper bounds and preconditions for functional correctness.