EST EST Home Page

Efficient Symbolic Tools package (EST) is a tool for the formal verification of systems.
EST 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 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 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 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 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

Binary distributions
EST 1st Edition
EST 2nd Edition

EST SVN repository
EST bug reports
EST Projects
Usefull links

* The Efficient Symbolic Tools package, 2000: paper, slides
* Notes on specifying systems in EST, 2006: paper, slides

Sorry, no user manual, yet!

Please, send your questions and comments to