FormalWare at SRI
The SRI Computer Science Laboratory has been working in the area of Formal
Methods for three decades. This page provides an overview of the
currently available Formal Methods Tools.
The roadmap document gives a high level
description of these tools, and is a good place to find out which tool
would be most useful to you, and what future plans we have for existing
and new tools.
- PVS
- The Prototype Verification System consists of a specification language
built on higher-order logic, and a classical interactive theorem prover.
- SAL
- The Symbolic Analysis Laboratory consists of a specification language
that is designed for transition system descriptions, and a suite of
tools for analyzing these systems.
- ICS
- The Integrated Canonizer/Solver is a decision procedure for a
combination of theories, including arithmetic and uninterpreted
functions.
Last modified: Tue Nov 11 15:34:32 PST 2003
by Sam Owre