FormalWare at SRI

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 4.0. Yices has been available since August 2006; its current version is 1.0. Its prototypes Yices 0.1 and Simplics were available since July 2005 and its predecessor ICS since 2001. Yices 1.0 won every division in the 2006 SMT Competition.

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.

PCE

We are also getting involved in probabilistic inferencing, and have a Probability Consistency Engine (PCE) tool for reasoning over Markov Logic Networks.

The information below is rather outdated, but we now have an SRI FM-Wiki. We're still learning how best to organize and use this new capability--please join in and help.

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

Recent 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.