Hossein Hojjat

In the general approach of verification condition generation, as shown in The big picture of vcg, an annotated source code is processed to derive a set of formulas. The formulas are then given to a theorem prover for further analysis. Deriving verification conditions for a practical language such as Java or Scala is difficult. In many previous attempts the source code is translated to a simple intermediate language.

• Extended Static Checker for Java (ESC/Java): Uses guarded-command languages as intermediate language. The translation is described in Checking Java Programs via Guarded Commands. The approach is divided into two steps. In the first step Java is translated to a “sugered” guarded command language. This language contains high level features such as iteration. In the second step the sugered guarded language is transferred to a primitive language.
• Boogie: Uses an assembly-like language called “BoogiePL”. BoogiePL has ignored many complexities of full object oriented languages, while has incorporated some features for the target logic. For example, BoogiePL does not have the notion of classes and interfaces, but it has pre- and post- conditions.

The hosseinreport3.pdfreport of this project, in the two-column format. Note that the report is being updated regularly, so please feel free to press F5 and see a newer version!

hossein-pres.pdfPresentation

SAL Language Report

Rustan Leino's page

Viktor's thesis

Spec#

guru