F@BOOL@: experiment with a simple verifying compiler based on SAT-solvers

A verifying compiler is a system computer program that translates programs written by man from a high-level language into equivalent executable programs, and besides, proves (verifies) mathematical statements specified by man 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 computational programs, that uses effective and sound automatic SAT-solvers (i.e. programs that check satisfiability of prepositional 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 the verification of functional properties, and it assumes generation of first-order verification conditions (from invariants), and the validation/refutation of each verification condition using SAT-solvers after “conservative” translation of the verification conditions into 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.