SimplifyExplanation

The Simplify automated theorem prover was written by Greg Nelson and others at DEC-SRC around fifteen years ago. It is implemented in Modula-III. Until very recently it was still considered the premier automated theorem prover for software verification tools. It supports reasoning about a decidable fragment of first-order logic that includes a theory of arrays, uninterpreted function symbols, and linear arithmetic.

The only recent development on Simplify that has taken place is the MOBIUS port of it to Mac OS X, building new releases with new Modula-III compilers, as well as some simple bug fixes. There are no plans on doing any development on Simplify, as the world of first-order theorem provers has changed quite a bit over the past decade or so. Instead, we are working on integrating ESC/Java2 with new-generation SMT-LIB provers, as discussed later in this chapter.

Simplify has been wrapped in the new MOBIUS prover backend, thus is accessible in a simple, transparent fashion like many other new generation automated provers.

Version: 1 Time: Fri Mar 28 18:22:25 2008 Author: dcochran (dcochran) IP: 193.1.132.32