EST 1st Edition


Project: Efficient Symbolic Tools - 1st Edition

Synopsis: EST 1st Edition is a toolbox for the formal verification of concurrent systems

Administrator: Robert Meolic (

Authors: Robert Meolic, Tatjana Kapus, Aleš Časar, Mirjam Sepesy Maučec, Zmago Brezočnik

History: started in 1992, first release in 1999

COBISS-ID: 5626902 (this number is used by Slovenian libraries)


[all] based on BDD package Biddy, includes API functions for Tcl/Tk GUI called My Interface

[pa] parser for simple textual representation of processes, encoding and decoding of processes, decoding of compositons

[versis] parallel composition, checking strong equivalence, observational equivalence, and testing equivalence, renaming, hiding and forbiding actions, searching for deadlocks and divergences

[mc] ACTL and ACTLW model checking

EST 1st Edition - release 1.5.x

The most important changes from release 1.4

[all] Biddy is isolated and does not belong to EST project anymore

[all] Biddy is now dynamically linked (v1.3 is required for release 1.5.4)

[all] modul gui added which covers functions removed in My Interface

[all] modul bdd added which covers functions removed in Biddy

[all] on MS Windows, bison and flex from MINGW distribution are used

[all] on MS Windows, EST is now compiled with MINGW 5.1.4 (gcc 3.4.5)

[all] improved packaging on MS Windows (using 7zsd.sfx)

[all] added Makefiles for Mac OS X (Darwin)

[all] makefiles improved and simplified

[all] adapted for 64-bit architectures

[all] added debian and rpm packaging

[all] Tcl/Tk related files are now compiled with Tcl Stubs

[all] all modules are using TCL stubs (to support changes in Tcl 8.5.10)

[all] added main program (it can be used instead of wish)

[all] added cmdsh mode (tcl api without mish gui)

[bdd] added experimental drawing of BDDs using bddview

Download sources, Apr 25, 2015, SVN revision 103, Oct 28, 2014, SVN revision 96, Oct 15, 2010, SVN revision 23, Jul 30, 2007, SVN revision 15, Jul 19, 2007, SVN revision 14

EST 1st Edition - release 1.4

The most important changes from release 1.3

[all] sources cleaned, makefiles fixed

[versis] implemented renaming, hiding and forbiding actions

[versis] implemented searching for deadlocks and divergences

Download sources, Jun 13, 2007, SVN revision 9

EST 1st Edition - release 1.3

The most important changes from release 1.2

[all] mingw and sunos specific files removed from the project

[all] makefiles improved

Download sources, Jan 15, 2007, SVN revision 7

EST 1st Edition - release 1.2

The most important changes from release 1.1

[all] improved dialogs

[all] supported tcl/tk 8.4

[all] makefiles improved, OS is now automaticaly recognized

[all] bdd package becomes a separated project called Biddy

[all] FSF rules to make program free are more strictly considered

Download sources, Oct 20, 2006, SVN revision 4

EST 1st Edition - release 1.1

The most important changes from release 1.0

[pa] parser for process algebra is now more roboust

[pa] added simple recovery on syntax errors

[mc] added standard ACTL model checking

[mc] semantics of ACTLW fixed

[mc] W is used instead of UU for unless

[mc] parser for ACTL/ACTLW is now more roboust

[mc] added simple recovery on syntax errors

Sources not available

EST 1st Edition - release 1.0

All version from 1999-2003 have been numbered as version 1.0. The last one was capable of representation of concurrent systems with LTSs, parallel composition of LTSs, strong, observational and testing equivalence checking between LTSs and ACTLW model checking on LTSs.

Sources not available

History notes

The project EST 1st Edition is now marked as matured, because we are not planning to add new features (others than GUI improvements). However, there is still a lot of work to do, including writing documentation, cleaning up the code, adding new examples etc. Hence, the project is not closed, yet.

Modules from EST 1st Edition and EST 2nd Edition are not interchangeable, i.e. EST 2nd Edition release-2-0 is not an upgrade of EST 1st Edition release-1-x.

In October 2006, we created local SVN repository for EST 1st Edition project (last version in this repository was labeled as revision 23). In October 2014, we created SVN repository at Savannah. First version in new repository is labeled as revison 95. Notes from local repository have not been passed to new repository.

Acknowledgement: Project EST 1st Edition has been entirely realized during the research process on Faculty of Electrical Engineering and Computer Science in Maribor, Slovenia. The project has been partly supported by the Slovenian Ministry of Science and Technology in years 1993-1995 and 1996-1998 under grants J2-5122-0796-95 and J2-7495-0796-96, respectively. From 1995-1997 the project has been partly supported by COST 247 project Verification and Validation Methods for Formal Descriptions.


Latest stable source

64-bit binary distribution (Tcl/Tk GUI)

(x86_64, GNU/Linux, Tcl/Tk, statically linked)


(amd64, GNU/Linux, Debian/Ubuntu, Tcl/Tk)


(x86_64, GNU/Linux, RPM, Tcl/Tk)


(x86_64, Windows, Tcl/Tk)

64-bit binary distribution (libraries only)

(x86_64, GNU/Linux, statically linked)



(amd64, GNU/Linux, Debian/Ubuntu)



(x86_64, GNU/Linux, RPM)


(x86_64, Windows)


The Efficient Symbolic Tools package, 2000

Notes on specifying systems in EST, 2006


EST Project page

EST SVN repository

Sorry, no user manual, yet!
Maribor, Slovenia