beyer_2007-08-29
BLAST release 2.4
This distribution of BLAST includes the following third party components:
- Interpolation procedure FOCI,
- Interpolation procedure CLP-Prover,
- Theorem prover Simplify (version 1.5.4, 4 October 2001)
- BDD-package CUDD
- Compiler frontend CIL
The following files are provided:
blast-2.4.tar.gz
OCaml source files that are needed to build BLAST,
including sources of CUDD and CIL,
and binaries of FOCI, CLP-Prover, and Simplify.
blast-2.4_linux-bin.gz
Executable program,
compiled under OCAML 3.09.2 and GCC 4.1.2.
New features of Blast 2.4:
- Interpolation procedure separated from the model-checking engine.
Blast 2.4 includes a new interface for interpolation procedures
that makes it easier to integrate alternative programs.
Currently, two external executables for interpolation are integrated:
FOCI and CLP-Prover.
- Theorem-prover interface based on the SMT-LIB expression language.
Blast 2.4 still uses Simplify as default theorem prover.
But by editing the configure file 'smt_solver' and using option '-smt',
any solver that supports the SMT-LIB standard can be plugged-in
as external executable. http://combination.cs.uiowa.edu/smtlib/
See also smt_lib/server/README.
Integration concept for external solvers (FOCI, SMT-Solvers):
For each solver that is integrated as external program,
there is a server process that does the following:
1. Start solver program as separate process.
2. Wait for query from BLAST and give it to the solver process.
3. Get the result from the solver and give it back to BLAST.
4. Go to step 1 after the solver process is terminated.
FOCI: The performance loss due to the restarts of executables is kept
minimal by the server process -- it not even doubles the run times.
(In the current version, FOCI needs to be killed in step 4 if an error occurred.)
CLP-Prover: This tool is based on constraint solving, and therefore,
when a lot of disjunctions occur, it shows exponential blow-up.
(CLP-Prover can be repeatedly queried and does not need to be
terminated in step 4.)
SMT-Solvers: Compared to Simplify, the SMT solvers that we have tried
suffered a lot from getting identical parts of a formula again and
again, whereas Simplify supports a 'context stack' on which we
can keep parts of formulas that would otherwise occur in many queries.
There is potential for optimization, since we do not use the power
that the SMT-solvers provide, e.g., encoding array and pointer
operations on a higher level supported by the SMT-solvers.
We successfully tried Yices, CVC3, and z3.
http://combination.cs.uiowa.edu/smtlib/