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 [1] (http://sal.csl.sri.com) (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, Berkeley, and Verimag, for specifying concurrent systems in a compositional way. Its verification toolbox includes an explicit-state model checker, a symbolic model checker, a witness-producing model checker, and a bounded model checker.