EST is a registered project at Savannah.
EST 1st Edition
Project: Efficient Symbolic Tools package - 1st Edition
Synopsis: EST 1st Edition is a tool for the formal verification of concurrent systems
Administrator: Robert Meolic (firstname.lastname@example.org)
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 Biddy BDD package, 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
an example of verification.
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.
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
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, flex, and pthreads 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 binary distribution of EST 1st Edition - interactive version with Tcl/Tk GUI My Interface
- est-1ed-1-5-4-source.zip, Apr 25, 2015, SVN revision 103
- est-1ed-1-5-3-source.zip, Oct 28, 2014, SVN revision 96
- est-1ed-1-5-2-source.zip, Oct 15, 2010, SVN revision 23
- est-1ed-1-5-1-source.zip, Jul 30, 2007, SVN revision 15
- est-1ed-1-5-source.zip, Jul 19, 2007, SVN revision 14
Download binary distribution of EST 1st Edition - libraries and projects
(i386, GNU/Linux, Tcl/Tk),
(i386, GNU/Linux, Debian, Tcl/Tk),
(i386, GNU/Linux, RPM, Tcl/Tk),
(i386-64, GNU/Linux, Tcl/Tk),
(i386, MacOSX, Tcl/Tk),
(sun4u, Solaris, Tcl/Tk),
(i386, Win32, Tcl/Tk).
(deb and rpm packages do not include projects)
(i386, GNU/Linux, Debian),
(i386, GNU/Linux, RPM),
EST 1st Edition - release 1.4 (Jun 13, 2007)
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
EST 1st Edition - release 1.3 (Jan 15, 2007)
The most important changes from release 1.2
- [all] mingw and sunos specific files removed from the project
- [all] makefiles improved
EST 1st Edition - release 1.2 (Oct 20, 2006)
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
EST 1st Edition - release 1.1 (Sep 16, 2003)
The most important changes from release 1.0
- [mc] standard ACTL model checking
Sources not available.
- [pa] parser for process algebra is now more roboust
- [pa] added simple recovery on syntax errors
- [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
EST 1st Edition - release 1.0 (1999 - 2003)
Sources not available.
- 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.
- In 1992, Aleš Časar and Robert Meolic implemented the first version of BDD package. It was written in Pascal and ran on VAX 4000-600. In 1994, Aleš Časar rewrote the package in C.
- In 1995, Aleš Časar implemented CTL model checker on finite state machines. His package is not a part of EST, but it served as a basis for ACTL model checker.
- In 1996, Mirjam Sepesy Maučec implemented a package for description and formal verification of concurrent systems with a simple CCS-like process algebra. Her package was called Versis (VERifikacija SIStemov) and was capable of performing basic operations on processes, parallel composition of processes, and checking strong and observational equivalence between processes. It was written in C and ran on HP Workstation.
- In 1999, Robert Meolic formed the first version of EST package. It was based on časar-Meolic's BDD package and Sepesy Maučec's Versis package. The code from BDD package had been purified and transformed into module called 'bdd'. The code from Versis package had been completelly rewrited and splited into two modules called 'pa' and 'versis'. Many improvements had been done and a lot of features had been added in comparison with the original packages. The first version of EST, which is now called EST 1st Edition, already contained testing equivalence checker, simple ACTL model checker and Tcl/Tk GUI called My Interface.
- Afterwards, many releases has been formed and all of them was stated to be
version 1.0. In August 2003, all packages have been reorganized and partially rewrited.
Moreover, a CVS repository for EST package was created. All history notes (which
were not very useful) have been deleted. Version numbers began to increase.
Please, send your questions and comments to