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] (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.
|
|
