spike-prover

The SPIKE ProverSPIKE is an automated theorem prover based on 'Descente Infinie' induction. It is written in Objective Caml.

For the moment, we deliver:

an example of specification file (some interesting equational conjectures only !!!) the bytecode and native Windows executable versions SPIKE tries to prove the conjectures from a specification file , by running spike_bc or spike_nc . You may need to install Objective Caml in order to run the prover.

SPIKE's user manual is under development. If you don't want to wait until its release, you can find below a list of recent publications (starting from 2000) about or related to SPIKE. This list is NOT exhaustive.

CONTACTSPIKE is currently developped by Sorin Stratulat. A previous version has been initiated by M. Rusinowitch and A. Bouhoula.

You can contact Sorin for any questions.

PUBLICATIONS (under construction)Stratulat, S. (2008). Combining rewriting with Noetherian induction to reason on non-orientable equalities. In Voronkov, A., editor, Rewriting Techniques and Applications, volume 5117 of Lecture Notes in Computer Science, pages 351–365. Springer Berlin. Weiss, S., Urso, P. and Molli, P. (2008). A flexible undo framework for collaborative editing. Technical Report 6516, INRIA. Rouached, M., Fdhila, W., and Godart, C. (2008). A semantical framework to engineering wsbpel processes. Information Systems and E-Business Management. Rouached, M. (2008). Une approche rigoureuse pour l’ingénierie de compositions de services Web. PhD thesis, Université Henri Poincaré Nancy 1. Rouached, M. and Godart, C. (2007). Reasoning about events to specify authorization policies for web services composition. In ICWS, pages 481–488. IEEE Computer Society. Rouached, M. and Godart, C. (2007). Requirements-driven verification of WSBPEL processes. In ICWS, pages 354–363. IEEE Computer Society. Gaaloul, W., Bhiri, S., Hauswirth, M., Rouached, M., and Godart, C. (2007). Formal verification of composite service recovery mechanisms consistency. Collaborative Computing: Networking, Applications and Worksharing, pages 278–287. Gaaloul, W., Rouached, M., Godart, C., and Hauswirth, M. (2007). Verifying composite service transactional behavior using event calculus. In Meersman, R. and Tari, Z., editors, OTM Conferences (1), volume 4803 of Lecture Notes in Computer Science, pages 353–370. Springer. Imine, A. and Rusinowitch, M. (2007). Applying a theorem prover to the verification of optimistic replication algorithms. Rewriting, Computation and Proof, pages 213–234. Weiss, S., Urso, P., and Molli, P. (2007). Compensation in Collaborative Editing. International Workshop on Collaborative Editing Systems, Sanibel Island, USA, November. Molli, P. (2007) Cohérence des données dans les environnements d'édition collaboratifs. Habilitation à Diriger des Recherches, Nancy-Université. Rouached, M. and Godart, C. (2006). Analysis of composite web services using logging facilities. In Georgakopoulos, D., Ritter, N., Benatallah, B., Zirpins, C., Feuerlicht, G., Sch¨onherr, M., and Nezhad, H. R. M., editors, ICSOC Workshops, volume 4652 of Lecture Notes in Computer Science, pages 74–85. Springer. Imine, A. (2006). Conception Formelle d’Algorithmes de Replication Optimiste. Vers l’Edition Collaborative dans les Réseaux Pair-à-Pair. PhD thesis, Université Henri Poincaré - Nancy I, France. Oster, G., Urso, P., Molli, P., and Imine, A. (2006). Tombstone transformation functions for ensuring consistency in collaborative editing systems. In The Second International Conference on Collaborative Computing: Networking, Applications and Worksharing, Atlanta, Georgia, USA. IEEE Press. Imine, A., Rusinowitch, M., Oster, G., and Molli, P. (2006). Formal design and verification of operational transformation algorithms for copies convergence. Theoretical Computer Science, 351(2):167–183. Oster, G. (2005). Réplication Optimiste et Cohérence des Données dans les Environnements Collaboratifs Répartis. Thèse de doctorat, Université Henri Poincaré - Nancy I. Oster, G., Urso, P., Molli, P., and Imine, A. (2005). Proving correctness of transformation functions in collaborative editing systems. Technical Report RR-5795, INRIA. Imine, A., Molli, P., Oster, G., and Rusinovitch, M. (2005). Towards synchronizing linear collaborative objects with operation transformation. In FORTE 2005, number 3731 in LNCS, pages 411–427. Kaliszyk, C. (2005). Validation des preuves par récurrence implicite avec des outils basés sur le calcul des constructions inductives. Master’s thesis, Université Paul Verlaine - Metz. Stratulat, S. (2005). Automatic ’Descente Infinie’ induction reasoning. In Beckert, B., editor, TABLEAUX, volume 3702 of Lecture Notes in Computer Science, pages 262–276. Springer. Oster, G., Molli, P., Skaf-Molli, H., and Imine, A. (2004). Un modèle sûr et générique pour la synchronisation de données divergentes. In Premières Journées Francophones : Mobilité et Ubiquité, pages 98-106, Nice, France. Imine, A., Molli, P., Oster, G., and Rusinowitch, M. (2004). Deductive verification of distributed groupware systems. In Tenth International Conference on Algebraic Methodology and Software Technology - AMAST 2004, Stirling, Scotland, United Kingdom, volume 3116 of Lecture Notes in Computer Science. Springer. Molli, P., Oster, G., Skaf-Molli, H., and Imine, A. (2003). Safe generic data synchronizer. Research Report A03-R-062, LORIA – INRIA Lorraine. Molli, P., Oster, G., Skaf-Molli, H., and Imine, A. (2003). Using the transformational approach to build a safe and generic data synchronizer. In Proceedings of the ACM SIGGROUP Conference on Supporting Group Work - GROUP 2003, pages 212–220, Sanibel Island, Florida, USA. ACM Press. Imine, A., Molli, P., Oster, G., and Urso, P. (2003). Vote: Group editors analyzing tool. In International Workshop on First-Order Theorem Proving (FTP 2003), Valencia, Spain. Imine, A., Molli, P., Oster, G., and Rusinowitch, M. (2003). Proving correctness of transformation functions in real-time groupware. In Proceedings of the 8th European Conference on Computer - Supported Cooperative Work (ECSCW 2003), Helsinki, Finland. ACM. Rusinowitch, M., Stratulat, S., and Klay, F. (2003). Mechanical verification of an ideal incremental ABR conformance algorithm. J. Autom. Reasoning, 30(2):53–177. Barthe, G. and Stratulat, S. (2003). Validation of the Javacard platform with implicit induction techniques. In Nieuwenhuis, R., editor, RTA, volume 2706 of Lecture Notes in Computer Science, pages 337–351. Springer. Molli, P., Oster, G., Rusinowitch, M., and Imine, A. (2002). Development of transformation functions assisted by theorem prover. In The Fourth International Workshop on Collaborative Editing, ACM CSCW 2002, New Orleans, Louisiana, USA. Imine, A., Slimani, Y. and Stratulat, S. (2002) Using Automated Induction-based Theorem Provers for Reasoning about Concurrent Systems. In Programmation en logique avec contraintes, JFPLC 2002, 27-30 Mai 2002, Université de Nice Sophia-Antipolis, France., pages 71-85. Imine, A., Slimani, Y. and Stratulat, S (2002) Inductive Theorem Prover Based Verification of Concurrent Algorithms. In MCSEAI02 (7th Maghrebian Conference on Computer Science)., pages 313-324. Armando, A., Rusinowitch, M., and Stratulat, S. (2002). Incorporating decision procedures in implicit induction. J. Symb. Comput., 34(4):241–258. Stratulat, S. (2001) A General Framework to Build Contextual Cover Set Induction Provers. Journal of Symbolic Computation, 32(4):403-445. Stratulat, S. (2000) Preuves par récurrence avec ensembles couvrants contextuels. Applications à la vérification de logiciels de télécommunications. PhD thesis, Université Henri Poincaré, Nancy I. SOME OLDER BUT INTERESTING PUBLICATIONSA. Bouhoula (1997) Automated Theorem Proving by Test Set Induction. J. Symb. Comput., 23(1):47-77. A. Bouhoula and M. Rusinowitch (1995) SPIKE: A System for Automatic Inductive Proofs. In Algebraic Methodology and Software Technology, 4th International Conference, AMAST '95, Montreal, Canada, July 3-7, 1995, Springer, pages 576-577. A. Bouhoula, E. Kounalis and M. Rusinowitch (1995) Automated Mathematical Induction. J. Log. Comput., 5(5):631-668.

Tags

  spike

Share