We present VS~3, 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~3 discovers program invariants with arbitrary, but prespecified, quantification and logical structure. The user supplies VS~3 with a set of predicates and invariant templates. VS~3 automatically finds instantiations of the unknowns in the templates as subsets of the predicate set. We have used VS~3 to automatically verify {arbitar}{exist} properties of programs and to infer worst case upper bounds and preconditions for functional correctness.
展开▼
