Automated Program Verification with SPIKE
by Adel Bouhoula and Michael Rusinowitch
The SPIKE system, developed in Nancy as part of the PROTHEO project
(see previous article), belongs to the family
of proof assistants for program verification. SPIKE is designed for the
construction of correct specifications through verification of properties
by induction.
The development of a program requires a certain number of proof obligations.
First of all, it must be verified that the program meets the original specifications.
Similarly, the transformation steps that lead to more efficient programs
must be formally justified to avoid any divergence from the initial specifications.
In general, the proofs are tedious and verification by hand becomes rapidly
unreliable. Automated or semi-automated proof assistants are essential
for eliminating an important ratio of proof obligations.
SPIKE is designed for the construction of correct specifications through
verifying properties by induction. In contrast to the majority of current
proof systems that construct their proofs step by step and require frequent
user intervention, not to say a great expertise on the part of the user,
SPIKE is meant to reduce the number of interactions due to the automation
of numerous routine tasks.
The SPIKE system is an automatic theorem prover for Horn equational
logics. It is written in Caml Light, a functional language of the ML family.
The program is provided with a graphic interface in TCL/TK that allows
for interaction through the mouse and menus.
SPIKE is applied to the validation of circuits as well as programs (in
collaboration with CNET-France-Telecom) and is also used for teaching formal
methods at ESIAL, an engineer school in Nancy. See also http://www.loria.fr/~bouhoula/spike.html
Please contact:
Adel Bouhoula - LORIA-INRIA
Tel: +33 3 83 59 30 55
E-mail: Adel.Bouhoula@loria.fr
Michael Rusinowitch - LORIA-INRIA
Tel: +33 3 83 59 30 20
E-mail: Michael.Rusinowitch@loria.fr
