Skip to content

Home

Jump to bottom
sorinica edited this page Sep 13, 2021 · 15 revisions

The SPIKE Prover

SPIKE is an automated theorem prover using (first-order) formula-based Noetherian induction. It is written in Objective Caml.

SPIKE can be called from the Coq proof assistant using a tactic that automatically performs lazy and mutual induction. We provide a zip file with the Coq scripts using this tactic.

CONTACT

SPIKE is currently developed by Sorin Stratulat. A previous version has been done by Adel Bouhoula and Michaël Rusinowitch.

You can contact Sorin for any questions.

MANUAL (under construction)

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.

  • Stratulat, S. (2020). SPIKE, an automatic theorem prover - revisited. SYNASC 2020: Proceedings of the 22th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing. IEEE press, pages 93-96.
  • Stratulat, S. (2017). Mechanically certifying formula-based Noetherian induction reasoning. J. Symb. Comput., 80(Part 1):209-249.
  • Stratulat, S. (2014). Implementing reasoning modules in implicit induction theorem provers. In SYNASC 2014: Proceedings of the 16th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing. IEEE press, pages 133-140.
  • Aoto, T. and Stratulat, S. (2014). Decision procedures for proving inductive theorems without induction. In Proc. of the 16th International Symposium on Principles and Practice of Declarative Programming (PPDP 2014). ACM press, pages 237–248.
  • Henaien, A. and Stratulat, S. (2013) Performing Implicit Induction Reasoning with Certifying Proof Environments. SCSS 2013 (4th International Symposium on Symbolic Computation in Software Science), volume 122 of Electronic Proceedings in Theoretical Computer Science, pages 97-108.
  • Stratulat, S. (2012) A Unified View of Induction Reasoning for First-Order Logic. In Turing-100 (The Alan Turing Centenary Conference), volume 10 of EPiC Series, pages 326-352. (received one of the 'Best Paper' awards)
  • Stratulat, S. and Demange, V. (2011) Automated Certification of Implicit Induction Proofs. In CPP'2011 (First International Conference on Certified Programs and Proofs), volume 7086 of LNCS, pages 37-53. Springer.
  • Stratulat, S. and Demange, V. (2010) Validating Implicit Induction Proofs Using Certified Proof Environments. Poster Session. 2010 Grande Region Security and Reliability Day, Saarbruck.
  • 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 PUBLICATIONS BEFORE 2000

  • A. 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.
Clone this wiki locally