SALenv: A SAL State Space Exploration Toolkit
SALenv is a state space exploration toolkit which may be used to build model checkers,
simulators, static debuggers, symbolic simulators, and other tools for the SAL specification language.
Abstractly, the toolkit provides an API to traverse the concrete (or abstract)
state space associated with a SAL specification. SALenv can also be seen as an
open model checker, where a substrate of the implementation is open, allowing the
user to extend, customize, and modify the implementation to affect functionality and/or
performance. The toolkit is similar to an open compiler such as Open-C++, or
an extensible application such as Emacs and AutoCAD. User extensions and modifications
should be coded in the Scheme programming language. These extensions may even be compiled and linked with the kernel.
Distribution:
- Download - free of charge for non-commercial use under the FM license
Please fill in this form and mail or fax to the address on the front cover. You will receive a login to download any SAL component
when your license has been processed.
SALenv Documentation:
SALenv documentation is available in various formats.
You may download the documentation or browse the html from this
site. The SALenv reference manual is available in:
Live Demo of the SRI LTL to Büchi Automata Converter
Try the live interactive demo of the LTL to Büchi Automata converter.
Last updated Jul 22 2002 by
Leonardo de Moura
