Exceptflat: Program Verifier Prototype for Subsystems

Bart Jacobs and Frank Piessens

exceptflat is a program verifier prototype for programs written in a small Java-like language that includes the subsystems constructs.

The basic ideas are as in the paper. However, for framing and invariants, the Spec#/Boogie approach is used instead of separation logic. Also, the language includes a compensation construct that is more practical than the pattern described in the paper, whereas the latter is more suitable for expository purposes.

• exceptflat.jar (4.6 MB) - executable jar file (requires Java)
• except1.ef - single-threaded example program
• except2.ef - multithreaded example program
• except3.ef - example program with compensation
• except4.ef - another example program with compensation, where the allocation construct is in a separate method

The executable jar file uses the Z3 SMT solver. It looks for it in the current directory. Unfortunately, Z3 is available only on Windows.

Exceptflat is based on a specflat implementation by Jan Smans and Bart Jacobs.

Last update: 2008-07-04.