Sorin Stratulat

, 2021

2020

SPIKE, an automatic theorem prover - revisited.

[BibT_eX]

[DOI]

Proceedings of the 22nd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2020

2019

Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques.

[BibT_eX]

[DOI]

J. Symb. Comput., 2019

2018

Validating Back-links of FOLID Cyclic Pre-proofs.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Seventh International Workshop on Classical Logic and Computation, 2018

2017

Mechanically certifying formula-based Noetherian induction reasoning.

[BibT_eX]

[DOI]

J. Symb. Comput., 2017

Cyclic Proofs with Ordering Constraints.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2017

2016

Structural vs. Cyclic Induction: A Report on Some Experiments with Coq.

[BibT_eX]

[DOI]

Proceedings of the 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2016

A case study on algorithm discovery from proofs: The insert function on binary trees.

[BibT_eX]

[DOI]

Proceedings of the 11th IEEE International Symposium on Applied Computational Intelligence and Informatics, 2016

Proof-Based Synthesis of Sorting Algorithms for Trees.

[BibT_eX]

[DOI]

Proceedings of the Language and Automata Theory and Applications, 2016

2015

Combinatorial Techniques for Proof-Based Synthesis of Sorting Algorithms.

[BibT_eX]

[DOI]

Proceedings of the 17th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2015

Theory exploration of binary trees.

[BibT_eX]

[DOI]

Proceedings of the 13th IEEE International Symposium on Intelligent Systems and Informatics, 2015

Better Careers for Transnational European Students? - A Case Study for French-German Diploma Alumni.

[BibT_eX]

[DOI]

Gabriel Michel

Véronique Jeanclaude

Proceedings of the International Joint Conference, 2015

2014

Implementing Reasoning Modules in Implicit Induction Theorem Provers.

[BibT_eX]

[DOI]

Proceedings of the 16th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2014

Decision Procedures for Proving Inductive Theorems without Induction.

[BibT_eX]

[DOI]

Takahito Aoto

Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming, 2014

2012

Performing Implicit Induction Reasoning with Certifying Proof Environments.

[BibT_eX]

[DOI]

Amira Henaien

Proceedings of the Proceedings Fourth International Symposium on Symbolic Computation in Software Science, 2012

A Unified View of Induction Reasoning for First-Order Logic.

[BibT_eX]

[DOI]

Proceedings of the Turing-100, 2012

2011

Automated Certification of Implicit Induction Proofs.

[BibT_eX]

[DOI]

Vincent Demange

Proceedings of the Certified Programs and Proofs - First International Conference, 2011

2010

Integrating Implicit Induction Proofs into Certified Proof Environments.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods - 8th International Conference, 2010

2008

Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 19th International Conference, 2008

2007

'Descente Infinie' Induction-Based Saturation Procedures.

[BibT_eX]

[DOI]

Proceedings of the Ninth International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2007

2005

Automatic 'Descente Infinie' Induction Reasoning.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2005

2003

Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm.

[BibT_eX]

[DOI]

Michaël Rusinowitch

Francis Klay

J. Autom. Reason., 2003

Validation of the JavaCard Platform with Implicit Induction Techniques.

[BibT_eX]

[DOI]

Gilles Barthe

Proceedings of the Rewriting Techniques and Applications, 14th International Conference, 2003

2002

Incorporating Decision Procedures in Implicit Induction.

[BibT_eX]

[DOI]

Alessandro Armando

Michaël Rusinowitch

J. Symb. Comput., 2002

Using Automated Induxtion-based Theorem Provers for Reasoning about Concurrent Systems.

[BibT_eX]

Abdessamad Imine

Yahya Slimani

Proceedings of the Programmation en logique avec contraintes, 2002

2001

A General Framework to Build Contextual Cover Set Induction Provers.

[BibT_eX]

[DOI]

J. Symb. Comput., 2001

2000

Preuves par récurrence avec ensembles couvrants contextuels. Application à la vérification de logiciels de télécommunications.

[BibT_eX]

[DOI]

PhD thesis, 2000

Mechanical Verification of an Ideal Incremental <i>ABR</i> Conformance.

[BibT_eX]

[DOI]

Michaël Rusinowitch

Francis Klay

Proceedings of the Computer Aided Verification, 12th International Conference, 2000

1995

Virtual Shared Memory Machines - an Application of PVM.

[BibT_eX]

[DOI]

David J. Evans

Parallel Algorithms Appl., 1995

1994

Logic, Prolog, and Legal Sentence.

[BibT_eX]

Cornell Popa

Yonut Lopatan