Home Intro Wiki Docs FAQ Download Mail FM Tools

Symbolic Analysis Laboratory

To become practical for assurance, automated formal methods must be made more scalable, automatic, and cost-effective. Such an increase in scope, scale, automation, and utility can be derived from an emphasis on a systematic separation of concerns during verification. SAL (Symbolic Analysis Laboratory) attempts to address these issues. It is a framework for combining different tools to calculate properties of concurrent systems.

The heart of SAL is a language, developed in collaboration with Stanford and Berkeley, for specifying concurrent systems in a compositional way. It is supported by a tool suite that includes state of the art symbolic (BDD-based) and bounded (SAT-based) model checkers, an experimental "Witness" model checker, and a unique "infinite" bounded model checker based on SMT solving. Auxiliary tools include a simulator, deadlock checker and an automated test generator.

SAL 3.3 is the current version of the SAL tool suite. It is open source (under the GPL license), and we also provide pre-built binaries for several common architectures. See the download page for details.

 *NEW* We have released HybridSAL (June 2007): a tool for abstracting hybrid systems (specified in an extension of SAL) to SAL specifications.

With SAL 3.0, we have introduced the SAL Wiki; this is intended to be the main vehicle for information and documentation about SAL. Some of information that was in static html pages has been moved to the Wiki, and an FAQ has been created there.

SAL is one of the SRI FormalWare tools.

Home Intro Wiki Docs FAQ Download Mail FM Tools

Last modified: Mon 22 Apr 2013 17:50 UTC
Maintainer: Bruno Dutertre