2009 | OriginalPaper | Buchkapitel
VS3: SMT Solvers for Program Verification
verfasst von : Saurabh Srivastava, Sumit Gulwani, Jeffrey S. Foster
Erschienen in: Computer Aided Verification
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. 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.