A verifying compiler automatically verifies the correctness of a source program before compiling it. Founded on the definition of the source language and a set of rules (a methodology) for using the language, the program's correctness criteria and correctness argument are provided in the program text by interface specifications and invariants.
This paper describes the program-verifier component of a verifying compiler for a core multi-threaded object-oriented language. The verifier takes as input a program written in the source language and generates, via a translation into an intermediate verification language, a set of verification conditions. The verification conditions are first-order logical formulas whose validity implies the correctness of the program. The formulas can be analyzed automatically by a satisfiability-modulo-theory (SMT) solver.
The paper defines the source language and intermediate language, the translation from the former into the latter, and the generation of verification conditions from the latter. The paper also builds a methodology for writing and verifying single- and multi-threaded code with object invariants, and encodes the methodology into the intermediate-language program.
The paper is intended as a student's guide to understanding automatic program verification. It includes enough detailed information that students can build their own basic program verifier.
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 firstname.lastname@example.org
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 email@example.com