Advertisement
Published in:
2009 | OriginalPaper | Chapter
VS3: SMT Solvers for Program Verification
Authors : Saurabh Srivastava, Sumit Gulwani, Jeffrey S. Foster
Published in: Computer Aided Verification
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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 ∀ ∃ properties of programs and to infer worst case upper bounds and preconditions for functional correctness.