Paper Info
Title
VS3: SMT Solvers for Program Verification
Abstract
We present VS3, 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. VS3 discovers program invariants with arbitrary, but prespecified, quantification and logical structure. The user supplies VS3 with a set of predicates and invariant templates. VS3 automatically finds instantiations of the unknowns in the templates as subsets of the predicate set. We have used VS3 to automatically verify *** *** properties of programs and to infer worst case upper bounds and preconditions for functional correctness.
Year
DOI
Venue
2009
10.1007/978-3-642-02658-4_58
CAV
Keywords
Field
DocType
functional correctness,smt solvers,weak precondition,program verification,invariant template,verifies complex property,program invariants,logical structure,predicate set,upper bound,maximally strong postconditions
Programming language,Path (graph theory),Predicate abstraction,Computer science,Correctness,Algorithm,Theoretical computer science,Structure (mathematical logic),Invariant (mathematics),Template,Predicate (grammar)
Conference
Volume
ISSN
Citations 
5643
0302-9743
13
PageRank 
References 
Authors
0.76
7
3
Name
Order
Citations
PageRank
Saurabh Srivastava118419.27
Sumit Gulwani22263110.91
Jeffrey S. Foster32035174.45