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.frMichael Rusinowitch - LORIA-INRIA
Tel: +33 3 83 59 30 20
E-mail: Michael.Rusinowitch@loria.fr