RISC Publications and Technical Reports of Tudor Jebelean
2021
Tudor Jebelean.A Heuristic Prover for Elementary Analysis in Theorema. Technical report no. 21-07 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).April2021.[doi][pdf][bib]
T. Jebelean.A Heuristic Prover for Elementary Analysis in Theorema. In: Intelligent Computer Mathematics, 14th International Conference, CICM 2021, Timisoara, Romania, F. Kamaredine, C. Sacerdoti Coen (ed.), Proceedings of Intelligent Computer Mathematics, 14th International Conference, CICM 2021, LNAI12833, pp. 130-134.July2021.Springer,978-3-030-81096-2.[pdf][bib]
I. Dramnesc, T. Jebelean.AlCons: Deductive Synthesis of Sorting Algorithms in Theorema. In: Theoretical Aspects of Computing - ICTAC 2021, A. Cerone, P. Csaba Ölveczky (ed.), Proceedings of 18th International Colloquium on Theoretical Aspects of Computing - ICTAC, Nur-Sultan, Kazakhstan, LNCS12819, pp. 314-333.September 2021.Springer,978-3-030-85315-0.[pdf][bib]
2020
Isabela Dramnesc, Tudor Jebelean.Implementation of Deletion Algorithms on Lists and Binary Trees in Theorema. Technical report no. 20-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).April2020.[pdf][bib]
Isabela Dramnesc, Tudor Jebelean.Synthesis of Delete on Lists and Binary Trees Using Multisets in Theorema. Technical report no. 20-15 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).September2020.[pdf][bib]
2018
T. Jebelean.Experiments with Automatic Proofs in Elementary Analysis. Technical report no. 18-06 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).April2018.Work in progress.[zip][pdf][pdf][bib]
Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat.Mechanical Synthesis of Sorting Algorithms for Binary Trees by Logic and Combinatorial Techniques.Journal of Symbolic Computation90, pp. 3-41.2018.Elsevier,07477171.[doi][bib]
2017
Tudor Jebelean, Nikolaj Popov.A Set-Based Approach to Qualitative and Quantitative Estimation of Competencies. Technical report no. 17-05 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).September2017.[pdf][bib]
E. Abraham, T. Jebelean.Adapting Cylindrical Algebraic Decomposition for Proof Specific Tasks. In: ICAI 2017: 10th International Conference on Applied Informatics, G. Kusper (ed.), Proceedings of ICAI 2017: 10th International Conference on Applied Informatics, pp. 0-0.2017.ISBN 0.In print.[url][pdf][bib]
2016
Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat.Proof-based Synthesis of Sorting Algorithms for Trees. In: Proceedings of LATA 2016, the 10th International Conference on Language and Automata Theory and Applications, Adrian-Horia Dediu, Jan Janousek, Carlos Martin-Vide, Bianca Truthe (ed.), Proceedings of LATA 2016, LNCS9618, pp. 562-575.2016.Springer,ISBN 978-3-319-29999-0.[bib]
Bruno Buchberger, Tudor Jebelean, Temur Kutsia, Alexander Maletzky, Wolfgang Windsteiger.Theorema 2.0: Computer-Assisted Natural-Style Mathematics.JFR9(1), pp. 149-185.2016.ISSN 1972-5787.[doi][bib]
Isabela Dramnesc and Tudor Jebelean, Sorin Stratulat.A case study on algorithm discovery from proofs: The insert function on binary trees. In: 11th IEEE International Symposium on Applied Computational Intelligence and Informatics, SACI 2016, Timisoara, Romania, May 12-14, 2016, IEEE (ed.), pp. 231-236.2016.978-1-5090-2380-6.[doi][bib]
2015
Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat.Combinatorial Techniques for Proof-based Synthesis of Sorting Algorithms. In: SYNASC 2015: Proceedings of the 17th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Laura Kovacs (ed.), pp. 137-144.2015.IEEE Computer Society,ISBN 978-0-7695-5742-2.[bib]
Isabela Dramnesc, Tudor Jebelean.Synthesis of list algorithms by mechanical proving.Journal of Symbolic Computation69, pp. 61-92.2015.ISSN 0747-7171.[bib]
Isabela Dramnesc, Tudor Jebelean and Sorin Stratulat.Synthesis of Some Algorithms for Trees: Experiments in Theorema. Technical report no. 15-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2015.[pdf][bib]
Isabela Dramnesc, Tudor Jebelean.A Case Study in Proof Based Synthesis of Algorithms on Monotone Lists. In: The 10th International Symposium on Applied Computational Intelligence and Informatics, . (ed.), Proceedings of SACI 2015, pp. 483-488.2015.IEEE Xplore,_.[bib]
Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat.Theory Exploration of Binary Trees. In: The IEEE 13th Jubilee International Symposium on Intelligent Systems and Informatics, . (ed.), Proceedings of SISY 2015, pp. 139-144.2015.IEEE Xplore,..[bib]
2014
Isabela Dramnesc, Tudor Jebelean.Theory Exploration of Sets Represented as Monotone Lists. In: Proceedings of SISY 2014 IEEE 12th International Symposium on Intelligent Systems and Informatics, IEEE Xplore (ed.), pp. 163-168.2014. ..[bib]
2012
Tudor Jebelean, Anna Medve.Formalization of Workflows Using Fork-Join Automata. Technical report no. 12-21 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December2012.[pdf][bib]
Isabela Dramnesc, Tudor Jebelean.Semi-automatic Synthesis of Some Sorting Programs in Theorema. Research Institute for Symbolic Computation (RISC), University of Linz. Technical report no. 12-01, Schloss Hagenberg, 4232 Hagenberg, Austria, January2012.RISC Report Series.[pdf][bib]
Isabela Dramnesc, Tudor Jebelean.Systematic Exploration of the Theory of Lists in Theorema. Technical report no. 12-02 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).January2012.RISC Report Series.[pdf][bib]
Isabela Dramnesc, Tudor Jebelean.Theory Exploration in Theorema: Case Study on Lists. In: Proceedings of the 7th IEEE International Symposium on Applied Computational Intelligence and Informatics, . (ed.), Proceedings of SACI 2012, pp. 421-426.May 24-262012.IEEE Xplore,Obuda University, Budapest, Hungary and "Politehnica" University of Timisoara, Romania,Print ISBN 978-1-4673-1013-0.[bib]
Isabela Dramnesc, Tudor Jebelean.Systematic Exploration of List Theory in Theorema.Scientific Bulletin of the "Politehnica" University of Timisoara, Transactions on Automatic Control and Computer Science(4/2012), pp. 203-210.2012.ISSN 1224-600X.[bib]
Isabela Dramnesc, Tudor Jebelean.Discovery of Inductive Algorithms through Automated Reasoning: A Case Study on Sorting. In: Proceedings of SISY 2012: the IEEE 10th Jubilee International Symposium on Intelligent Systems and Informatics, . (ed.), pp. 293-298.September2012.IEEE Xplore,ISBN 978-1-4673-4751-8.[url][bib]
Isabela Dramnesc, Tudor Jebelean.Automated Synthesis of Some Algorithms on Finite Sets. In: Proceedings of SYNASC 2012: the 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, . (ed.), pp. 143-151.September2012.IEEE Computer Society,ISBN-13: 978-0-7695-4934-7.[bib]
2011
N. Popov, T. Jebelean.Sound and Complete Verification Condition Generator for Functional Recursive Programs.. In: Numerical and Symbolic Scientific Computing: Progress and Prospects, U. Langer and P. Paule (ed.), pp. 219-256.2011.Springer,Wien,ISBN 978-3-7091-0793-5.[bib]
Tudor Jebelean, Gabor Kusper.SAT Solving Experiments in Multi-Domain Logic. In: ICAI 2001, Emod Kovacs (ed.)I, pp. 95-105.2011.Eger, Hungary,0.[bib]
Isabela Dramnesc, Tudor Jebelean.Automated Reasoning on Tuples - Case Studies in Proof Based Synthesis. Technical report no. 11-08 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).July2011.[pdf][bib]
Isabela Dramnesc, Tudor Jebelean .Proof Techniques for Synthesis of Sorting Algorithms. In: Proceedings of the 13th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, D. Wang, V. Negru, T. Ida, T. Jebelean, D. Petcu, S. Watt and D. Zaharie (ed.), pp. 101-109.September2011.IEEE Computer Society,ISBN 978-0-7695-4630-8.[url][pdf][bib]
2010
Tudor Jebelean, Gabor Kusper.Experiments with Multi-Domain Logic: Variable Merging and Split Strategies. Technical report no. 10-03 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).February2010.[pdf][bib]
Isabela Dramnesc, Tudor Jebelean and Adrian Craciun.Case Studies in Systematic Exploration of Tuple Theory. Technical report no. 10-09 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).May2010.[pdf][bib]
Madalina Erascu, Tudor Jebelean.A Purely Logical Approach to Program Termination. In: Proceedings of the 11th International Workshop on Termination, Peter Schneider-Kamp (ed.), Proceedings of Federated Logic Conference, Edinburgh, 9-21 July, pp. - .2010.[pdf][bib]
Madalina Erascu, Tudor Jebelean.A Purely Logical Approach to Imperative Program Verification. Technical report no. 10-07 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2010.[pdf][bib]
M. Erascu, T. Jebelean.A Purely Logical Approach to the Termination of Imperative Loops. In: Proceedings of the 12th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, T. Ida, V. Negru, T. Jebelean, D. Petcu, S. M. Watt, D. Zaharie (ed.), pp. 142-149.September2010.IEEE Computer Society, 978-0-7695-4324-6.[pdf][bib]
T. Jebelean, M. Mosbah, N. Popov (eds.).Proceedings of SCSS 2010 Symbolic Computation in Software Science. Technical report no. 10-10 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).August2010.[pdf][bib]
N. Popov, T. Jebelean, B. Buchberger.From Program Verification to Automated Debugging. In: Workshop on Symbolic Computation in Software Science, T. Jebelean and M. Mosbah and N. Popov (ed.), Proceedings of SCSS 2010, pp. 55-65.July2010.RISC-Linz Report Series,Johannes Kepler University of Linz, Austria,..[bib]
A. Anisimov, T. Jebelean, A. Lyaletski, N. Popov.Projects of Evidence Algorithm and Theorema. In: Theoretical and Applied Aspects of Program Systems Development, A. Anisimov, V. Redko (ed.), pp. 54-58.October2010.Kiev, Ukraine,..[bib]
N. Popov, T. Jebelean.Proving Partial Correctness and Termination of Mutually Recursive Programs. In: SYNASC 2010, T. Ida, V. Negru, T. Jebelean, D. Petcu, S. Watt, and, D. Zaharie (ed.), Proceedings of Symposium on Symbolic and Numeric Algorithms for Scientific Computing, pp. 153-158.September2010.IEEE ,ISBN 978-0-7695-4324-6.[pdf][bib]
Isabela Dramnesc, Tudor Jebelean.A Case Study in Proof Based Synthesis of Sorting Algorithms. In: Analele Universitatii de Vest, Timisoara, D.Gaspar, D.Zaharie, B.Buchberger, D.Burghelea, G.Cassier (ed.), Proceedings of 12th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2010), Matematica - InformaticaXLVIII/3, pp. 47-58.23-26 September2010.West University of Timisoara, Romania,ISSN-1841-3293.[pdf][bib]
Isabela Dramnesc, Tudor Jebelean, Adrian Craciun.A Case Study in Systematic Exploration of Tuple Theory. In: Workshop of Symbolic Computation in Software Science, Tudor Jebelean, Mohamed Mosbah, Nikolaj Popov (ed.), Proceedings of SCSS 2010 Symbolic Computation in Software Science, Hagenberg1/10-10, pp. 82-95.29-30 July2010.RISC-Linz Report Series,Johannes Kepler University of Linz, Austria,.[pdf][bib]
2009
Camelia Rosenkranz, Bruno Buchberger, Tudor Jebelean.Knowledge Archives in Theorema: A Logic-Internal Approach. Technical report no. 09-01 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).January2009.[ps][pdf][bib]
N. Popov, T. Jebelean.Using Computer Algebra Techniques for the Specification, Verification and Synthesis of Recursive Programs.Mathematics and Computers in Simulation79(8), pp. 2293-2301.April2009.Elsevier,ISSN: 0378-4754.[pdf][bib]
R. Vajda, T. Jebelean, B. Buchberger.Combining Logical and Algebraic Techniques for Natural Style Proving in Elementary Analysis.Mathematics and Computers in Simulation79(8), pp. 2310-2316.April2009.Elsevier,ISSN: 0378-4754.Special Issue on Nonstandard Applications of Computer Algebra.[url][pdf][bib]
Tudor Jebelean, Bruno Buchberger, Temur Kutsia, Nikolaj Popov, Wolfgang Schreiner, Wolfgang Windsteiger.Automated Reasoning. In: Hagenberg Research, B. Buchberger, M. Affenzeller, A. Ferscha, M. Haller, T. Jebelean, E.P. Klement, P. Paule, G. Pomberger, W. Schreiner, R. Stubenrauch, R. Wagner, G. Weiss, W. Windsteiger (ed.), pp. 63-101.2009.Springer Dordrecht Heidelberg London New York,ISBN 978-3-642-02126-8.[url][bib]
N. Popov, T. Jebelean.Verification of Mutual Recursive Functional Programs. In: Proceedings of Workshop on Symbolic Computation in Software Science SCSS'09, T. Ida, A. Bouhoula (ed.), pp. 120-122.September2009.Carthage, Tunisia,..[pdf][bib]
N. Popov, T. Jebelean.Functional Program Verification in Theorema. Soundness and Completeness. In: Proceedings of 15th Biennial Workshop on Programmiersprachen und Grundlagen der Programmierung KPS'09, J. Knoop, A. Prantl (ed.), pp. 221-229.October2009.Maria Taferl, Austria,..[pdf][bib]
N. Popov, T. Jebelean.A Complete Method for Algorithm Validation. In: Proceedings of the Workshop on Automated Mathematical Theory Exploration AUTOMATHEO'09, B. Buchberger, R. McCasland, A. Craciun (ed.), pp. 21-25.June2009.Hagenberg, Austria,-.[pdf][bib]
2008
N. Popov, T. Jebelean.A Prototype Environment for Verification of Recursive Programs. In: FORMED'08, Z. Istenes (ed.), Proceedings of Formal Methods in Computer Science Education, Budapest, Hungary, ENTCS, pp. 121-130.March2008.Elsevier,..[pdf][bib]
N. Popov, T. Jebelean.Verification of Functional Programs Containing Nested Recursion . In: SCSS'08, B. Buchberger, T. Ida and T. Kutsia (ed.), Proceedings of Austrian-Japan Workshop on Symbolic Computation in Software Science, Hagenberg, Austria, pp. 163-175.July2008...[pdf][bib]
Madalina Erascu, Tudor Jebelean.Practical Program Verification by Forward Symbolic Execution: Correctness and Examples. In: Austrian-Japan Workshop on Symbolic Computation in Software Science, Bruno Buchberger, Tetsuo Ida, Temur Kutsia (ed.)08-08, pp. 47-56.2008.RISC Report Series, University of Linz, Austria,[pdf][bib]
Camelia Rosenkranz, Bruno Buchberger, Tudor Jebelean.Mathematical Knowledge Archives in Theorema. Technical report no. 08-16 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).September2008.[pdf][bib]
Tudor Jebelean, Gabor Kusper.Multi-Domain Logic and its Applications to SAT. In: SYNASC 2008, V. Negru et. al. (ed.), Proceedings of International Simposium on Symbolic and Numeric Scientific Computation, pp. 3-8.2008.IEEE Society Press,978-0-7695-3523-4.[pdf][bib]
2007
N. Popov, T. Jebelean.Proving Termination of Recursive Programs by Matching Against Simplified Program Versions and Construction of Specialized Libraries in Theorema. In: Proceedings of 9-th International Workshop on Termination, D. Hofbauer, A. Serebrenik (ed.), pp. 48-52.June2007.Paris, France,ISSN-0935-3232.[pdf][bib]
M. Giese, T. Jebelean.Proc. Workshop on Invariant Generation, WING 2007. Technical report no. 07-07 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).062007.Workshop Proceedings.[pdf][bib]
M. Erascu, T. Jebelean.Verification of Imperative Programs using Symbolic Execution and Forward Reasoning in the Theorema System. RISC Linz. Technical report no. 07-12, July 12007.Presented at First Austria-Japan Workshop on Symbolic Computation and Software Verification, Linz, Austria, July 1st 2007.[pdf][bib]
Florina Piroi, Bruno Buchberger, Camelia Rosenkranz, Tudor Jebelean.Organisational Tools for MKM in Theorema. Technical report no. 07-11 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2007.[ps][bib]
L. Ruff, T. Jebelean.Functional Based Synthesis of a Systolic Array for GCD Computation. In: Implementation and Application of Functional Languages, Z. Horvath, V. Zsok (ed.), LNCS4449, pp. 37-54.2007.Springer,978-3-540-74129-9.[bib]
2006
B. Buchberger, A. Craciun, T. Jebelean, L. Kovacs, T. Kutsia, K. Nakagawa, F. Piroi, N. Popov, J. Robu, M. Rosenkranz, W. Windsteiger.Theorema: Towards Computer-Aided Mathematical Theory Exploration.Journal of Applied Logic4(4), pp. 470-504.2006.ISSN 1570-8683.[doi][pdf][bib]
T. Jebelean, L. Kovacs, N. Popov.Experimental Program Verification in the Theorema System.Int. Journal on Software Tools for Technology Transfer (STTT), pp. _-_.2006.Springer, ISSN: 1433-2779 (Paper) 1433-2787 (Online).in press.[pdf][bib]
L. Kovacs, T. Jebelean.Finding Polynomial Invariants for Imperative Loops in the Theorema System. Technical report no. 03-06 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2006.[pdf][bib]
L. Kovacs, T. Jebelean.Finding Polynomial Invariants for Imperative Loops in the Theorema System. In: Proceedings of Verify'06 Workshop, IJCAR'06, The 2006 Federated Logic Conference, S. Autexier and H. Mantel (ed.), pp. 52-67.August 15-162006.[url][pdf][bib]
L. Kovacs, N. Popov, T. Jebelean.Combining Logic and Algebraic Techniques for Program Verification in Theorema. In: Proceedings ISOLA 2006, T. Margaria, A. Philippou, B. Steffen (ed.), Proceedings of Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISOLA 2006), pp. 59-68.November2006.IEEE,Paphos, Cyprus,ISBN 978-0-7695-3071-0.[pdf][bib]
L. Kovacs, T. Jebelean, D. Kapur.Using Symbolic Summation and Polynomial Algebra for Imperative Program Verification in Theorema. RISC-Linz. Technical report, 2006.submitted to MatCom Journal.[pdf][bib]
2005
L. Kovacs, T. Jebelean, A. Kovacs.Practical Aspects of Algebraic Invariant Generation for Loops with Conditionals. In: Bulletins for Applied and Computer Mathematics, Pannonian Applied Mathematical Meetings, PC-147/148, F.Fazekas et al (ed.), pp. --.26-29 May2005.Technical University of Budapest, PAMM-Centre,Balatonalmadi, Hungary,-.[pdf][bib]
L. Kovacs, T. Jebelean.An Algorithm for Automated Generation of Invariants for Loops with Conditionals. In: Proceedings of the Computer-Aided Verification on Information Systems Workshop (CAVIS05), 7th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC05), D. Petcu et al (ed.), pp. 16-19.September 25-282005.Department of Computer Science, West University of Timisoara, Romania,-.to appear in IEEE journal.[pdf][bib]
L. Kovacs, N. Popov, T. Jebelean.Verification Environment in Theorema.Annals of Mathematics, Computing and Teleinformatics (AMCT)1(2), pp. 27-34.2005.ISSN 1109-9305.[url][pdf][bib]
Tudor Jebelean, Laura Szakacs.Functional-Based Synthesis of Systolic Online Multipliers. In: SYNASC-05 (International Symposium on Symbolic and Numeric Scientific Computing), D. Zaharie, D. Petcu, V. Negru, T. Jebelean, G. Ciobanu, A. Cicortas, A. Abraham, M. Paprzycki (ed.), Proceedings of SYNASC-05, pp. 267-275.2005.IEEE Computer Society,ISBN 0-7695-2453-2.[pdf][bib]
2004
L. Kovacs, T. Jebelean.Automated Generation of Loop Invariants by Recurrence Solving in Theorema. In: Proc. of the 6th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC04), D. Petcu and V. Negru and D. Zaharie and T. Jebelean (ed.), pp. 451-464.26-30 September2004.Mirton Publisher,Timisoara, Romania,ISBN 973-661-441-7.[pdf][bib]
L. Kovacs, T. Jebelean.Generation of Loop Invariants in Theorema by Combinatorial and Algebraic Methods. In: Bulletins for Applied and Computer Mathematics, Pannonian Applied Mathematical Meetings, PC-144, F. Fazekas et al (ed.) vol. CVI/2172, pp. 125-134.20-23 May2004.Technical University of Budapest, PAMM-Centre,Balatonalmadi, Hungary,ISSN 0133-3526.[pdf][bib]
Nikolaj Popov, Tudor Jebelean.Verification of Simple Recursive Programs: Sufficient Conditions. Technical report no. 04-06 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).June2004.[pdf][ps][ps][bib]
N. Popov, T. Jebelean.A Practical Approach to Proving Termination of Recursive Programs in Theorema. In: Proceedings of 7th International Workshop on Termination, M. Codish, A. Middeldorp (ed.), pp. 43-46.June2004.Aachen, Germany,ISSN-0935-3232.[pdf][bib]
T. Jebelean, L. Kovacs, N. Popov.Experimental Program Verification in the Theorema System. In: Proceedings ISOLA 2004, T. Margaria, B. Steffen (ed.), Proceedings of International Symposium on Leveraging Applications of Formal Methods ISOLA 2004, pp. 92-99.November2004.Paphos, Cyprus,University of Cyprus,[pdf][ps][bib]
L. Kovacs, T. Jebelean.Automated Generation of Loop Invariants by Recurrence Solving in Theorema.Analele Universitatii din Timisoara, Seria Matematica - InformaticaXLII, pp. 151-166.2004.Mirton Publisher,Timisoara, Romania,ISSN 1224-970X.special issue on Computer Science - Proceedings of SYNASC'04.[pdf][bib]
2003
L. Kovacs, T. Jebelean.Practical Aspects of Imperative Program Verification in Theorema.Analele Universitatii din Timisoara, Seria Matematica - InformaticaXLI, pp. 135-154.2003.Mirton Publisher,Timisoara, Romania,ISSN 1224-970X.special issue on Computer Science - Proceedings of SYNASC'03.[pdf][bib]
L. Kovacs, T. Jebelean.Practical Aspects of Imperative Program Verification in Theorema. In: Proceedings of SYNASC 2003, 5th International Workshop on Symbolic and Numeric Algorithms for Scientific Computing Timisoara, D. Petcu, V. Negru, D. Zaharie, T. Jebelean (ed.), pp. 317-320.1-4 October2003.Mirton Publisher,Timisoara, Romania,ISBN: 973-661-104-3.[pdf][bib]
L. Kovacs, T. Jebelean, N. Popov.Verification of Imperative Programs in Theorema. In: Proceedings of the 1st South-East European Workshop on Formal Methods (SEEFM'03), D. Dranidis and K. Tigka (ed.), pp. 140-147.November2003.Thessaloniki, Greece,ISSN: 960-87869-1-6.[pdf][bib]
Nikolaj Popov, Tudor Jebelean.A Practical Approach to Verification of Recursive Programs in Theorema. In: Proceedings of SYNASC'03 (International Workshop on Symbolic and Numeric Algorithms for Scientific Computing Timisoara, Romania, 2003), T. Jebelean, V. Negru, A. Popovici (ed.), pp. 329-332.October2003.Mirton,ISBN 973-661-104-3.[ps][pdf][bib]
L. Kovacs, T. Jebelean.Generation of Invariants in Theorema. In: Proceedings of the 10th International Symphosium of Mathematics and its Application, N.Boja (ed.), Scientific Bulletins of the Politehnica University Timisoara, Transactions on Mathematics and Physics, pp. 407-415.6-9 November2003.Timisoara, Romania,ISSN 1224-6069.[pdf][talk.nb][bib]
B. Buchberger, T. Jebelean, W. Windsteiger, T. Kutsia, K. Nakagawa, J. Robu, F. Piroi, A. Craciun, N. Popov, G. Kusper, M. Rosenkranz, L. Kovacs, C. Kocsis.F 1302: THEOREMA: Proving, Solving, and Computing in the Theory of Hilbert Spaces. In: Special Research Program (SFB) F 013, Numerical and Symbolic Scientific Computing, Proposal for Continuation, Part II: Proposal, P. Paule, U. Langer (ed.), pp. 58-73.October2003.Johannes Kepler University Linz, Austria,-.[bib]
T. Jebelean, B. Buchberger.Theorema: Computation and Deduction in Natural Style. In: Computer Algebra Handbook, J. Grabmeier, E. Kaltofen, V. Weispfennig (ed.), pp. 453-454.2003.Springer - Verlag Berlin,ISBN 3-540-65466-6.[bib]
L. Kovacs, T. Jebelean.Generation of Invariants in Theorema. In: Proceedings of the 10th International Symphosium of Mathematics and its Application, N.Boja (ed.), pp. 407-415.6-9 November2003.ISSN 1224-6069.Scientific Bulletins of the Politehnica University Timisoara, Transactions on Mathematics and Physics.[bib]
2002
Tudor Jebelean.Nonconventional Algorithms for Multiprecision Arithmetic. In: Proceeding of SYNASC'02, Negru at al (ed.), pp. 3-7.October2002.Mirton,Timisoara, Romania,ISBN: 973-585-785-5.[bib]
B. Buchberger, T. Jebelean, W. Windsteiger, T. Kutsia, K. Nakagawa, J. Robu, F. Piroi, A. Craciun, N. Popov, G. Kusper, M. Rosenkranz.F 1302: Solving and Proving in General Domains. In: Special Research Program (SFB) F 013, Numerical and Symbolic Scientific Computing, Annual Report 2002, U. Langer, F. Winkler (ed.), pp. 4-5.February2002.Johannes Kepler University Linz, Austria,[bib]
2001
Tudor Jebelean.Natural Proofs in Elementary Analysis by S-Decomposition. Technical report no. 01-33 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).November2001.[ps][ps][bib]
Florina Piroi, Tudor Jebelean.Advanced Proof Presentation in Theorema.Special Issue of the Annals of the University of the West, Timisoara.XXXIX, pp. 181-199.September2001.ISSN 1224-970X.Proceedings of SYNASC 01, 3rd International Workshop on Symbolic and Numeric Algorithms for Scientific Computing, Timisoara, Romania, October 2-5, 2001.[bib]
Boris Konev, Tudor Jebelean.Solution Lifting Method for Handling Meta-variables in Theorema. In: Proceedings of SYNASC01, S. Maruster, B. Buchberger, V. Negru, T. Jebelean (ed.), Proceedings of 3rd International Workshop on Symbolic and Numeric Algorithms for Scientific Computing, pp. 15-23.October2001.Mirton,Timisoara, Romania,ISSN: 973-661-441-7.[bib]
Tudor Jebelean.Non-conventional Algorithms for Multiple Precision Arithmetic. RISC, University of Linz. PhD Thesis.December2001.Habilitation thesis.[bib]
2000
B. Buchberger, D. Vasaru, T. Jebelean.The Theorema System: Current Status and the Proving-Solving-Computing Cycle. Technical report no. 00-37 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).May2000.[ps][bib]
B. Buchberger, C. Dupre, T. Jebelean, B. Konev, F. Kriftner, T. Kutsia, K. Nakagawa, F. Piroi, D. Vasaru, W. Windsteiger.The Theorema System: Proving, Solving, and Computing for the Working Mathematician. Technical report no. 00-38 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).August2000.[ps][bib]
B. Buchberger, C. Dupre, T. Jebelean, B. Konev, F. Kriftner, T. Kutsia, K. Nakagawa, F. Piroi, D. Vasaru, W. Windsteiger.The Natural Style Provers of Theorema: A Survey of Strategies for Different Mathematical Domains. Technical report no. 00-39 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).June2000.[ps][bib]
Boris Konev, Tudor Jebelean.Combining Level-Saturation Strategies and Meta-Variables for Predicate Logic Proving in Theorema. Technical report no. 00-40 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).June2000.[ps][bib]
B. Buchberger, C. Dupre, T. Jebelean, B. Konev, F. Kriftner, T. Kutsia, K. Nakagawa, F. Piroi, D. Vasaru, W. Windsteiger.The Facilities of Theorema for Teaching Logic and Mathematics. Technical report no. 00-41 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).June2000.[ps][bib]
T. Jebelean, M. Dragan, D. Tepeneu, V. Negru.Parallel Algorithms for Practical Multiprecision Arithmetic Using the Karatsuba Method. Technical report no. 00-42 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).September2000.[ps][bib]
B. Buchberger, C. Dupre, T. Jebelean, F. Kriftner, K. Nakagawa, D. Vasaru, W. Windsteiger.The Theorema Project: A Progress Report. In: Symbolic Computation and Automated Reasoning (Proceedings of CALCULEMUS 2000, Symposium on the Integration of Symbolic Computation and Mechanized Reasoning), M. Kerber, M. Kohlhase (ed.), pp. 98-113.6-7 August2000.Copyright: A.K. Peters, Natick, Massachusetts,St. Andrews, Scotland,ISBN 1-56881-145-4.[ps][pdf][abstract][bib]
1999
B. Buchberger, T. Jebelean.Teaching of Mathematics Using Theorema. The International Journal of Computer Algebra in Mathematical Education6(1), pp. 25-50.1999.Copyright: Research Information Ltd., UK.,ISSN 1362-7368.[bib]
Bogdan Matasaru, Tudor Jebelean.FPGA Implementation of an Extended Binary GCD Algorithm for Systolic Reduction of Rational Numbers. Technical report no. 99-48 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).November1999.[ps][bib]
Bruno Buchberger, Claudio Dupre, Tudor Jebelean, Franz Kriftner, Koji Nakagawa, Daniela Vasaru, Wolfgang Windsteiger.Theorema: A Progress Report. Technical report no. 99-42 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December1999.Also available as SFB Report 99-35, Johannes Kepler University Linz, Spezialforschungsbereich F013, December, 1999.[ps][bib]
Bruno Buchberger, Tudor Jebelean.Distance Teaching of Mathematics Using Theorema. Technical report no. 99-43 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December1999.Also available as SFB Report No. 99-36, Johannes Kepler University Linz, Spezialforschungsbereich F013, December, 1999.[doc][bib]
Bruno Buchberger, Claudio Dupre, Tudor Jebelean, Franz Kriftner, Koji Nakagawa, Daniela Vasaru, Wolfgang Windsteiger.Theorema: A Short Demo. Technical report no. 99-45 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December1999.Also available as SFB Report 99-37, Johannes Kepler University Linz, Spezialforschungsbereich F013, December, 1999.[tar.gz][bib]
B. Buchberger, T. Jebelean.Distance Teaching of Mathematics Using Theorema. In: Proceedings of the 3rd Technion Symposium on Software for Communication, H. Gutmann (ed.), pp. -.April 1-31999.Hagenberg, Austria,[bib]
1998
Bruno Buchberger, Tudor Jebelean.The Second International Theorema Workshop. Technical report no. 98-10 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).June1998.[bib]
Bruno Buchberger, Klaus Aigner, Claudio Dupre, Tudor Jebelean, Franz Kriftner, Mircea Marin, Koji Nakagawa, Ovidiu Podisor, Elena Tomuta, Yaroslav Usenko, Daniela Vasaru, Wolfgang Windsteiger.Theorema: An Integrated System for Computation and Deduction in Natural Style. Technical report no. 98-25 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December1998.Also available as SFB Report No. 98-06.[ps][bib]
B. Buchberger, T. Jebelean, D. Vasaru.Theorema: A System for Formal Scientific Training in Natural Language Presentation. Johannes Kepler University Linz, Spezialforschungsbereich F013. Technical report no. 98-05, SFB Report, June1998.[bib]
B. Buchberger, T. Jebelean, D.Vasaru.Theorema: A System for Formal Scientific Training in Natural Language Presentation. In: Proceedings of Ed-Media 1998 (International Conference on Educational Multimedia), - (ed.), pp. 174-179.June 20-231998.Freiburg, Germany,[bib]
B. Buchberger, T. Jebelean.Theorema: Using the Predicate Logic Prover for Proof Training. In: Proceedings of the Second International Theorema Workshop, B. Buchberger, T. Jebelean (ed.), pp. -.June 29-301998.RISC, Hagenberg, Austria,-.RISC-Linz Report Series No. 98-10.[bib]
1997
Bruno Buchberger, Tudor Jebelean, Franz Kriftner, Mircea Marin, Elena Tomuta, Daniela Vasaru.A Survey of the Theorema Project. Technical report no. 97-15 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).March1997.[ps][bib]
Tudor Jebelean.Using the Parallel Karatsuba Algorithm for Long Integer Multiplication and Division. Technical report no. 97-08 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).February1997.[ps][bib]
Tudor Jebelean.Auto-Configurable Array for GCD Computation. Technical report no. 97-12 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).March1997.[ps][bib]
Bruno Buchberger, Tudor Jebelean, Daniela Vasaru.Theorema: A System for Formal Scientific Training in Natural Language Presentation. Technical report no. 97-34 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).October1997.[bib]
B. Buchberger, T. Jebelean, F. Kriftner, M. Marin, E. Tomuta, D. Vasaru.A Survey of the Theorema project. In: Proceedings of ISSAC'97 (International Symposium on Symbolic and Algebraic Computation, Maui, Hawaii, July 21-23, 1997), W. Kuechlin (ed.), pp. 384-391.1997.ACM Press, ISBN 0-89791-875-4.[bib]
B. Buchberger, T. Jebelean.Theorema: The Predicate Logic Prover. In: First International Theorema Workshop, B. Buchberger, T. Ida, D. Vasaru (ed.), pp. -.June 9-101997.RISC, Hagenberg, Austria,-.RISC-Linz Report Series No. 97-20.[bib]
1996
Tudor Jebelean.Practical Integer Division with Karatsuba Complexity. Technical report no. 96-29 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December1996.[ps][bib]
Tudor Jebelean.Exact Division with Karatsuba Complexity. Technical report no. 96-31 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December1996.[ps][bib]
Werner Krandick, Tudor Jebelean.Bidirectional Exact Integer Division. Technical report no. 96-32 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December1996.not available in electronic form.[bib]
Tudor Jebelean.Integer and Rational Arithmetic on MasPar. Technical report no. 96-38 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December1996.[ps][bib]
Tudor Jebelean.Design of a Systolic Coprocessor for Rational Addition. Technical report no. 96-37 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December1996.[ps][bib]
1994
Tudor Jebelean.Systolic Multiprecision Arithmetic. Technical report no. 94-37 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).1994.[bib]
Lucian Cucu, Mircea Dragan, Tudor Jebelean, Viorel Negru.Motion Planning Through Voronoi Diagrams Construction on Shared Memory Architecture. Technical report no. 94-42 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).1994.[bib]
Tudor Jebelean.Designing Systolic Arrays for Integer GCD Computation. Technical report no. 94-47 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).1994.Published in Proceedings of ASAP'94 (Application Specific Array Processors), San Francisco, August 1994, IEEE Computer Society Press..[bib]
Werner Krandick, Tudor Jebelean.Bidirectional Exact Integer Divison. Technical report no. 94-50 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).1994.Published in Proceedings, PASCO'94, World Scientific Publ. Comp..[bib]
Tudor Jebelean.Implementing GCD Systolic Arrays on FPGA. Technical report no. 94-57 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).1994.Published in Proceedings of FPLA 94 (Field Programmable Logic and Applications), Prague, Czech Republic, Sept. 1994..[bib]
Tudor Jebelean.Systolic Algorithms for Long Integer GCD Computation. Technical report no. 94-58 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).1994.Published in Proceedings of CONPAR 94, Linz, Austria, Sept. 1994..[bib]
Tudor Jebelean.Systolic Multiprecision Arithmetics. RISC, Johannes Kepler University Linz. PhD Thesis.1994.[bib]
1993
Tudor Jebelean.Systolic Normalization of Rational Numbers. Technical report no. 93-45 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).XXX1993.Published in Proceedings ASAP'93(Application Specific Array Processors), Venice, Oct. 1993, IEEE Computer Society Press. To appear..[ps][bib]
Tudor Jebelean.A Generalization of the Binary GCD Algorithm. Technical report no. 93-01 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).1993.[bib]
Tudor Jebelean.Rational Arithmetic Using FPGA. Technical report no. 93-48 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).1993.Published in Presented at: Second International Workshop on Field Programmable Logic and Application; Oxford, England, Sept. 7-9, 1993..[bib]
Lucian Cucu, Mircea Dragan, Tudor Jebelean, Viorel Negru, Ion Popescu.Construction of Voronoi Diagrams. Technical report no. 93-52 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).1993.[bib]
Lucian Cucu, Mircea Dragan, Tudor Jebelean, Viorel Negru.Delaunay Triangulation Using Divide-and-Conquer. Technical report no. 93-62 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).1993.[bib]
B. Buchberger, T. Jebelean.Systolic Multiprecision Arithmetic. In: Proceedings of Impact TEMPUS JEP and Hungarian Transputer Users Group Workshop "Parallel Processing in Education", - (ed.), pp. -.March1993.Miskolc, Hungary,-.[bib]
1992
Bruno Buchberger, Tudor Jebelean.Parallel Rational Arithmetic for Computer Algebra Systems: Motivating Experiments. Technical report no. 92-29 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).1992.Published in A preliminary version was presented at the ACPC (Austrian Center for Parallel Computation) workshop in Weinberg, Austria, April 1992..[bib]
Hoon Hong, Wolfgang Schreiner, Andreas Neubacher, Kurt Siegl, Hans-Wolfgang Loidl, Tudor Jebelean, Peter Zettler.PAC LIB User Manual. Technical report no. 92-32 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).1992.[bib]
Tudor Jebelean.An Algorithm for Exact Division. Technical report no. 92-35 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).1992.[bib]
Bruno Buchberger, Tudor Jebelean.Systolic Algorithms in Computer Algebra State of the Project. Technical report no. 92-38 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).1992.[bib]
Tudor Jebelean, Thomas Moritz.RISPEL RISC's Specification Language Reference Manual. Technical report no. 92-44 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).1992.[bib]
Tudor Jebelean.Systolic Multiplication on MasPar. Technical report no. 92-68 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).1992.[bib]
Tudor Jebelean.Improving the Multiprecision Euclidean Algorithm. Technical report no. 92-69 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).1992.[bib]
Tudor Jebelean.Comparing Several GCD Algorithms. Technical report no. 92-70 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).1992.[bib]
Tudor Jebelean.Systolic Algorithms for Exact Division. Technical report no. 92-71 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).1992.[bib]
Tudor Jebelean.On the Possibility of Implementing Fine Grain Systolic Algorithms on Certain Parallel Architectures. Technical report no. 92-72 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).1992.[bib]
1991
B. Buchberger, T. Jebelean.Systolic Algorithms in Computer Algebra. In: Proceedings of the NATO ASI on Parallel Processing on Distributed Memory Multiprocessors, - (ed.), pp. -.July1991.Ankara,-.[bib]