Comparing several GCD algorithms. - Tudor Jebelean (IEEE Symposium on Computer Arithmetic, 1993)

Systolic normalization of rational numbers. - Tudor Jebelean (ASAP, 1993)

Improving the Multiprecision Euclidian Algorithm. - Tudor Jebelean (DISCO, 1993)

A Generalization of the Binary GCD Algorithm. - Tudor Jebelean (ISSAC, 1993)

An Algorithm for Exact Division. - Tudor Jebelean (J. Symb. Comput., 1993)

Designing systolic arrays for integer GCD computation. - Tudor Jebelean (ASAP, 1994)

Systolic Algorithms for Long Integer GCD Computation. - Tudor Jebelean (CONPAR, 1994)

Implementing GCD Systolic Arrays on FPGA. - Tudor Jebelean (FPL, 1994)

Design of a systolic coprocessor for rational addition. - Tudor Jebelean (ASAP, 1995)

FPGA Implementation of a Rational Adder. - Tudor Jebelean (FPL, 1995)

A Double-Digit Lehmer-Euclid Algorithm for Finding the GCD of Long Integers. - Tudor Jebelean (J. Symb. Comput., 1995)

Integer and Rational Arithmetic on MasPar. - Tudor Jebelean (DISCO, 1996)

Bidirectional Exact Integer Division. - Werner Krandick; Tudor Jebelean (J. Symb. Comput., 1996)

Using the Parallel Karatsuba Algorithm for Long Integer Multiplication and Division. - Tudor Jebelean (Euro-Par, 1997)

Auto-configurable array for GCD computation. - Tudor Jebelean (FPL, 1997)

A Survey of the Theorema Project. - Bruno Buchberger; Tudor Jebelean; Franz Kriftner; Mircea Marin; Elena Tomuta; Daniela Vasaru (ISSAC, 1997)

Practical Integer Division with Karatsuba Complexity. - Tudor Jebelean (ISSAC, 1997)

Preface. - Alessandro Armando; Tudor Jebelean (Calculemus, 1999)

FPGA Implementation of an Extended Binary GCD Algorithm for Systolic Reduction of Rational Numbers. - Bogdan Matasaru; Tudor Jebelean (FPL, 2000)

Special Issue on Calculemus-99: Integrating Computation and Deduction - Foreword of the Guest Editors. - Alessandro Armando; Tudor Jebelean (J. Symb. Comput., 2001)

Experimental Program Verification in the Theorema System. - Tudor Jebelean; Laura Kovács; Nikolaj Popov (ISoLA (Preliminary proceedings), 2004)

Functional-Based Synthesis of Systolic Online Multipliers. - Tudor Jebelean; Laura Szakacs (SYNASC, 2005)

An Algorithm for Automated Generation of Invariants for Loops with Conditionals. - Laura Ildikó Kovács; Tudor Jebelean (SYNASC, 2005)

Functional-Based Synthesis of a Systolic Array for GCD Computation. - Laura Ruff; Tudor Jebelean (IFL, 2006)

Combining Logic and Algebraic Techniques for Program Verification in Theorema. - Laura Kovács; Nikolaj Popov; Tudor Jebelean (ISoLA, 2006)

Theorema: Towards computer-aided mathematical theory exploration. - Bruno Buchberger; Adrian Craciun; Tudor Jebelean; Laura Kovács; Temur Kutsia; Koji Nakagawa; Florina Piroi; Nikolaj Popov; Judit Robu; Markus Rosenkranz; Wolfgang Windsteiger (J. Appl. Log., 2006)

Multi-Domain Logic and its Applications to SAT. - Tudor Jebelean; Gábor Kusper (SYNASC, 2008)

Automated Reasoning. - Tudor Jebelean; Bruno Buchberger; Temur Kutsia; Nikolaj Popov; Wolfgang Schreiner; Wolfgang Windsteiger (Hagenberg Research, 2009)

A Calculus for Imperative Programs: Formalization and Implementation. - Madalina Erascu; Tudor Jebelean (SYNASC, 2009)

Using Computer Algebra techniques for the specification, verification and synthesis of recursive programs. - Nikolaj Popov; Tudor Jebelean (Math. Comput. Simul., 2009)

Combining logical and algebraic techniques for natural style proving in elementary analysis. - Róbert Vajda; Tudor Jebelean; Bruno Buchberger (Math. Comput. Simul., 2009)

A Purely Logical Approach to the Termination of Imperative Loops. - Madalina Erascu; Tudor Jebelean (SYNASC, 2010)

Proving Partial Correctness and Termination of Mutually Recursive Programs. - Nikolaj Popov; Tudor Jebelean (SYNASC, 2010)

Proof Techniques for Synthesis of Sorting Algorithms. - Isabela Dramnesc; Tudor Jebelean (SYNASC, 2011)

Theory Exploration in Theorema: Case Study on Lists. - Isabela Dramnesc; Tudor Jebelean (SACI, 2012)

Discovery of inductive algorithms through automated reasoning: A case study on sorting. - Isabela Dramnesc; Tudor Jebelean (SISY, 2012)

Automated Synthesis of Some Algorithms on Finite Sets. - Isabela Dramnesc; Tudor Jebelean (SYNASC, 2012)

Soundness of a Logic-Based Verification Method for Imperative Loops. - Madalina Erascu; Tudor Jebelean (SYNASC, 2012)

Theory exploration of sets represented as monotone lists. - Isabela Dramnesc; Tudor Jebelean (SISY, 2014)

A case study in proof based synthesis of algorithms on monotone lists. - Isabela Dramnesc; Tudor Jebelean (SACI, 2015)

Theory exploration of binary trees. - Isabela Dramnesc; Tudor Jebelean; Sorin Stratulat (SISY, 2015)

Combinatorial Techniques for Proof-Based Synthesis of Sorting Algorithms. - Isabela Dramnesc; Tudor Jebelean; Sorin Stratulat (SYNASC, 2015)

Synthesis of list algorithms by mechanical proving. - Isabela Dramnesc; Tudor Jebelean (J. Symb. Comput., 2015)

Proof-Based Synthesis of Sorting Algorithms for Trees. - Isabela Dramnesc; Tudor Jebelean; Sorin Stratulat (LATA, 2016)

A case study on algorithm discovery from proofs: The insert function on binary trees. - Isabela Dramnesc; Tudor Jebelean; Sorin Stratulat (SACI, 2016)

Theorema 2.0: Computer-Assisted Natural-Style Mathematics. - Bruno Buchberger; Tudor Jebelean; Temur Kutsia; Alexander Maletzky; Wolfgang Windsteiger (J. Formaliz. Reason., 2016)

Special Issue on Program Verification, Automated Debugging and Symbolic Computation. - Tudor Jebelean; Wei Li 022; Dongming Wang 001 (J. Symb. Comput., 2017)

Techniques for natural-style proofs in elementary analysis. - Tudor Jebelean (ACM Commun. Comput. Algebra, 2018)

Automatic Synthesis of Merging and Inserting Algorithms on Binary Trees Using Multisets in Theorema. - Isabela Dramnesc; Tudor Jebelean (MACIS, 2019)

Case Studies on Algorithm Discovery from Proofs: The Delete Function on Lists and Binary Trees using Multisets. - Isabela Dramnesc; Tudor Jebelean (SISY, 2019)

Proof-Based Synthesis of Sorting Algorithms Using Multisets in Theorema. - Isabela Dramnesc; Tudor Jebelean (FROM, 2019)

Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques. - Isabela Dramnesc; Tudor Jebelean; Sorin Stratulat (J. Symb. Comput., 2019)

Deductive Synthesis of Min-Max-Sort Using Multisets in Theorema. - Isabela Dramnesc; Tudor Jebelean (SACI, 2020)

AlCons : Deductive Synthesis of Sorting Algorithms in Theorema. - Isabela Dramnesc; Tudor Jebelean (ICTAC, 2021)

A Heuristic Prover for Elementary Analysis in Theorema. - Tudor Jebelean (CICM, 2021)

Synthesis of Merging algorithms on binary trees using multisets in Theorema. - Isabela Dramnesc; Tudor Jebelean (SACI, 2021)

Synthesis of sorting algorithms using multisets in Theorema. - Isabela Dramnesc; Tudor Jebelean (J. Log. Algebraic Methods Program., 2021)

Experiments with Automated Reasoning in the Class. - Isabela Dramnesc; Erika Ábrahám; Tudor Jebelean; Gábor Kusper; Sorin Stratulat (CICM, 2022)

Mechanical Verification of Insert-Sort and Merge-Sort Using Multisets in Theorema. - Isabela Dramnesc; Tudor Jebelean (SISY, 2023)

Certification of Tail Recursive Bubble-Sort in Theorema and Coq. - Isabela Dramnesc; Tudor Jebelean; Sorin Stratulat (LPAR Complementary Volume, 2024)

A Natural-style Prover in Theorema Using Sequent Calculus with Unit Propagation. - Tudor Jebelean (LPAR Complementary Volume, 2024)

Certification of Sorting Algorithms Using Theorema and Coq. - Isabela Dramnesc; Tudor Jebelean; Sorin Stratulat (SCSS, 2024)

A European Project on AI-based Robotics. - Isabela Dramnesc; Erika Ábrahám; Tudor Jebelean; Nikolaos Fachantidis; Gábor Kusper; Sorin Stratulat (TALE, 2024)