|
|
|
|
|
Symbolic Analysis LaboratoryTo 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 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.
|
 |
|
| Copyright 2005-2009 OnPedia.com. All Rights Reserved |
|
|