ESAT (Evolvable Systems Animator Tool) is a Java based simulator for the Evolvable Systems Framework described in this page:

http://www.cs.man.ac.uk/~david/evolution/evolution.html

ESAT accepts as input a specification of an evolvable system in textual form, and uses several first order logic Automated Theorem Proving (ATP) programs to resolve proof obligations that are generated on the fly while simulating the specification. The tool produces execution traces.

ESAT can generally use any Prover that accepts the TPTP format. ESAT is currently used with: e-darwin, eprover, iprover, metis, prover9, vampire, darwin, ekrhyper, equinox, mac4 and paradox.

The tool is presented in these papers:

* ESAT: A Tool for Animating Logic-based Specifications of Evolvable Computing Systems,

Djihed Afifi, David E. Rydeheard and Howard Barringer. Runtime Verification, RV 2010. LNCS 6418.

* Automated Reasoning in the Simulation of Evolvable Systems,

Djihed Afifi, David E. Rydeheard and Howard Barringer. FLOC 2010 Workshop on Practical Aspects of Automated Reasoning (PAAR) 2010.

Download:

ESAT is written in Java and has been tested on Windows, Linux and Mac OS (Intel) systems.

The following download contains ESAT without any of the prover binaries. To get help into using the prover binaries please contact djihed at cs.man.ac.uk

* esat-0.2.zip

Please send any comments and bug reports to Djihed Afifi: djihed at cs.man.ac.uk