FormalWare at SRI

The Formal Methods and Dependable Systems Program in the Computer Science Laboratory of SRI International has been at the forefront of Formal Methods research for three decades. During this period, we have developed several software tools for automated verification. This page provides an overview of our current tools and links for downloading them. All these tools are under active development, extension, and mutual integration.

PVS: The Prototype Verification System is a comprehensive verification environment: it provides a specification language in which mathematical theories and conjectures can be specified, together with an interactive theorem prover. The PVS specification language is a higher-order logic with a rich type system that supports concise and perspicuous specifications. Its theorem prover provides powerful automation, with decision procedures for several theories including real and integer arithmetic. PVS has been available since 1993, and has been Open Source since Version 4.0, released in December 2006.
Yices: is an SMT solver: it decides the satisfiability of propositional formulas containing uninterpreted function symbols with equality, linear real and integer arithmetic, scalar types, recursive datatypes, tuples, records, extensional arrays, fixed-size bit-vectors, quantifiers, and lambda expressions. It's basic capability resembles the decision procedures of PVS, but in a form that incorporates many new theoretical and practical insights and delivers vastly greater performance and scalability. Yices also does MaxSMT (and, dually, unsat cores) and is competitive as an ordinary SAT and MaxSAT solver. Yices can be used as a library in any application that requires "embedded deduction". Yices is used in SAL 3.0 and in PVS since version 4.0. Yices has been available since August 2006..
SAL: The Symbolic Analysis Laboratory is an environment for the exploration and analysis of concurrent systems specified as transition relations. Its language includes many of the attractive features of PVS. The SAL toolkit provides several tools for examining SAL specifications, including three different high-performance model checkers for LTL: symbolic, bounded, and infinite-bounded. The infinite-bounded model checker uses Yices to provide bounded model checking for systems defined over infinite data types, such as integers and reals. In addition, both the bounded and infinite-bounded model checkers can prove invariants by k-induction. SAL has been available since 2002, and has been Open Source since Version 3.0, released in December 2006.
HybridSAL: We have released (as of June 2007) a tool for abstracting hybrid systems (specified in an extension of SAL) to SAL specifications.

For an introduction to mechanized formal analysis using these tool, and an overview of their capabilities, please see this tutorial.

The information below is rather outdated.

For more information on the relationships between the tools and our plans for their evolution, please see our Roadmap.

Earlier papers on the theory, development, and applications of our tools are available here, while other papers can be found by by following links to our personal home pages.

Development of these tools has been funded by SRI International, the National Science Foundation, the National Aeronautics and Space Administration, the Naval Research Laboratory, and the Defense Advanced Research Projects Agency.