RISC-Linz RISC-Linz Research Institute for Symbolic Computation  
about
|
people
|
publications
|
research
|
education
|
industry
|
conferences
|
media
|
projects
internal
  
search:
  

Tudor Jebelean, A.Univ.-Prof. Dr.

RISC Faculty

Publications

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. April 2018. 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 Computation 90, pp. 3-41. 2018. Elsevier, 07477171. [url] [bib]
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. September 2017. [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]
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, LNCS 9618, 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. JFR 9(1), pp. 149-185. 2016. ISSN 1972-5787. [url] [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. [url] [bib]
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 Computation 69, 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. 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]
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]
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. December 2012. [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, January 2012. 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. January 2012. 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-26 2012. 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. September 2012. 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. September 2012. IEEE Computer Society, ISBN-13: 978-0-7695-4934-7. [bib]
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. July 2011. [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. September 2011. IEEE Computer Society, ISBN 978-0-7695-4630-8. [url] [pdf] [bib]
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. February 2010. [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. May 2010. [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. 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. September 2010. 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. August 2010. [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. July 2010. 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. October 2010. 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. September 2010. 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 - Informatica XLVIII/3, pp. 47-58. 23-26 September 2010. 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 July 2010. RISC-Linz Report Series, Johannes Kepler University of Linz, Austria, . [pdf] [bib]
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. January 2009. [pdf] [ps] [bib]
N. Popov, T. Jebelean. Using Computer Algebra Techniques for the Specification, Verification and Synthesis of Recursive Programs. Mathematics and Computers in Simulation 79(8), pp. 2293-2301. April 2009. 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 Simulation 79(8), pp. 2310-2316. April 2009. 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. September 2009. 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. October 2009. 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. June 2009. Hagenberg, Austria, -. [pdf] [bib]
B. Buchberger, M. Affenzeller, A. Ferscha, M. Haller, T. Jebelean, E.P. Klement, P. Paule, G. Pomberger, W. Schreiner, R. Stubenrauch, R. Wagner, G. Weiß, W. Windsteiger (ed.). Hagenberg Research. 2009. Springer Dordrecht Heidelberg London New York, ISBN 978-3-642-02126-8. [url] [bib]
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. March 2008. 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. July 2008. .. [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. September 2008. [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]
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. June 2007. 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. 06 2007. 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 1 2007. 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. 2007. [ps] [bib]
T. Jebelean, V. Negru (ed.). SYNASC'07. Proceedings of International Workshop on Symbolic and Numeric Algorithms for Scientific Computing, September 2007. Mirton, Timisoara, Romania, [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.), LNCS 4449, pp. 37-54. 2007. Springer, 978-3-540-74129-9. [bib]
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 Logic 4(4), pp. 470-504. 2006. ISSN 1570-8683. [url] [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. 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-16 2006. [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. November 2006. 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]
L. Kovacs, T. Jebelean. Combining Computer Algebra and Computational Logic for Imperative Program Verification in Theorema. July 6-9 2006. Poster presentation at Calculemus'06, Genova, Italy. [bib]
T. Jebelean, V. Negru (ed.). SYNASC'06. Proceedings of International Workshop on Symbolic and Numeric Algorithms for Scientific Computing, September 2006. Mirton, Timisoara, Romania, ISBN: 0-7695-2740-X. [bib]
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 May 2005. 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-28 2005. 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]
T. Jebelean, V. Negru (ed.). SYNASC'05. Proceedings of International Workshop on Symbolic and Numeric Algorithms for Scientific Computing, 2005. Mirton, Timisoara, Romania, ISBN: 0-7695-2453-2. [bib]
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 September 2004. 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 May 2004. 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. June 2004. [pdf] [ps] [ps] [bib]
T. Jebelean, V. Negru (ed.). SYNASC'04. Proceedings of International Workshop on Symbolic and Numeric Scientific Computing, September 2004. Mirton, Timisoara, Romania, ISBN: 973-661-441-4. [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. June 2004. 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. November 2004. Paphos, Cyprus, University of Cyprus, [ps] [pdf] [bib]
L. Kovacs, T. Jebelean. Automated Generation of Loop Invariants by Recurrence Solving in Theorema. Analele Universitatii din Timisoara, Seria Matematica - Informatica XLII, pp. 151-166. 2004. Mirton Publisher, Timisoara, Romania, ISSN 1224-970X. special issue on Computer Science - Proceedings of SYNASC'04. [pdf] [bib]
L. Kovacs, T. Jebelean. Practical Aspects of Imperative Program Verification in Theorema. Analele Universitatii din Timisoara, Seria Matematica - Informatica XLI, 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 October 2003. 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. November 2003. 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. October 2003. Mirton, ISBN 973-661-104-3. [pdf] [ps] [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 November 2003. Timisoara, Romania, ISSN 1224-6069. [pdf] [talk.nb] [bib]
T. Jebelean, V. Negru (ed.). SYNASC'03. Proceedings of International Workshop on Symbolic and Numeric Algorithms for Scientific Computing, October 2003. Mirton, Timisoara, Romania, ISSN: 973-661-104-3. [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. October 2003. 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 November 2003. ISSN 1224-6069. Scientific Bulletins of the Politehnica University Timisoara, Transactions on Mathematics and Physics. [bib]
T. Jebelean, V. Negru (ed.). SYNASC'02. Proceedings of International Workshop on Symbolic and Numeric Scientific Computing, October 2002. Mirton, Timisoara, Romania, ISBN: 973-585-785-5. [bib]
Tudor Jebelean. Theorema: A system for the working mathematician. 2002. The abstract of the talk and the software demo are published electronically on the CD-ROM accompanying the proceedings (ACM Press, ISBN 1-58113-582-3). Software presentation at International Symposium for Symbolic and Algebraic Computation (ISSAC). [bib]
Tudor Jebelean. Nonconventional Algorithms for Multiprecision Arithmetic. In: Proceeding of SYNASC'02, Negru at al (ed.), pp. 3-7. October 2002. 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. February 2002. Johannes Kepler University Linz, Austria, [bib]
Armando and Jebelean (ed.). Calculemus: Integrating Computation and Deduction. Proceedings of Calculemus: Integrating Computation and Deduction, 32/4, November 2001. Special Issue of Journal of Symbolic Computation. [bib]
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. November 2001. [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. September 2001. 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. October 2001. Mirton, Timisoara, Romania, ISSN: 973-661-441-7. [bib]
Tudor Jebelean. Non-conventional Algorithms for Multiple Precision Arithmetic. RISC, University of Linz. PhD Thesis. December 2001. Habilitation thesis. [bib]
T. Jebelean and V. Negru (ed.). SYNASC'01. Proceedings of International Workshop on Symbolic and Numeric Algorithms for Scientific Computing, September 2001. Mirton, Timisoara, Romania, ISSN: 973-661-441-7. [bib]
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. May 2000. [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. August 2000. [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. June 2000. [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. June 2000. [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. June 2000. [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. September 2000. [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 August 2000. Copyright: A.K. Peters, Natick, Massachusetts, St. Andrews, Scotland, ISBN 1-56881-145-4. [ps] [pdf] [abstract] [bib]
B. Buchberger, T. Jebelean. Teaching of Mathematics Using Theorema. The International Journal of Computer Algebra in Mathematical Education 6(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. November 1999. [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. December 1999. 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. December 1999. 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. December 1999. 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-3 1999. Hagenberg, Austria, [bib]
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. June 1998. [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. December 1998. 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, June 1998. [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-23 1998. 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-30 1998. RISC, Hagenberg, Austria, -. RISC-Linz Report Series No. 98-10. [bib]
Second International Theorema Workshop (ed.). Second International Theorema Workshop. Proceedings of Second International Theorema Workshop, 1998. [bib]
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. March 1997. [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. February 1997. [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. March 1997. [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. October 1997. [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-10 1997. RISC, Hagenberg, Austria, -. RISC-Linz Report Series No. 97-20. [bib]
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. December 1996. [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. December 1996. [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. December 1996. 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. December 1996. [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. December 1996. [ps] [bib]
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. 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. 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. 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. 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. 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. 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]
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. XXX 1993. 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. 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. 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. 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. 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. -. March 1993. Miskolc, Hungary, -. [bib]
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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 1992. [bib]
B. Buchberger, T. Jebelean. Systolic Algorithms in Computer Algebra. In: Proceedings of the NATO ASI on Parallel Processing on Distributed Memory Multiprocessors, - (ed.), pp. -. July 1991. Ankara, -. [bib]


webmaster