F@BOOL@: Experiment with a simple verifying compiler based on SAT-solvers |
| |
Authors: | N V Shilov |
| |
Affiliation: | 1.A.P. Ershov Institute of Informatic Systems, Siberian Branch,Russian Academy of Sciences,Novosibirsk,Russia;2.Novosibirsk State University,Novosibirsk,Russia;3.Novosibirsk State Technical University,Novosibirsk,Russia |
| |
Abstract: | A verifying compiler is computer system program that translates programs written by a human from a high-level language to
equivalent executable programs and proves (verifies) mathematical statements specified by a human concerning the properties
of the translated programs. The objective of the project F@BOOL@ is to develop a user friendly, compact, and portable verifying
compiler of annotated computational programs that uses efficient and reliable automatic SAT solvers as the tools for automatic
validation of correctness conditions (instead of semiautomatic proof techniques). In the period from 2006 to 2009, the SAT
solver zChaff was used in the project F@BOOL@. The first experiments on the verification of simple Mini-NIL programs were
performed using this solver, namely, the programs swapping variable values, checking whether three integer numbers are the
sides of an equilateral or an isoscales triangle, and searching for one fake coin among 15 coins using scales. This paper
considers the main ideas of the project F@BOOL@ and gives the details of the experiment on the verification of the program
solving the coin puzzle. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|