| 2024 | LPAR | Certification of Tail Recursive Bubble-Sort in Theorema and Coq. | Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat |
| 2020 | SYNASC | SPIKE, an automatic theorem prover - revisited. | Sorin Stratulat |
| 2017 | TABLEAUX | Cyclic Proofs with Ordering Constraints. | Sorin Stratulat |
| 2016 | LATA | Proof-Based Synthesis of Sorting Algorithms for Trees. | Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat |
| 2016 | SACI | A case study on algorithm discovery from proofs: The insert function on binary trees. | Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat |
| 2016 | SYNASC | Structural vs. Cyclic Induction: A Report on Some Experiments with Coq. | Sorin Stratulat |
| 2015 | SISY | Theory exploration of binary trees. | Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat |
| 2015 | SYNASC | Combinatorial Techniques for Proof-Based Synthesis of Sorting Algorithms. | Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat |
| 2014 | PPDP | Decision Procedures for Proving Inductive Theorems without Induction. | Takahito Aoto, Sorin Stratulat |
| 2014 | SYNASC | Implementing Reasoning Modules in Implicit Induction Theorem Provers. | Sorin Stratulat |
| 2011 | CPP | Automated Certification of Implicit Induction Proofs. | Sorin Stratulat, Vincent Demange |
| 2010 | IFM | Integrating Implicit Induction Proofs into Certified Proof Environments. | Sorin Stratulat |
| 2007 | SYNASC | 'Descente Infinie' Induction-Based Saturation Procedures. | Sorin Stratulat |
| 2005 | TABLEAUX | Automatic 'Descente Infinie' Induction Reasoning. | Sorin Stratulat |
| 2000 | CAV | Mechanical Verification of an Ideal Incremental | Michal Rusinowitch, Sorin Stratulat, Francis Klay |
| 1994 | ICLP | Logic, Prolog, and Legal Sentence. | Cornell Popa, Yonut Lopatan, Sorin Stratulat |