This was a one-day workshop on Integrated Formal Methods based around the SRI tools PVS, SAL, and Yices. The workshop included a half-day tutorial on the novel and advanced features of these systems, and another half-day session devoted to contributed talks.
The contributed session included talks from within the user community of PVS, SAL, and Yices. These contributions reported on experiments carried out with these tools, experience integrating these tools into other systems, and comparisons with other comparable tools.
PVS is a comprehensive system for formal specification and analysis. It provides an attractive specification language based on higher order logic extended with dependent types and predicate subtypes, and includes constructs for recursively defined abstract data types, recursive functions, inductive relations, and tabular specifications, as well as traditional logical formulas. Analysis capabilities include very strong typechecking (which can involve theorem proving), direct execution (at speeds within a factor of five of hand-crafted C), theorem proving, and model checking. The PVS theorem prover provides powerful automation including rewriting and decision procedures for real and integer arithmetic, and is scriptable. The system is supported by massive built-in and user-provided libraries of specifications for mathematics and computer science.
Whereas PVS can be applied to any formalized mathematics, SAL is specialized to the specification and analysis of state machines and can therefore apply more targeted automation. SAL is supported by a suite of tools based on state-of-the-art model-checking technology for LTL properties but, unlike other model checkers, it is not restricted to finite-state state systems. And unlike most other languages for model checkers, SAL supports fairly high-level specifications, with a type system similar to that of PVS. For finite state systems, SAL provides both a symbolic model checker (using BDDs) and a bounded model checker (using a SAT solver); for infinite state systems it provides an ``infinite bounded'' model checker that uses SMT solving. The bounded model checkers can verify safety properties by k-induction and can make use of lemmas. The infinite bounded model checker blurs the line between theorem proving and model checking: it has been used to automate (in a few lines of specification and a few seconds of execution) verifications that previously required weeks of work using interactive systems such as PVS. SAL is scriptable (in Scheme); an example is a script that performs automated test case generation.
Satisfiability Modulo Theories (SMT) generalizes boolean satisfiability by adding equality reasoning, arithmetic, and other useful first-order theories. Yices is a new SMT solver developed at SRI that is capable of deciding the satisfiability of large and propositionally complex formulas in a rich combination of theories. Yices supports linear arithmetic, uninterpreted functions, bit vectors, arrays, recursive datatypes, first-order quantifiers, and more.
Yices is implemented in C++ and can be used as a standalone tool or as a library in other software. Its input language is related to PVS's and SAL's but it has a Lisp-like syntax. The Yices type system is also similar to the PVS type system and includes subtypes and dependent types. Beyond pure SMT solving, Yices can solve MAX-SAT or MAX-SMT problems, compute unsatisfiable cores, and construct models. It can also be used as a regular boolean SAT solver.
Yices 1.0 is embedded as a new decision procedure in PVS. In this application, Yices complements the existing decision procedures of PVS that are primarily designed for interactive theorem proving but can be overwhelmed by large proof goals with a complex proposition structure. Yices provides the capability to automatically discharge such goals in a fire-and-forget mode.
The latest version of SAL includes Yices 1.0 as a backend solver. In SAL, Yices can be used both as a SAT solver for finite-state bounded model checking and as the default SMT solver for the SAL infinite-state bounded model checkers.
PVS, SAL, and Yices are available under license from SRI; there is no charge for research and educational use.
More papers on formal methods and automated verification by SRI authors be found at http://www.csl.sri.com/programs/formalmethods/.