The SPIKE system is an automatic theorem prover for Horn equational logics. SPIKE 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 designed for supporting 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 automatization of numerous routine tasks.
The SPIKE system belongs to the family of program verification tools. 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 necessary proofs are tedious and verification by hand becomes rapidly unreliable. This shows the importance of automatic proof systems such as SPIKE, for eliminating an important ratio of such computations.
Spike is applied to the validation of circuits as well as programs (in collaboration with CNET-France-Telecom) and is also used as a teaching tool (e.g. at ESIAL, an engineer school in Nancy).
Contact: Adel Bouhoula, Sorin Stratulat and Michael Rusinowitch
Adel.Bouhoula @ loria.fr, Sorin.Stratulat @ loria.fr