Geodesic
F@BOOL@: experiment with a simple verifying compiler based on SAT-solvers
Modelirovanie i analiz informacionnyh sistem, Tome 17 (2010) no. 4, pp. 111-124

Voir la notice de l'article provenant de la source Math-Net.Ru

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.
Keywords: formal program verification, operational and transformational semantics, Floyd–Hoare proof technique, correctness conditions, SAT-solvers. 
@article{MAIS_2010_17_4_a11,
     author = {N. V. Shilov},
     title = {F@BOOL@: experiment with a simple verifying compiler based on {SAT-solvers}},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {111--124},
     publisher = {mathdoc},
     volume = {17},
     number = {4},
     year = {2010},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a11/}
}
TY  - JOUR
AU  - N. V. Shilov
TI  - F@BOOL@: experiment with a simple verifying compiler based on SAT-solvers
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2010
SP  - 111
EP  - 124
VL  - 17
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a11/
LA  - ru
ID  - MAIS_2010_17_4_a11
ER  - 
%0 Journal Article
%A N. V. Shilov
%T F@BOOL@: experiment with a simple verifying compiler based on SAT-solvers
%J Modelirovanie i analiz informacionnyh sistem
%D 2010
%P 111-124
%V 17
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a11/
%G ru
%F MAIS_2010_17_4_a11
N. V. Shilov. F@BOOL@: experiment with a simple verifying compiler based on SAT-solvers. Modelirovanie i analiz informacionnyh sistem, Tome 17 (2010) no. 4, pp. 111-124. http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a11/