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.


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