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

Abstract

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 (veri¯es) mathematical statements speci¯ed 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 anno-
tated computational programs, that uses e®ective and sound automatic SAT-solvers (i.e.
programs that check satis¯ability 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 ¯rst-order representation. (It makes di®erence be-
tween F@BOOL@ and SLAM.) Our project is aimed at the veri¯cation of functional
properties, and it assumes generation of ¯rst-order veri¯cation conditions (from invari-
ants), and the validation/refutation of each veri¯cation condition using SAT-solvers after
\conservative" translation of the veri¯cation conditions into Boolean form. During the
period from 2006 to 2009, a popular (at that time) SAT-solver zCha® was used in the
F@BOOL@ project. The ¯rst three veri¯cation 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.