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/

[1] A. Akho, Dzh. Khopkroft, Dzh. Ulman, Postroenie i analiz vychislitelnykh algoritmov, Mir, M., 1979 | MR

[2] E. V. Bodin, N. A. Kalinina, N. V. Shilov, Proekt verifitsiruyuschego kompilyatora F@BOOL@ Chast I: Obschee opisanie proekta F@BOOL@, ego mesto v komponentnom podkhode k programmirovaniyu. Yazyk Mini-NIL — prototip yazyka virtualnoi mashiny proekta, Preprint No 131, Instituta sistem informatiki im. A. P. Ershova SO RAN, 2005

[3] E. V. Bodin, N. A. Kalinina, N. V. Shilov, Proekt verifitsiruyuschego kompilyatora F@BOOL@. Chast II: Logicheskie annotatsii v yazyke Mini-NIL, ikh staticheskaya semantika i semantika vremeni ispolneniya, Preprint No 138, Instituta sistem informatiki im. A. P. Ershova SO RAN, 2006

[4] V. E. Deikstra, Distsiplina programmirovaniya, Mir, M., 1978

[5] D. Gris, Nauka programmirovaniya, Mir, M., 1984

[6] N. V. Shilov, E. V. Bodin, I. Ii, “O programmnykh logikakh — prosto”, Cistemnaya informatika, 8 (2002), 206–249, Nauka, Novosibirsk

[7] N. V. Shilov, I. S. Anureev, E. V.Bodin, “O generatsii uslovii korrektnosti dlya imperativnykh programm”, Programmirovanie, 2008, no. 6, 1–20 | MR

[8] N. V. Shilov, “Zametki o trëkh paradigmakh programmirovaniya”, Kompyuternye instrumenty v obrazovanii, 2010, no. 2, 24–37

[9] I. S. Anureev, E. V. Bodin, L. V. Gorodnyaya, A. G. Marchuk, F. A. Murzin, N. V. Shilov, “On the Problem of Computer Language Classification”, Joint NCC Bulletin, Series Computer Science, 28, 2008, 1–29

[10] T. Ball, B. Cook, V. Levin, S. K. Rajamani, “SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft”, LNCS, 2999, Springer-Verlag, Berlin, 2004, 1–20

[11] D. Beyer, T. A. Henzinger, R. Jhala, R. Majumdar, “The Software Model Checker Blast: Applications to Software Engineering”, Int. Journal on Software Tools for Technology Transfer, 2007, no. 9, 505–525

[12] R. W. Floyd, “Assigning meanings to programs”, Proc. of a Symposium in Applied Mathematics, Mathematical Aspects of Computer Science, 19, American Math. Society, Providence, R.I., 1967, 19–32 | MR

[13] C. A. R. Hoare, “The Verifying Compiler: A Grand Challenge for Computing Research”, Perspectives of Systems Informatics (PSI'2003), LNCS, 2890, Springer-Verlag, Berlin, 2003, 1–12 | MR | Zbl

[14] N. V. Shilov, Eu. V. Bodin, S. O. Shilova, “Fabulous arrays I: Operational and transformational semantics of static arrays in vericationproject F@BOOL@”, Bull. Nov. Comp. Center, Comp. Science, 29 (2009), 121–140