Efficient Symbolic Tools package (EST) is a tool for the
formal verification of systems.
EST project has started in 1992. In 2000, we created two
branches called EST 1st Edition and EST 2nd Edition.
Please, follow the given links to obtain source and binary releases.
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, Mac OSX, 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 programs. Here are
our EST projects.
Moreover, you can run EST interactively by using simple Tcl/Tk GUI called
My Interface, from which you can access all the features.
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 1st Edition
EST 2nd Edition
Local SVN repository
Savannah CVS repository
Savannah main page
* The Efficient Symbolic Tools package, 2000:
* Notes on specifying systems in EST, 2006:
Sorry, no user manual, yet!