Efficient Symbolic Tools package (EST) is a tool for the
formal verification of systems.
|
EST distinguishes itself as a small and portable package
with a readable source code in C and well implemented algorithms.
EST runs on many different computers with different
operating systems, including GNU/Linux, MS Windows, and Solaris.
|
|
EST is a collection of symbolic algorithms based on binary decision diagrams (BDDs).
Curently, it supports only our own BDD package called Biddy, but one day it
could support other BDD packages, too.
|
|
EST itself provides libraries of functions, which you can use in
your own main program. Or, you can try our simple Tcl/Tk GUI called
My Interface, from which you can access all the features.
|
EST project has started in 1992. In 1999, we devided it into two
branches called EST 1st Edition and EST 2nd Edition.
Please, follow the given links to obtain source and binary releases.
EST is a free software. We can show you every single line of code and we will explain you the meaning of all used constructs if you ask for that. However, it is a sort of academic research software. Some tricks are used, which are not clear to anyone except the author. Thus, do not hesitate to ask us any question you may have about EST.
|
Latest stable sources
est-1ed-1-5-1-source.zip
est-2ed-5-1-source.zip
Binary distributions
EST 1st Edition
EST 2nd Edition
Links
Local SVN repository
Savannah CVS repository
Savannah main page
Usefull links
Documentation
* The Efficient Symbolic Tools package, 2000:
paper,
slides
* Notes on specifying systems in EST, 2006:
paper,
slides
Sorry, no user manual, yet!
|