Efficient Symbolic Tools (EST) is a toolbox 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 different operating systems, including GNU/Linux and MS Windows.

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 projects. Moreover, you can run EST interactively by using simple Tcl/Tk GUI called My Interface.

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.