e-Austria Timisoara: Pilot Phase I

Project Description

B. Buchberger, T. Jebelean.
Budget: 100.000,– Eur.
Projektbeginn bzw. Projectende 2003:

Project Lead

Project Duration

01/03/2002 - 30/06/2003

Publications

2017

[Buchberger]

Gröbner Bases Computation by Triangularizing Macaulay Matrices

Bruno Buchberger

Advanced Studies in Pure Mathematics (The 50th Anniversary of Gröbner Bases) 75, pp. 1-9. 2017. Mathematical Society of Japan, 0.
[bib]
@article{RISC5586,
author = {Bruno Buchberger},
title = {{Gröbner Bases Computation by Triangularizing Macaulay Matrices}},
language = {english},
journal = {Advanced Studies in Pure Mathematics (The 50th Anniversary of Gröbner Bases)},
volume = {75},
pages = {1--9},
publisher = {Mathematical Society of Japan},
isbn_issn = {0},
year = {2017},
refereed = {no},
length = {9}
}
[Buchberger]

Satisfiability Checking and Symbolic Computation

Abraham Erika , Abbott John , Becker Bernd , Bigatti Anna Maria , Brain Martin , Buchberger Bruno , Cimatti Alessandro , Davenport James , England Matthew , Fontaine Pascal , Forrest Stephen , Griggio Alberto , Kröning Daniel , Seiler Werner M. , Sturm

ACM Communications in Computer Algebra 50(4), pp. 145-147. 2017. 0.
[bib]
@article{RISC5587,
author = { Abraham Erika and Abbott John and Becker Bernd and Bigatti Anna Maria and Brain Martin and Buchberger Bruno and Cimatti Alessandro and Davenport James and England Matthew and Fontaine Pascal and Forrest Stephen and Griggio Alberto and Kröning Daniel and Seiler Werner M. and Sturm },
title = {{Satisfiability Checking and Symbolic Computation}},
language = {english},
journal = {ACM Communications in Computer Algebra},
volume = {50},
number = {4},
pages = {145--147},
isbn_issn = {0},
year = {2017},
refereed = {no},
length = {3}
}

2015

[Dramnesc]

Theory Exploration of Binary Trees

Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat

In: The IEEE 13th Jubilee International Symposium on Intelligent Systems and Informatics, . (ed.), Proceedings of SISY 2015, pp. 139-144. 2015. IEEE Xplore, ..
[bib]
@inproceedings{RISC5165,
author = {Isabela Dramnesc and Tudor Jebelean and Sorin Stratulat},
title = {{Theory Exploration of Binary Trees}},
booktitle = {{The IEEE 13th Jubilee International Symposium on Intelligent Systems and Informatics}},
language = {english},
pages = {139--144},
publisher = {IEEE Xplore},
isbn_issn = {.},
year = {2015},
editor = {.},
refereed = {yes},
length = {6},
conferencename = {SISY 2015}
}
[Dramnesc]

Synthesis of Some Algorithms for Trees: Experiments in Theorema

Isabela Dramnesc, Tudor Jebelean and Sorin Stratulat

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]
@techreport{RISC5147,
author = {Isabela Dramnesc and Tudor Jebelean and Sorin Stratulat},
title = {{Synthesis of Some Algorithms for Trees: Experiments in Theorema}},
language = {english},
number = {15-04},
year = {2015},
length = {57},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}

2011

[Buchberger]

Symbolic Analysis for Boundary Problems: From Rewriting to Parametrized Groebner Bases

Markus Rosenkranz, Georg Regensburger, Loredana Tec, Bruno Buchberger

In: Numerical and Symbolic Scientific Computing: Progress and Prospects, Ulrich Langer and Peter Paule (ed.), pp. 273-331. 2011. Springer, Wien, ISBN 978-3-7091-0793-5. Also available as RICAM Report 2010-05, September 2010. [pdf]
[bib]
@incollection{RISC4330,
author = {Markus Rosenkranz and Georg Regensburger and Loredana Tec and Bruno Buchberger},
title = {{Symbolic Analysis for Boundary Problems: From Rewriting to Parametrized Groebner Bases}},
booktitle = {{Numerical and Symbolic Scientific Computing: Progress and Prospects}},
language = {english},
pages = {273--331},
publisher = {Springer, Wien},
isbn_issn = {ISBN 978-3-7091-0793-5},
year = {2011},
annote = {2011-00-00-A},
note = {Also available as RICAM Report 2010-05, September 2010},
editor = {Ulrich Langer and Peter Paule},
refereed = {yes},
length = {54}
}
[Buchberger]

Buchberger's Algorithm

Bruno Buchberger, Manuel Kauers

Scholarpedia 6(10), pp. 7764-7764. October 2011. 1941-6016. [url]
[bib]
@article{RISC4394,
author = {Bruno Buchberger and Manuel Kauers},
title = {{Buchberger's Algorithm}},
language = {english},
journal = {Scholarpedia},
volume = {6},
number = {10},
pages = {7764--7764},
isbn_issn = {1941-6016},
year = {2011},
month = {October},
annote = {2011-10-00-A},
refereed = {yes},
length = {1},
url = {http://www.scholarpedia.org/article/Buchberger%27s_algorithm}
}
[Popov]

Sound and Complete Verification Condition Generator for Functional Recursive Programs.

N. Popov, T. Jebelean

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]
@incollection{RISC4342,
author = {N. Popov and T. Jebelean},
title = {{Sound and Complete Verification Condition Generator for Functional Recursive Programs.}},
booktitle = {{Numerical and Symbolic Scientific Computing: Progress and Prospects}},
language = {english},
pages = {219--256},
publisher = {Springer},
address = {Wien},
isbn_issn = {ISBN 978-3-7091-0793-5},
year = {2011},
editor = {U. Langer and P. Paule},
refereed = {yes},
length = {38}
}

2010

[Buchberger]

An Automated Confluence Proof for an Infinite Rewrite System Parametrized over an Integro-Differential Algebra

Loredana Tec, Georg Regensburger, Markus Rosenkranz and Bruno Buchberger

In: Mathematical Software - ICMS 2010, Third International Congress on Mathematical Software, Kobe, Japan, September 13-17, Komei Fukuda and Joris van der Hoeven and Michael Joswig and Nobuki Takayama (ed.), Proceedings of ICMS, Lecture Notes in Computer Science 6327, pp. 245-248. 2010. Springer, 978-3-642-15581-9. [pdf]
[bib]
@inproceedings{RISC4044,
author = {Loredana Tec and Georg Regensburger and Markus Rosenkranz and Bruno Buchberger},
title = {{An Automated Confluence Proof for an Infinite Rewrite System Parametrized over an Integro-Differential Algebra}},
booktitle = {{Mathematical Software - ICMS 2010, Third International Congress on Mathematical Software, Kobe, Japan, September 13-17}},
language = {english},
series = {Lecture Notes in Computer Science},
volume = {6327},
pages = {245--248},
publisher = {Springer},
isbn_issn = {978-3-642-15581-9},
year = {2010},
annote = {2010-09-00-A},
editor = {Komei Fukuda and Joris van der Hoeven and Michael Joswig and Nobuki Takayama},
refereed = {yes},
length = {4},
conferencename = {ICMS}
}
[Buchberger]

Groebner Bases

Bruno Buchberger, Manuel Kauers

Scholarpedia 5(10), pp. 7763-7763. October 2010. ISSN 1941-6016. [url]
[bib]
@article{RISC4161,
author = {Bruno Buchberger and Manuel Kauers},
title = {{Groebner Bases}},
language = {english},
journal = {Scholarpedia},
volume = {5},
number = {10},
pages = {7763--7763},
isbn_issn = {ISSN 1941-6016},
year = {2010},
month = {October},
annote = {2010-10-00-A},
refereed = {yes},
length = {16},
url = {http://www.scholarpedia.org/article/Groebner_basis}
}
[Buchberger]

From Program Verification to Automated Debugging

N. Popov, T. Jebelean, B. Buchberger

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]
@inproceedings{RISC4192,
author = {N. Popov and T. Jebelean and B. Buchberger},
title = {{From Program Verification to Automated Debugging}},
booktitle = {{Workshop on Symbolic Computation in Software Science}},
language = {english},
pages = {55--65},
publisher = {RISC-Linz Report Series},
isbn_issn = {.},
year = {2010},
month = {July},
annote = {2010-07-00-A},
editor = {T. Jebelean and M. Mosbah and N. Popov},
refereed = {yes},
institution = {Johannes Kepler University of Linz, Austria},
length = {11},
conferencename = {SCSS 2010}
}
[Kusper]

Experiments with Multi-Domain Logic: Variable Merging and Split Strategies

Tudor Jebelean, Gabor Kusper

Technical report no. 10-03 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). February 2010. [pdf]
[bib]
@techreport{RISC3948,
author = {Tudor Jebelean and Gabor Kusper},
title = {{Experiments with Multi-Domain Logic: Variable Merging and Split Strategies}},
language = {English},
abstract = {Multi-Domain Logic (MDL) is a generalization of signed logic, in whichevery variable has its own domain.This aspect increases the efficiency of direct solving of MDL satisfiability,because the solving process proceeds by reducing the size of the domains(contradiction appears as an empty domain).In contrast to the usual approach of translating signed logic satisfiabilityinto boolean satisfiability, we implement the generalized DPLL directly forMDL, using a specific version of the techniques used for signed logic.Moreover, we use a novel techinque -- {\em variable merging}, whichconsists in replacing two or more variables by a new one, whose domain is thecartesian product of the old domains.This operation is used during the solving process in order to reduce the number of variables.Moreover, variable merging can be used at the beginning of the solving processin order to translate a boolean SAT problem into an MDL problem.This opens the possibility of using MDL solvers as an alternative to booleansolvers, which is promising because in MDL several boolean constraints can bepropagated simultaneously.Our experiments with a prototype eager solver show the effects of the initialmerging factor of boolean variables, as well as the effects of differentdesign decisions on the efficiency of the method.},
number = {10-03},
year = {2010},
month = {February},
keywords = {SAT, signed logic, Multi-Domain Logic},
length = {10},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
[Popov]

Projects of Evidence Algorithm and Theorema

A. Anisimov, T. Jebelean, A. Lyaletski, N. Popov

In: Theoretical and Applied Aspects of Program Systems Development, A. Anisimov, V. Redko (ed.), pp. 54-58. October 2010. Kiev, Ukraine, ..
[bib]
@inproceedings{RISC4195,
author = {A. Anisimov and T. Jebelean and A. Lyaletski and N. Popov},
title = {{Projects of Evidence Algorithm and Theorema}},
booktitle = {{Theoretical and Applied Aspects of Program Systems Development}},
language = {russian},
pages = {54--58},
address = {Kiev, Ukraine},
isbn_issn = {.},
year = {2010},
month = {October},
editor = {A. Anisimov and V. Redko},
refereed = {yes},
length = {5}
}
[Popov]

Proceedings of SCSS 2010 Symbolic Computation in Software Science

T. Jebelean, M. Mosbah, N. Popov (eds.)

Technical report no. 10-10 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). August 2010. [pdf]
[bib]
@techreport{RISC4191,
author = {T. Jebelean and M. Mosbah and N. Popov (eds.)},
title = {{Proceedings of SCSS 2010 Symbolic Computation in Software Science}},
language = {english},
number = {10-10},
year = {2010},
month = {August},
length = {160},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
[Popov]

Proving Partial Correctness and Termination of Mutually Recursive Programs

N. Popov, T. Jebelean

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]
@inproceedings{RISC4287,
author = {N. Popov and T. Jebelean},
title = {{Proving Partial Correctness and Termination of Mutually Recursive Programs}},
booktitle = {{SYNASC 2010}},
language = {english},
pages = {153--158},
publisher = {IEEE },
isbn_issn = {ISBN 978-0-7695-4324-6},
year = {2010},
month = {September},
editor = {T. Ida and V. Negru and T. Jebelean and D. Petcu and S. Watt and and and D. Zaharie},
refereed = {yes},
length = {5},
conferencename = {Symposium on Symbolic and Numeric Algorithms for Scientific Computing}
}

2009

[Buchberger]

Automated Reasoning

Tudor Jebelean, Bruno Buchberger, Temur Kutsia, Nikolaj Popov, Wolfgang Schreiner, Wolfgang Windsteiger

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]
@incollection{RISC3844,
author = {Tudor Jebelean and Bruno Buchberger and Temur Kutsia and Nikolaj Popov and Wolfgang Schreiner and Wolfgang Windsteiger},
title = {{Automated Reasoning}},
booktitle = {{Hagenberg Research}},
language = {english},
pages = {63--101},
publisher = {Springer Dordrecht Heidelberg London New York},
isbn_issn = {ISBN 978-3-642-02126-8},
year = {2009},
annote = {2009-00-00-B},
editor = {B. Buchberger and M. Affenzeller and A. Ferscha and M. Haller and T. Jebelean and E.P. Klement and P. Paule and G. Pomberger and W. Schreiner and R. Stubenrauch and R. Wagner and G. Weiss and W. Windsteiger},
refereed = {no},
length = {39},
url = {http://www.springer.com/computer/programming/book/978-3-642-02126-8}
}
[Buchberger]

Algorithms in Symbolic Computation

Peter Paule, Bruno Buchberger, Lena Kartashova, Manuel Kauers, Carsten Schneider, Franz Winkler

In: Hagenberg Research, Bruno Buchberger et al. (ed.), Chapter 1, pp. 5-62. 2009. Springer, 978-3-642-02126-8. [doi] [pdf]
[bib]
@incollection{RISC3845,
author = {Peter Paule and Bruno Buchberger and Lena Kartashova and Manuel Kauers and Carsten Schneider and Franz Winkler},
title = {{Algorithms in Symbolic Computation}},
booktitle = {{Hagenberg Research}},
language = {english},
chapter = {1},
pages = {5--62},
publisher = {Springer},
isbn_issn = {978-3-642-02126-8},
year = {2009},
annote = {2009-00-00-C},
editor = {Bruno Buchberger et al.},
refereed = {no},
length = {58},
url = {https://doi.org/10.1007/978-3-642-02127-5_2}
}
[Craciun]

Automatheo 2009: Proceedings of the Workshop on Automated Mathematical Theory Exploration

B. Buchberger, R. McCasland, A. Craciun

Technical report no. 09-12 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). June 2009.
[bib]
@techreport{RISC3914,
author = {B. Buchberger and R. McCasland and A. Craciun},
title = {{Automatheo 2009: Proceedings of the Workshop on Automated Mathematical Theory Exploration}},
language = {english},
number = {09-12},
year = {2009},
month = {June},
annote = {2009-06-00-A},
length = {148},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
[Popov]

Using Computer Algebra Techniques for the Specification, Verification and Synthesis of Recursive Programs

N. Popov, T. Jebelean

Mathematics and Computers in Simulation 79(8), pp. 2293-2301. April 2009. Elsevier, ISSN: 0378-4754. [pdf]
[bib]
@article{RISC3095,
author = {N. Popov and T. Jebelean},
title = {{Using Computer Algebra Techniques for the Specification, Verification and Synthesis of Recursive Programs}},
language = {english},
journal = {Mathematics and Computers in Simulation},
volume = {79},
number = {8},
pages = {2293--2301},
publisher = {Elsevier},
isbn_issn = {ISSN: 0378-4754},
year = {2009},
month = {April},
refereed = {yes},
length = {12}
}
[Popov]

Verification of Mutual Recursive Functional Programs

N. Popov, T. Jebelean

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]
@inproceedings{RISC3912,
author = {N. Popov and T. Jebelean},
title = {{Verification of Mutual Recursive Functional Programs}},
booktitle = {{Proceedings of Workshop on Symbolic Computation in Software Science SCSS'09}},
language = {english},
pages = {120--122},
address = {Carthage, Tunisia},
isbn_issn = {.},
year = {2009},
month = {September},
editor = {T. Ida and A. Bouhoula},
refereed = {yes},
length = {15}
}
[Popov]

Functional Program Verification in Theorema. Soundness and Completeness

N. Popov, T. Jebelean

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]
@inproceedings{RISC3913,
author = {N. Popov and T. Jebelean},
title = {{Functional Program Verification in Theorema. Soundness and Completeness}},
booktitle = {{Proceedings of 15th Biennial Workshop on Programmiersprachen und Grundlagen der Programmierung KPS'09}},
language = {english},
pages = {221--229},
address = {Maria Taferl, Austria},
isbn_issn = {.},
year = {2009},
month = {October},
editor = {J. Knoop and A. Prantl},
refereed = {yes},
length = {9}
}

Loading…