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.0 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 are also introducing the SAL Wiki; this will become the main vehicle for information and documentation about SAL. Some of information that was in static html pages has already 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: Tue 24 Aug 2010 14:21 PDT
Maintainer: Bruno Dutertre