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.

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

SAL is one of the SRI FormalWare tools.