Guided tour inside F@BOOL@: a case-study for a SAT-based verifying compiler

A verifying compiler is a system program that translates programs written by an user from a high-level language into equivalent executable programs, and besides, proves (verifies) mathematical statements specified by the human about the properties of the programs being translated. The purpose of the F@BOOL@ project is to develop a transparent for users, compact and portable verifying compiler F@BOOL@ for annotated computer programs, that uses effective and sound automatic SAT-solvers (i.e. programs that check satisfiability of propositional Boolean formulas in the conjunctive normal form) as means of automatic validation of correctness conditions (instead of semi-automatic proof techniques). The key idea is Boolean representation of all data instead of Boolean abstraction or first-order representation. (It makes difference between F@BOOL@ and SLAM.) Our project is aimed at verification of functional properties, and it assumes generation of first-order verification conditions (from invariants) and validation/refutation of each verification condition using SAT-solvers after their conservative translation into a Boolean form. During the period from 2006 to 2009, a popular (at that time) SAT-solver zChaff was used in the F@BOOL@ project. The first three verification experiments that have been exercised with its help are listed below: swapping values of two variables, checking whether three input values are lengths of sides of an equilateral or isosceles triangle, and detecting a unique fake in a set of 15 coins. The paper presents general outlines of the project and details of the last (the most extensive) experiment.