FreeBoogieExplanation

Freeboogie aims to be a backend for verification tools such as Spec# and future versions of ESCJava2 and similar tools. It takes as input a BoogiePL (Boogie Programming Language) file, generates verification conditions, calls provers such as Simplify and Z3, and reports the errors in a way that relates to the BoogiePL source. It is a work in progress.

The most important part missing is the verification condition generation. The tool can already be used to parse, typecheck, and build symbol tables and flow graphs for BoogiePL code. The AST data structures are generated from a short description of the BoogiePL abstract grammar by a tool included in Freeboogie. The backend communicates with Simplify and with Z3 running in Simplify mode. (There are only minor differences in the way the two provers communicate.) The design allows adding other provers easily, in particular there is support for sort-checking that should facilitate adding sorted provers.

The API is available at [http://radu.ucd.ie/freeboogie/doc/].

The Spec# system from Microsoft Research generates BoogiePL from the Spec# language, which is a variant of Microsoft's C# programming language with annotations. Another way of obtaining BoogiePL from a higher level language is via JACK (BBC+07), which translates Java with JML annotations into a variant of BML, and BML2BPL, which was developed at ETH under the MOBIUS project and translates BML into BPL. In fact, one design goal of BPL was to be used as an intermediate language by multiple verification tools, thereby reducing the implementation effort needed to support multiple high-level languages and multiple static analyzes at the same time.

An initial release of the Freeboogie subsystem, which supports parsing, name resolution, flow graphs, and typechecking, took place at T0+18.

Version: 4 Time: Mon Mar 31 16:11:57 2008 Author: dcochran (dcochran) IP: 193.1.132.32