| 2024 | LPAR | Certification of Tail Recursive Bubble-Sort in Theorema and Coq. | Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat |
| 2024 | LPAR | A Natural-style Prover in Theorema Using Sequent Calculus with Unit Propagation. | Tudor Jebelean |
| 2023 | SISY | Mechanical Verification of Insert-Sort and Merge-Sort Using Multisets in Theorema. | Isabela Dramnesc, Tudor Jebelean |
| 2021 | ICTAC | AlCons : Deductive Synthesis of Sorting Algorithms in Theorema. | Isabela Dramnesc, Tudor Jebelean |
| 2021 | SACI | Synthesis of Merging algorithms on binary trees using multisets in Theorema. | Isabela Dramnesc, Tudor Jebelean |
| 2020 | SACI | Deductive Synthesis of Min-Max-Sort Using Multisets in Theorema. | Isabela Dramnesc, Tudor Jebelean |
| 2019 | SISY | Case Studies on Algorithm Discovery from Proofs: The Delete Function on Lists and Binary Trees using Multisets. | Isabela Dramnesc, Tudor Jebelean |
| 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 |
| 2015 | SACI | A case study in proof based synthesis of algorithms on monotone lists. | Isabela Dramnesc, Tudor Jebelean |
| 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 | SISY | Theory exploration of sets represented as monotone lists. | Isabela Dramnesc, Tudor Jebelean |
| 2012 | SACI | Theory Exploration in Theorema: Case Study on Lists. | Isabela Dramnesc, Tudor Jebelean |
| 2012 | SISY | Discovery of inductive algorithms through automated reasoning: A case study on sorting. | Isabela Dramnesc, Tudor Jebelean |
| 2012 | SYNASC | Automated Synthesis of Some Algorithms on Finite Sets. | Isabela Dramnesc, Tudor Jebelean |
| 2012 | SYNASC | Soundness of a Logic-Based Verification Method for Imperative Loops. | Madalina Erascu, Tudor Jebelean |
| 2011 | SYNASC | Proof Techniques for Synthesis of Sorting Algorithms. | Isabela Dramnesc, Tudor Jebelean |
| 2010 | SYNASC | A Purely Logical Approach to the Termination of Imperative Loops. | Madalina Erascu, Tudor Jebelean |
| 2010 | SYNASC | Proving Partial Correctness and Termination of Mutually Recursive Programs. | Nikolaj Popov, Tudor Jebelean |
| 2009 | SYNASC | A Calculus for Imperative Programs: Formalization and Implementation. | Madalina Erascu, Tudor Jebelean |
| 2008 | SYNASC | Multi-Domain Logic and its Applications to SAT. | Tudor Jebelean, Gbor Kusper |
| 2006 | ISoLA | Combining Logic and Algebraic Techniques for Program Verification in Theorema. | Laura Kovcs, Nikolaj Popov, Tudor Jebelean |
| 2005 | SYNASC | Functional-Based Synthesis of Systolic Online Multipliers. | Tudor Jebelean, Laura Szakacs |
| 2005 | SYNASC | An Algorithm for Automated Generation of Invariants for Loops with Conditionals. | Laura Ildik Kovcs, Tudor Jebelean |
| 2004 | ISoLA | Experimental Program Verification in the Theorema System. | Tudor Jebelean, Laura Kovcs, Nikolaj Popov |
| 2000 | FPL | FPGA Implementation of an Extended Binary GCD Algorithm for Systolic Reduction of Rational Numbers. | Bogdan Matasaru, Tudor Jebelean |
| 1997 | EuroPar | Using the Parallel Karatsuba Algorithm for Long Integer Multiplication and Division. | Tudor Jebelean |
| 1997 | FPL | Auto-configurable array for GCD computation. | Tudor Jebelean |
| 1997 | ISSAC | A Survey of the Theorema Project. | Bruno Buchberger, Tudor Jebelean, Franz Kriftner, Mircea Marin, Elena Tomuta, Daniela Vasaru |
| 1997 | ISSAC | Practical Integer Division with Karatsuba Complexity. | Tudor Jebelean |
| 1995 | FPL | FPGA Implementation of a Rational Adder. | Tudor Jebelean |
| 1994 | FPL | Implementing GCD Systolic Arrays on FPGA. | Tudor Jebelean |
| 1993 | ARITH | Comparing several GCD algorithms. | Tudor Jebelean |
| 1993 | ISSAC | A Generalization of the Binary GCD Algorithm. | Tudor Jebelean |