Tudor Jebelean

Proceedings of the Symbolic Computation in Software Science - 10th International Symposium, 2024

A Natural-style Prover in Theorema Using Sequent Calculus with Unit Propagation.

[BibT_eX]

[DOI]

Proceedings of the LPAR 2024 Complementary Volume, Port Louis, Mauritius, May 26-31, 2024, 2024

Certification of Tail Recursive Bubble-Sort in Theorema and Coq.

[BibT_eX]

[DOI]

Proceedings of the LPAR 2024 Complementary Volume, Port Louis, Mauritius, May 26-31, 2024, 2024

2023

Mechanical Verification of Insert-Sort and Merge-Sort Using Multisets in Theorema.

[BibT_eX]

[DOI]

Proceedings of the 21st IEEE Jubilee International Symposium on Intelligent Systems and Informatics, 2023

2022

Experiments with Automated Reasoning in the Class.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - 15th International Conference, 2022

2021

Synthesis of sorting algorithms using multisets in <i>Theorema</i>.

[BibT_eX]

[DOI]

J. Log. Algebraic Methods Program., 2021

Synthesis of Merging algorithms on binary trees using multisets in Theorema.

[BibT_eX]

[DOI]

Proceedings of the 15th IEEE International Symposium on Applied Computational Intelligence and Informatics, 2021

A Heuristic Prover for Elementary Analysis in Theorema.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - 14th International Conference, 2021

AlCons : Deductive Synthesis of Sorting Algorithms in Theorema.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing - ICTAC 2021, 2021

2020

Deductive Synthesis of Min-Max-Sort Using Multisets in Theorema.

[BibT_eX]

[DOI]

Proceedings of the 14th IEEE International Symposium on Applied Computational Intelligence and Informatics, 2020

2019

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

[BibT_eX]

[DOI]

J. Symb. Comput., 2019

Proof-Based Synthesis of Sorting Algorithms Using Multisets in Theorema.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Third Symposium on Working Formal Methods, 2019

Case Studies on Algorithm Discovery from Proofs: The Delete Function on Lists and Binary Trees using Multisets.

[BibT_eX]

[DOI]

Proceedings of the 17th IEEE International Symposium on Intelligent Systems and Informatics, 2019

Automatic Synthesis of Merging and Inserting Algorithms on Binary Trees Using Multisets in Theorema.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Aspects of Computer and Information Sciences, 2019

2018

Techniques for natural-style proofs in elementary analysis.

[BibT_eX]

[DOI]

ACM Commun. Comput. Algebra, 2018

2017

Special Issue on Program Verification, Automated Debugging and Symbolic Computation.

[BibT_eX]

[DOI]

Wei Li

Dongming Wang

J. Symb. Comput., 2017

2016

Theorema 2.0: Computer-Assisted Natural-Style Mathematics.

[BibT_eX]

[DOI]

J. Formaliz. Reason., 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

Synthesis of list algorithms by mechanical proving.

[BibT_eX]

[DOI]

J. Symb. Comput., 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

A case study in proof based synthesis of algorithms on monotone lists.

[BibT_eX]

[DOI]

Proceedings of the 10th IEEE Jubilee International Symposium on Applied Computational Intelligence and Informatics, 2015

2014

Theory exploration of sets represented as monotone lists.

[BibT_eX]

[DOI]

Proceedings of the IEEE 12th International Symposium on Intelligent Systems and Informatics, 2014

2012

Soundness of a Logic-Based Verification Method for Imperative Loops.

[BibT_eX]

[DOI]

Madalina Erascu

Proceedings of the 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2012

Automated Synthesis of Some Algorithms on Finite Sets.

[BibT_eX]

[DOI]

Proceedings of the 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2012

Discovery of inductive algorithms through automated reasoning: A case study on sorting.

[BibT_eX]

[DOI]

Proceedings of the 10th IEEE Jubilee International Symposium on Intelligent Systems and Informatics, 2012

Theory Exploration in Theorema: Case Study on Lists.

[BibT_eX]

[DOI]

Proceedings of the 7th IEEE International Symposium on Applied Computational Intelligence and Informatics, 2012

2011

Proof Techniques for Synthesis of Sorting Algorithms.

[BibT_eX]

[DOI]

Proceedings of the 13th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2011

2010

Proving Partial Correctness and Termination of Mutually Recursive Programs.

[BibT_eX]

[DOI]

Proceedings of the 12th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2010

A Purely Logical Approach to the Termination of Imperative Loops.

[BibT_eX]

[DOI]

Madalina Erascu

Proceedings of the 12th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2010

2009

Combining logical and algebraic techniques for natural style proving in elementary analysis.

[BibT_eX]

[DOI]

Róbert Vajda

Bruno Buchberger

Math. Comput. Simul., 2009

Using Computer Algebra techniques for the specification, verification and synthesis of recursive programs.

[BibT_eX]

[DOI]

Math. Comput. Simul., 2009

A Calculus for Imperative Programs: Formalization and Implementation.

[BibT_eX]

[DOI]

Madalina Erascu

Proceedings of the 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2009

Automated Reasoning.

[BibT_eX]

[DOI]

Proceedings of the Hagenberg Research, 2009

2008

Multi-Domain Logic and its Applications to SAT.

[BibT_eX]

[DOI]

Gábor Kusper

Proceedings of the SYNASC 2008, 2008

2006

Theorema: Towards computer-aided mathematical theory exploration.

[BibT_eX]

[DOI]

J. Appl. Log., 2006

Combining Logic and Algebraic Techniques for Program Verification in Theorema.

[BibT_eX]

[DOI]

Laura Kovács

Proceedings of the Leveraging Applications of Formal Methods, 2006

Functional-Based Synthesis of a Systolic Array for GCD Computation.

[BibT_eX]

[DOI]

Laura Ruff

Proceedings of the Implementation and Application of Functional Languages, 2006

2005

An Algorithm for Automated Generation of Invariants for Loops with Conditionals.

[BibT_eX]

[DOI]

Laura Ildikó Kovács

Proceedings of the Seventh International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2005), 2005

Functional-Based Synthesis of Systolic Online Multipliers.

[BibT_eX]

[DOI]

Laura Szakacs

Proceedings of the Seventh International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2005), 2005

2004

Experimental Program Verification in the Theorema System.

[BibT_eX]

Laura Kovács

Proceedings of the International Symposium on Leveraging Applications of Formal Methods, 2004

2001

Special Issue on Calculemus-99: Integrating Computation and Deduction - Foreword of the Guest Editors.

[BibT_eX]

[DOI]

Alessandro Armando

J. Symb. Comput., 2001

2000

FPGA Implementation of an Extended Binary GCD Algorithm for Systolic Reduction of Rational Numbers.

[BibT_eX]

[DOI]

Bogdan Matasaru

Proceedings of the Field-Programmable Logic and Applications, 2000

1999

Preface.

[BibT_eX]

[DOI]

Alessandro Armando

Proceedings of the Systems for Integrated Computation and Deduction, 1999

1997

Practical Integer Division with Karatsuba Complexity.

[BibT_eX]

[DOI]

Proceedings of the 1997 International Symposium on Symbolic and Algebraic Computation, 1997

A Survey of the Theorema Project.

[BibT_eX]

[DOI]

Proceedings of the 1997 International Symposium on Symbolic and Algebraic Computation, 1997

Auto-configurable array for GCD computation.

[BibT_eX]

[DOI]

Proceedings of the Field-Programmable Logic and Applications, 7th International Workshop, 1997

Using the Parallel Karatsuba Algorithm for Long Integer Multiplication and Division.

[BibT_eX]

[DOI]

Proceedings of the Euro-Par '97 Parallel Processing, 1997

1996

Bidirectional Exact Integer Division.

[BibT_eX]

[DOI]

Werner Krandick

J. Symb. Comput., 1996

Integer and Rational Arithmetic on MasPar.

[BibT_eX]

[DOI]

Proceedings of the Design and Implementation of Symbolic Computation Systems, 1996

1995

A Double-Digit Lehmer-Euclid Algorithm for Finding the GCD of Long Integers.

[BibT_eX]

[DOI]

J. Symb. Comput., 1995

FPGA Implementation of a Rational Adder.

[BibT_eX]

[DOI]

Proceedings of the Field-Programmable Logic and Applications, 5th International Workshop, 1995

Design of a systolic coprocessor for rational addition.

[BibT_eX]

[DOI]

Proceedings of the International Conference on Application Specific Array Processors (ASAP'95), 1995

1994

Implementing GCD Systolic Arrays on FPGA.

[BibT_eX]

[DOI]

Proceedings of the Field-Programmable Logic, 1994

Systolic Algorithms for Long Integer GCD Computation.

[BibT_eX]

[DOI]

Proceedings of the Parallel Processing: CONPAR 94, 1994

Designing systolic arrays for integer GCD computation.

[BibT_eX]

[DOI]

Proceedings of the International Conference on Application Specific Array Processors, 1994

1993

An Algorithm for Exact Division.

[BibT_eX]

[DOI]

J. Symb. Comput., 1993

A Generalization of the Binary GCD Algorithm.

[BibT_eX]

[DOI]

Proceedings of the 1993 International Symposium on Symbolic and Algebraic Computation, 1993

Improving the Multiprecision Euclidian Algorithm.

[BibT_eX]

[DOI]

Proceedings of the Design and Implementation of Symbolic Computation Systems, 1993

Systolic normalization of rational numbers.

[BibT_eX]

[DOI]

Proceedings of the International Conference on Application-Specific Array Processors, 1993

Comparing several GCD algorithms.

[BibT_eX]

[DOI]