## Open Topics

Prerequisites: basic knowledge of the Mathematica programming language and LaTeX, interest in writing/formating mathematical documents, working in a bigger team, and structured software development.

Working area: 50% mathematics, 50% informatics.

### Symbolic Summation and the Interlacing Method in Difference Rings

Master Thesis

Advisor: Carsten Schneider

## Theses in Progress

### Eine industrielle Anwendung von heuristischen Optimierungsverfahren für das Bin-Packing Problem

Master Thesis

Advisor: Wolfgang Windsteiger

Investigator: Ingolf Neumüller

### Implementation of symbolic geometric method for rational solutions of AODEs

Master Thesis

Advisor: Franz Winkler

Investigator: Fabrizio Zucca

### Radu’s Ramanujan-Kolberg Algorithm in Mathematica

Master Thesis

Advisor: Peter Paule

Investigator: Bernhard Kepplinger

### Formal Design Method For Reasoning about Algorithms and Representing Efficient Programs

PhD Thesis

Advisor: Tudor Jebelean

Investigator: Jakob Praher

### Unification and Anti-Unification Algorithms with Proximity Relations

PhD Thesis

Advisor: Teimuraz Kutsia

Investigator: Ioana-Cleopatra Pau

## Finished Theses

### 2020

### Power Series Solutions of AODEs - Existence, Uniqueness, Convergence and Computation

#### S. Falkensteiner

RISC Hagenberg, Johannes Kepler University Linz. PhD Thesis. June 2020. Also available as RISC report no. 20-13. [pdf]@

author = {S. Falkensteiner},

title = {{Power Series Solutions of AODEs - Existence, Uniqueness, Convergence and Computation}},

language = {english},

year = {2020},

month = {June},

note = {Also available as RISC report no. 20-13},

translation = {0},

school = {RISC Hagenberg, Johannes Kepler University Linz},

length = {146}

}

**phdthesis**{RISC6120,author = {S. Falkensteiner},

title = {{Power Series Solutions of AODEs - Existence, Uniqueness, Convergence and Computation}},

language = {english},

year = {2020},

month = {June},

note = {Also available as RISC report no. 20-13},

translation = {0},

school = {RISC Hagenberg, Johannes Kepler University Linz},

length = {146}

}

### The Integration of SMT Solvers into the RISCAL Model Checker

#### Franz-Xaver Reichl

Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. Master Thesis. April 2020. [pdf]@

author = {Franz-Xaver Reichl},

title = {{The Integration of SMT Solvers into the RISCAL Model Checker}},

language = {english},

abstract = {In this thesis we present an alternative approach to check specifications from asubstantial subset of the RISC Algorithm Language (RISCAL). The main goal forthis new approach is to speed up checks done in RISCAL. For this purpose wedeveloped a translation from the RISCAL language to the SMT-LIB language (usingthe QF_UFBV logic). The realisation of this translation in particular required to solvethe problems of eliminating RISCAL’s quantifiers and of encoding RISCAL’s typesand operations. We formally described core components of this translation, provedsome aspects of their correctness, and implemented it in the programming languageJava. We tested the implementation together with the SMT solvers Boolector, CVC4,Yices and Z3, on several real world RISCAL specifications. Additionally, we evaluatedthe performance of our approach by systematic benchmarks and compared it withthat of the original RISCAL checking mechanism. Finally, we analysed the testsin order to determine patterns in specifications that could possibly have a negativeinfluence on the performance of the presented method. The tests showed that amongthe four used SMT solvers, the solver Yices delivered, for almost all, tests the bestresults. Additionally, the tests indicated that the translation is indeed a viablealternative to RISCAL’s current checking method, especially when used togetherwith Yices. So the translation used with Yices was substantially faster than RISCALin approximately 75% of the test cases. Nevertheless, the tests also illustrated thatRISCAL could still check certain test cases substantially faster. Thus, the translationcannot fully replace RISCAL’s current checking methods.},

year = {2020},

month = {April},

translation = {0},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria},

keywords = {formal methods, automated reasoning, model checking, program verification},

sponsor = {Johannes Kepler University, Linz, Institute of Technology(LIT) project LOGTECHEDU.},

length = {151}

}

**misc**{RISC6103,author = {Franz-Xaver Reichl},

title = {{The Integration of SMT Solvers into the RISCAL Model Checker}},

language = {english},

abstract = {In this thesis we present an alternative approach to check specifications from asubstantial subset of the RISC Algorithm Language (RISCAL). The main goal forthis new approach is to speed up checks done in RISCAL. For this purpose wedeveloped a translation from the RISCAL language to the SMT-LIB language (usingthe QF_UFBV logic). The realisation of this translation in particular required to solvethe problems of eliminating RISCAL’s quantifiers and of encoding RISCAL’s typesand operations. We formally described core components of this translation, provedsome aspects of their correctness, and implemented it in the programming languageJava. We tested the implementation together with the SMT solvers Boolector, CVC4,Yices and Z3, on several real world RISCAL specifications. Additionally, we evaluatedthe performance of our approach by systematic benchmarks and compared it withthat of the original RISCAL checking mechanism. Finally, we analysed the testsin order to determine patterns in specifications that could possibly have a negativeinfluence on the performance of the presented method. The tests showed that amongthe four used SMT solvers, the solver Yices delivered, for almost all, tests the bestresults. Additionally, the tests indicated that the translation is indeed a viablealternative to RISCAL’s current checking method, especially when used togetherwith Yices. So the translation used with Yices was substantially faster than RISCALin approximately 75% of the test cases. Nevertheless, the tests also illustrated thatRISCAL could still check certain test cases substantially faster. Thus, the translationcannot fully replace RISCAL’s current checking methods.},

year = {2020},

month = {April},

translation = {0},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria},

keywords = {formal methods, automated reasoning, model checking, program verification},

sponsor = {Johannes Kepler University, Linz, Institute of Technology(LIT) project LOGTECHEDU.},

length = {151}

}

### Modelling and Solving a Scheduling Problem by Max-Flow

#### Moritz Willnauer

RISC Institute, JKU Linz. Bachelor Thesis. March 2020. [pdf]@

author = {Moritz Willnauer},

title = {{Modelling and Solving a Scheduling Problem by Max-Flow}},

language = {english},

abstract = {This thesis shows how to specify and solve a specific scheduling problem of workgroups and loading orders. The sections on graph theory and network flows give support to understand the necessary definitions for modelling the scheduling problem as a network problem. For solving the resulting Max-Flow-Problem three different algorithms are presented. Two of them were implemented and tested with Mathematica to analyze their performance. To do this an auxiliary algorithm for finding a shortest path for the modelled network of a scheduling problem was developed. Finally, a pretty complex problem was solved by using Mathematica.},

year = {2020},

month = {March},

translation = {0},

institution = {RISC Institute, JKU Linz},

length = {51}

}

**misc**{RISC6194,author = {Moritz Willnauer},

title = {{Modelling and Solving a Scheduling Problem by Max-Flow}},

language = {english},

abstract = {This thesis shows how to specify and solve a specific scheduling problem of workgroups and loading orders. The sections on graph theory and network flows give support to understand the necessary definitions for modelling the scheduling problem as a network problem. For solving the resulting Max-Flow-Problem three different algorithms are presented. Two of them were implemented and tested with Mathematica to analyze their performance. To do this an auxiliary algorithm for finding a shortest path for the modelled network of a scheduling problem was developed. Finally, a pretty complex problem was solved by using Mathematica.},

year = {2020},

month = {March},

translation = {0},

institution = {RISC Institute, JKU Linz},

length = {51}

}

### Eine industrielle Anwendung von heuristischen Optimierungsverfahren für das Bin-Packing Problem

#### Ingolf Neumüller

RISC Institute, JKU Linz. Master Thesis. September 2020. [pdf]@

author = {Ingolf Neumüller},

title = {{Eine industrielle Anwendung von heuristischen Optimierungsverfahren für das Bin-Packing Problem}},

language = {german},

year = {2020},

month = {September},

translation = {0},

institution = {RISC Institute, JKU Linz},

length = {95}

}

**misc**{RISC6208,author = {Ingolf Neumüller},

title = {{Eine industrielle Anwendung von heuristischen Optimierungsverfahren für das Bin-Packing Problem}},

language = {german},

year = {2020},

month = {September},

translation = {0},

institution = {RISC Institute, JKU Linz},

length = {95}

}

### Strong Rational General Solutions of AODEs using Optimal Curve Parametrization

#### Lukas Weigert

Research Institute for Symbolic Computation. Master Thesis. April 2020. [pdf]@

author = {Lukas Weigert},

title = {{Strong Rational General Solutions of AODEs using Optimal Curve Parametrization}},

language = {english},

abstract = {The aim of this thesis is to implement an algorithm that finds rational solutions of first-order algebraic ordinary differential equations (AODEs). We are interested in the general solution that depends on a transcendental constant.To tackle this problem, a geometric approach is used. We neglect the differential aspect and consider the derivative as new variable. This leads to an algebraic equation. So we consider the AODE as an algebraic curve, in which the coefficients are rational functions. We have to compute the rational parametrization of the obtained curve. Since we look for rational solutions, we also require the coefficients of the parametrization to be rational. Every curve over the field of rational functions admits such a parametrization. Therefore, the key notion is optimal parametrization.For parametrizing over the rational numbers, there are already implementations available. But these are not applicable for our problem, since they require field extensions. So we have to construct a new implementation.Our goal is to decide whether the AODE has a rational general solution and in the affirmative case compute it. To do so, we have to modify the problem and search for solutions where also the arbitrary constant appears rationally. Such a solution is called strong rational general solution. Thus, we achieve a decision algorithm.},

year = {2020},

month = {April},

translation = {0},

institution = {Research Institute for Symbolic Computation},

keywords = {differential equation, general solution, parametrization},

length = {78}

}

**misc**{RISC6198,author = {Lukas Weigert},

title = {{Strong Rational General Solutions of AODEs using Optimal Curve Parametrization}},

language = {english},

abstract = {The aim of this thesis is to implement an algorithm that finds rational solutions of first-order algebraic ordinary differential equations (AODEs). We are interested in the general solution that depends on a transcendental constant.To tackle this problem, a geometric approach is used. We neglect the differential aspect and consider the derivative as new variable. This leads to an algebraic equation. So we consider the AODE as an algebraic curve, in which the coefficients are rational functions. We have to compute the rational parametrization of the obtained curve. Since we look for rational solutions, we also require the coefficients of the parametrization to be rational. Every curve over the field of rational functions admits such a parametrization. Therefore, the key notion is optimal parametrization.For parametrizing over the rational numbers, there are already implementations available. But these are not applicable for our problem, since they require field extensions. So we have to construct a new implementation.Our goal is to decide whether the AODE has a rational general solution and in the affirmative case compute it. To do so, we have to modify the problem and search for solutions where also the arbitrary constant appears rationally. Such a solution is called strong rational general solution. Thus, we achieve a decision algorithm.},

year = {2020},

month = {April},

translation = {0},

institution = {Research Institute for Symbolic Computation},

keywords = {differential equation, general solution, parametrization},

length = {78}

}

### 2019

### Some Problems in Analytic Number Theory

#### Ankush Goswami

University of Florida. PhD Thesis. 2019. First part of this thesis is to appear in Proceedings of Analytic and Combinatorial Number Theory: The Legacy of Ramanujan - A CONFERENCE IN HONOR OF BRUCE C. BERNDT'S 80TH BIRTHDAY.@

author = {Ankush Goswami},

title = {{Some Problems in Analytic Number Theory}},

language = {english},

year = {2019},

note = {First part of this thesis is to appear in Proceedings of Analytic and Combinatorial Number Theory: The Legacy of Ramanujan -- A CONFERENCE IN HONOR OF BRUCE C. BERNDT'S 80TH BIRTHDAY},

translation = {0},

school = {University of Florida},

length = {90}

}

**phdthesis**{RISC5961,author = {Ankush Goswami},

title = {{Some Problems in Analytic Number Theory}},

language = {english},

year = {2019},

note = {First part of this thesis is to appear in Proceedings of Analytic and Combinatorial Number Theory: The Legacy of Ramanujan -- A CONFERENCE IN HONOR OF BRUCE C. BERNDT'S 80TH BIRTHDAY},

translation = {0},

school = {University of Florida},

length = {90}

}

### Flexible and Rigid Labelings of Graphs

#### Jan Legerský

Research Institute for Symbolic Computation, Johannes Kepler University Linz. PhD Thesis. 2019. [url] [pdf]@

author = {Jan Legerský},

title = {{Flexible and Rigid Labelings of Graphs}},

language = {english},

year = {2019},

translation = {0},

school = {Research Institute for Symbolic Computation, Johannes Kepler University Linz},

length = {108},

url = {https://jan.legersky.cz/project/movablegraphs/}

}

**phdthesis**{RISC5941,author = {Jan Legerský},

title = {{Flexible and Rigid Labelings of Graphs}},

language = {english},

year = {2019},

translation = {0},

school = {Research Institute for Symbolic Computation, Johannes Kepler University Linz},

length = {108},

url = {https://jan.legersky.cz/project/movablegraphs/}

}

### Difference Ring Algorithms for Nested Products

#### Evans Doe Ocansey

RISC, Johannes Kepler University. PhD Thesis. November 2019. [pdf]@

author = {Evans Doe Ocansey},

title = {{Difference Ring Algorithms for Nested Products}},

language = {english},

year = {2019},

month = {November},

translation = {0},

school = {RISC, Johannes Kepler University},

length = {178}

}

**phdthesis**{RISC6199,author = {Evans Doe Ocansey},

title = {{Difference Ring Algorithms for Nested Products}},

language = {english},

year = {2019},

month = {November},

translation = {0},

school = {RISC, Johannes Kepler University},

length = {178}

}

### A Parallel, In-Place, Rectangular Matrix Transpose Algorithm

#### Stefan Amberger

Research Institute for Symbolic Computatation (RISC), Johannes Kepler University, Linz, Austria. Master Thesis. March 2019. [pdf]@

author = {Stefan Amberger},

title = {{A Parallel, In-Place, Rectangular Matrix Transpose Algorithm}},

language = {english},

abstract = {This thesis presents a novel algorithm for Transposing Rectangular matrices In-place and in Parallel(TRIP) including a proof of correctness and an analysis of work, span and parallelism.After almost 60 years since its introduction, the problem of in-place rectangular matrix transpositionstill does not have a satisfying solution. Increased concurrency in today's computers, and the need for low overhead algorithms to solve memory-intense challenges are motivating the development of algorithmslike TRIP. The algorithm is based on recursive splitting of the matrix into sub-matrices, independent, paralleltransposition of these sub-matrices, and subsequent combining of the results by a parallel, perfect shuffle.We prove correctness of the algorithm for different matrix shapes (ratios of dimensions), and analyzework and span . Compared to out-of-place algorithms, TRIP, implemented in Cilk, trades work-efficiency for parallelism and for being in-place.},

year = {2019},

month = {March},

translation = {0},

institution = {Research Institute for Symbolic Computatation (RISC), Johannes Kepler University, Linz, Austria},

keywords = {linear algebra, parallel computation},

length = {67}

}

**misc**{RISC5916,author = {Stefan Amberger},

title = {{A Parallel, In-Place, Rectangular Matrix Transpose Algorithm}},

language = {english},

abstract = {This thesis presents a novel algorithm for Transposing Rectangular matrices In-place and in Parallel(TRIP) including a proof of correctness and an analysis of work, span and parallelism.After almost 60 years since its introduction, the problem of in-place rectangular matrix transpositionstill does not have a satisfying solution. Increased concurrency in today's computers, and the need for low overhead algorithms to solve memory-intense challenges are motivating the development of algorithmslike TRIP. The algorithm is based on recursive splitting of the matrix into sub-matrices, independent, paralleltransposition of these sub-matrices, and subsequent combining of the results by a parallel, perfect shuffle.We prove correctness of the algorithm for different matrix shapes (ratios of dimensions), and analyzework and span . Compared to out-of-place algorithms, TRIP, implemented in Cilk, trades work-efficiency for parallelism and for being in-place.},

year = {2019},

month = {March},

translation = {0},

institution = {Research Institute for Symbolic Computatation (RISC), Johannes Kepler University, Linz, Austria},

keywords = {linear algebra, parallel computation},

length = {67}

}

### Migrating Mathematical Programs to Web Interface Frameworks

#### Hsuan-Ming Chen

Research Institute for Symbolic Computatation (RISC), Johannes Kepler University, Linz, Austria. Master Thesis. April 2019. Internationaler Universitätslehrgang: Informatics: Engineering & Management. [pdf]@

author = {Hsuan-Ming Chen},

title = {{Migrating Mathematical Programs to Web Interface Frameworks}},

language = {english},

abstract = {A mathematical software system, the RISC Algorithm Language (RISCAL), has beenimplemented in Java; however, it can be only executed on the local machine of the user.The aim of this master thesis is to migrate RISCAL to the web, such that users can accessthe software via a conventional web browser without needing a local installation of thesoftware. In a preparatory phase, this thesis evaluates various web interface frameworksand how these can be executed on the web. Based in the result of this investigation whichcompares the advantages and disadvantages of the frameworks, one framework is selectedas the most promising candidate for future work. The core of the thesis is then themigration of RISCAL to the web on the basis of this framework and the subsequentevaluation of how the demands have been met and how well all of the RISCAL programsare working after the migration.},

year = {2019},

month = {April},

note = {Internationaler Universitätslehrgang: Informatics: Engineering & Management},

translation = {0},

institution = {Research Institute for Symbolic Computatation (RISC), Johannes Kepler University, Linz, Austria},

length = {85}

}

**misc**{RISC5917,author = {Hsuan-Ming Chen},

title = {{Migrating Mathematical Programs to Web Interface Frameworks}},

language = {english},

abstract = {A mathematical software system, the RISC Algorithm Language (RISCAL), has beenimplemented in Java; however, it can be only executed on the local machine of the user.The aim of this master thesis is to migrate RISCAL to the web, such that users can accessthe software via a conventional web browser without needing a local installation of thesoftware. In a preparatory phase, this thesis evaluates various web interface frameworksand how these can be executed on the web. Based in the result of this investigation whichcompares the advantages and disadvantages of the frameworks, one framework is selectedas the most promising candidate for future work. The core of the thesis is then themigration of RISCAL to the web on the basis of this framework and the subsequentevaluation of how the demands have been met and how well all of the RISCAL programsare working after the migration.},

year = {2019},

month = {April},

note = {Internationaler Universitätslehrgang: Informatics: Engineering & Management},

translation = {0},

institution = {Research Institute for Symbolic Computatation (RISC), Johannes Kepler University, Linz, Austria},

length = {85}

}

### 2018

### A Gateway for the Generic Conversion of Protocols for Smart Meters and IoT Applications

#### Ramez Elbaroudy

Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Master Thesis. July 2018. [pdf]@

author = {Ramez Elbaroudy},

title = {{A Gateway for the Generic Conversion of Protocols for Smart Meters and IoT Applications}},

language = {english},

abstract = {In the recent years the number of Internet of things (IoT) devices have increased in a remarkable way.Due to this increase of devices many challenges have appeared. One of the most markable challenge isinteroperability challenge, where devices use different standards, protocols and conventions to exchangeinformation. This challenge has appeared because of the different devices’ specifications and the differentmanufacturers of the different types of IoT devices. The current thesis proposes a generic API that canbe used for communication with different IoT devices, which use different conventions and protocols;understanding the underlying conventions or protocols used. In this thesis, we used smart meters as theIoT devices for testing the generic API. The generic API is first described in an abstract way; then wedescribe the Java binding in order to use the API with the Java programming language. The implementedgeneric API enables developers to communicate with different IoT devices without the need of knowing thespecification of each protocol. The current thesis can be considered as an important point of extendingthe research field of interoperability of IoT devices. Furthermore, the generic API can be extended inorder to support other types of protocols and conventions.},

year = {2018},

month = {July},

translation = {0},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},

length = {85}

}

**misc**{RISC5727,author = {Ramez Elbaroudy},

title = {{A Gateway for the Generic Conversion of Protocols for Smart Meters and IoT Applications}},

language = {english},

abstract = {In the recent years the number of Internet of things (IoT) devices have increased in a remarkable way.Due to this increase of devices many challenges have appeared. One of the most markable challenge isinteroperability challenge, where devices use different standards, protocols and conventions to exchangeinformation. This challenge has appeared because of the different devices’ specifications and the differentmanufacturers of the different types of IoT devices. The current thesis proposes a generic API that canbe used for communication with different IoT devices, which use different conventions and protocols;understanding the underlying conventions or protocols used. In this thesis, we used smart meters as theIoT devices for testing the generic API. The generic API is first described in an abstract way; then wedescribe the Java binding in order to use the API with the Java programming language. The implementedgeneric API enables developers to communicate with different IoT devices without the need of knowing thespecification of each protocol. The current thesis can be considered as an important point of extendingthe research field of interoperability of IoT devices. Furthermore, the generic API can be extended inorder to support other types of protocols and conventions.},

year = {2018},

month = {July},

translation = {0},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},

length = {85}

}

### Das Shifting-Bottleneck Verfahren für das Job-Shop Scheduling-Problem

#### M. Schlenkrich

JKU Linz. Bachelor Thesis. September 2018. [pdf]@

author = {M. Schlenkrich},

title = {{Das Shifting-Bottleneck Verfahren für das Job-Shop Scheduling-Problem}},

language = {deutsch},

abstract = {Schedulingprobleme treten in unserer Welt in den verschiedensten Bereichen auf.Egal ob in Krankenhäusern bei der Zuteilung von Patienten zu Behandlungs-räumen, in Tischlereien und anderen Manufakturen bei der Abfolge von Ar-beitsschritten auf Maschinen oder der Nutzung von Schienentrassen im Bahn-verkehr. Das Lösen dieser Ablaufplanungsprobleme ist oftmals essentiell, umeinen reibungsfreien Arbeitsalltag garantieren zu können oder um Produktions-prozesse zu optimieren.Eine besonders häufig auftretende Variante dieser Schedulingprobleme istdas sogenannte Job-Shop Ablaufplanungsproblem, bei dem die Aufträge aufallen zur Verfügung stehenden Ressourcen in einer definierten Reihenfolge be-arbeitet werden müssen. Für große Problemdaten mit einer hohen Anzahl anAufträgen und Maschinen ist das Lösen dieser Probleme sehr aufwändig und immathematisch-wissenschaftlichen Bereich noch nicht zur Gänze erforscht.Eine Methode zur Lösung dieser Problemklasse ist die Shifting-BottleneckHeuristik. Wie der Name schon verrät, handelt es sich dabei nicht um ein exaktesVerfahren, sondern um eine Heuristik, die zwar eine zulässige Lösung liefert, diesjedoch nicht unbedingt das Optimum sein muss. In der Regel sind die Lösungendieses Verfahrens jedoch sehr gute Näherungen.Dieses Verfahren löst mehrere kleinere Hilfsprobleme und gelangt nach mIterationen zu einem Ergebnis, wobei m die Anzahl der Ressourcen bzw. Ma-schinen ist. Das Lösen dieser Hilfsprobleme geschieht zwar exakt, was Zeit undRechenaufwand kostet, diese sind jedoch um einiges einfacher zu lösen als dasGesamtproblem und somit bleibt der Aufwand in einem akzeptablen Rahmen.Die Basisversion der Shifting-Bottleneck Heuristik wurde im Rahmen dieserArbeit in Python implementiert und mit Benchmarkproblemdaten aus der Li-teratur getestet.},

year = {2018},

month = {September},

translation = {0},

institution = {JKU Linz},

length = {36}

}

**misc**{RISC5874,author = {M. Schlenkrich},

title = {{Das Shifting-Bottleneck Verfahren für das Job-Shop Scheduling-Problem}},

language = {deutsch},

abstract = {Schedulingprobleme treten in unserer Welt in den verschiedensten Bereichen auf.Egal ob in Krankenhäusern bei der Zuteilung von Patienten zu Behandlungs-räumen, in Tischlereien und anderen Manufakturen bei der Abfolge von Ar-beitsschritten auf Maschinen oder der Nutzung von Schienentrassen im Bahn-verkehr. Das Lösen dieser Ablaufplanungsprobleme ist oftmals essentiell, umeinen reibungsfreien Arbeitsalltag garantieren zu können oder um Produktions-prozesse zu optimieren.Eine besonders häufig auftretende Variante dieser Schedulingprobleme istdas sogenannte Job-Shop Ablaufplanungsproblem, bei dem die Aufträge aufallen zur Verfügung stehenden Ressourcen in einer definierten Reihenfolge be-arbeitet werden müssen. Für große Problemdaten mit einer hohen Anzahl anAufträgen und Maschinen ist das Lösen dieser Probleme sehr aufwändig und immathematisch-wissenschaftlichen Bereich noch nicht zur Gänze erforscht.Eine Methode zur Lösung dieser Problemklasse ist die Shifting-BottleneckHeuristik. Wie der Name schon verrät, handelt es sich dabei nicht um ein exaktesVerfahren, sondern um eine Heuristik, die zwar eine zulässige Lösung liefert, diesjedoch nicht unbedingt das Optimum sein muss. In der Regel sind die Lösungendieses Verfahrens jedoch sehr gute Näherungen.Dieses Verfahren löst mehrere kleinere Hilfsprobleme und gelangt nach mIterationen zu einem Ergebnis, wobei m die Anzahl der Ressourcen bzw. Ma-schinen ist. Das Lösen dieser Hilfsprobleme geschieht zwar exakt, was Zeit undRechenaufwand kostet, diese sind jedoch um einiges einfacher zu lösen als dasGesamtproblem und somit bleibt der Aufwand in einem akzeptablen Rahmen.Die Basisversion der Shifting-Bottleneck Heuristik wurde im Rahmen dieserArbeit in Python implementiert und mit Benchmarkproblemdaten aus der Li-teratur getestet.},

year = {2018},

month = {September},

translation = {0},

institution = {JKU Linz},

length = {36}

}

### Formalization and Validation of Fundamental Sequence Algorithms by Computer-assisted Checking of Finite Models

#### Lucas Payr

Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Bachelor Thesis. December 2018. [pdf]@

author = {Lucas Payr},

title = {{Formalization and Validation of Fundamental Sequence Algorithms by Computer-assisted Checking of Finite Models}},

language = {english},

abstract = {While common textbooks go into great details when it comes to the analy-sis of sequence algorithms, they lack in proper proofs and moreover formalspecifications. The most essential part, the loop invariant is either describedvery vaguely or is completely missing. This thesis gives those missing spec-ifications as well as so called verification conditions upon which one canfully prove an algorithm. Normally such a process is very difficult and it iseasy to wrongly specify an algorithm. With the help of the RISC AlgorithmLanguage (RISCAL), developed at the Research Institute for Symbolic Com-putation (RISC), this process is simpler as this system provides additionalchecks that help noticing early if a specification is wrong. It uses finitemodel checking, which makes it possible to check the adequacy of speci-fications even if they include general quantifiers, which would be difficultinfinite models.The result of the thesis is a collection of specifications for various search-ing and sorting algorithms. The algorithms are implemented for differentdata types (array, recursive lists, pointer-linked lists) to serve as an additionto common textbooks.},

year = {2018},

month = {December},

translation = {0},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},

keywords = {formal methods, specification, verification, model checking},

sponsor = {Supported by the Johannes Kepler University, Linz, Institute of Technology(LIT) project LOGTECHEDU "Logic Technologies for Computer Science Education"},

length = {85}

}

**misc**{RISC6125,author = {Lucas Payr},

title = {{Formalization and Validation of Fundamental Sequence Algorithms by Computer-assisted Checking of Finite Models}},

language = {english},

abstract = {While common textbooks go into great details when it comes to the analy-sis of sequence algorithms, they lack in proper proofs and moreover formalspecifications. The most essential part, the loop invariant is either describedvery vaguely or is completely missing. This thesis gives those missing spec-ifications as well as so called verification conditions upon which one canfully prove an algorithm. Normally such a process is very difficult and it iseasy to wrongly specify an algorithm. With the help of the RISC AlgorithmLanguage (RISCAL), developed at the Research Institute for Symbolic Com-putation (RISC), this process is simpler as this system provides additionalchecks that help noticing early if a specification is wrong. It uses finitemodel checking, which makes it possible to check the adequacy of speci-fications even if they include general quantifiers, which would be difficultinfinite models.The result of the thesis is a collection of specifications for various search-ing and sorting algorithms. The algorithms are implemented for differentdata types (array, recursive lists, pointer-linked lists) to serve as an additionto common textbooks.},

year = {2018},

month = {December},

translation = {0},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},

keywords = {formal methods, specification, verification, model checking},

sponsor = {Supported by the Johannes Kepler University, Linz, Institute of Technology(LIT) project LOGTECHEDU "Logic Technologies for Computer Science Education"},

length = {85}

}

### 2017

### An Online Auction System for Selling Fiber Products

#### C. Ilonka

ISI Hagenberg, JKU Linz. Master Thesis. July 2017. [pdf]@

author = {C. Ilonka},

title = {{An Online Auction System for Selling Fiber Products}},

language = {english},

abstract = {The thesis presents the design and development of the Lenzing Global Auction Portalproject. The Lenzing Global Auction Portal is a software system for running multiplesimultaneous online auctions. The system implements the Dutch auction model, butprovides the means to integrate different auction models as well.The system is based on the Client/Server architecture model. The server-side follows themicroservice based architecture model combined with the multi-layer architecture model.The client-side consists of two mobile-first web applications following the single-pageapplication principle.},

year = {2017},

month = {July},

translation = {0},

institution = {ISI Hagenberg, JKU Linz},

length = {60}

}

**misc**{RISC5873,author = {C. Ilonka},

title = {{An Online Auction System for Selling Fiber Products}},

language = {english},

abstract = {The thesis presents the design and development of the Lenzing Global Auction Portalproject. The Lenzing Global Auction Portal is a software system for running multiplesimultaneous online auctions. The system implements the Dutch auction model, butprovides the means to integrate different auction models as well.The system is based on the Client/Server architecture model. The server-side follows themicroservice based architecture model combined with the multi-layer architecture model.The client-side consists of two mobile-first web applications following the single-pageapplication principle.},

year = {2017},

month = {July},

translation = {0},

institution = {ISI Hagenberg, JKU Linz},

length = {60}

}

### Validating the Formalization of Theories and Algorithms of Discrete Mathematics by the Computer-Supported Checking of Finite Models

#### Alexander Brunhuemer

Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Bachelor Thesis. September 2017. [pdf]@

author = {Alexander Brunhuemer},

title = {{Validating the Formalization of Theories and Algorithms of Discrete Mathematics by the Computer-Supported Checking of Finite Models}},

language = {english},

abstract = {The goal of this Bachelor’s thesis is the formal specification and implementation of centraltheories and algorithms in the field of discrete mathematics by using the RISC AlgorithmLanguage (RISCAL), developed at the Research Institute for Symbolic Computation (RISC).This specification language and associated software system allow the verification of specifications,by using the concept of finite model checking. Validation on finite models is intendedto serve as a foundation layer for further research on the corresponding generalized theorieson infinite models.This thesis results in a collection of specifications of exemplarily chosen formalized algorithmsof set theory, relation and function theory and graph theory. The algorithms arespecified in different ways (implicit, recursive and procedural), to emphasize the correspondingconnections between them.The evaluation and validation of implemented theories is demonstrated on Dijkstra’s algorithmfor finding a shortest path between vertices in a graph.},

year = {2017},

month = {September},

translation = {0},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},

length = {88}

}

**misc**{RISC6126,author = {Alexander Brunhuemer},

title = {{Validating the Formalization of Theories and Algorithms of Discrete Mathematics by the Computer-Supported Checking of Finite Models}},

language = {english},

abstract = {The goal of this Bachelor’s thesis is the formal specification and implementation of centraltheories and algorithms in the field of discrete mathematics by using the RISC AlgorithmLanguage (RISCAL), developed at the Research Institute for Symbolic Computation (RISC).This specification language and associated software system allow the verification of specifications,by using the concept of finite model checking. Validation on finite models is intendedto serve as a foundation layer for further research on the corresponding generalized theorieson infinite models.This thesis results in a collection of specifications of exemplarily chosen formalized algorithmsof set theory, relation and function theory and graph theory. The algorithms arespecified in different ways (implicit, recursive and procedural), to emphasize the correspondingconnections between them.The evaluation and validation of implemented theories is demonstrated on Dijkstra’s algorithmfor finding a shortest path between vertices in a graph.},

year = {2017},

month = {September},

translation = {0},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},

length = {88}

}

### Complex Analysis Based Computer Algebra Algorithms for Proving Jacobi Theta Function Identities

#### Liangjie Ye

RISC and the DK program Linz. PhD Thesis. 2017. Updated version in June 2017. [pdf]@

author = {Liangjie Ye},

title = {{Complex Analysis Based Computer Algebra Algorithms for Proving Jacobi Theta Function Identities}},

language = {english},

year = {2017},

note = {Updated version in June 2017},

translation = {0},

school = {RISC and the DK program Linz},

length = {122}

}

**phdthesis**{RISC5463,author = {Liangjie Ye},

title = {{Complex Analysis Based Computer Algebra Algorithms for Proving Jacobi Theta Function Identities}},

language = {english},

year = {2017},

note = {Updated version in June 2017},

translation = {0},

school = {RISC and the DK program Linz},

length = {122}

}

### 2016

### Axiomatic Description of Gröbner Reduction

#### Christoph Fuerst

RISC, JKU Linz. PhD Thesis. December 2016. [pdf]@

author = {Christoph Fuerst},

title = {{Axiomatic Description of Gröbner Reduction}},

language = {english},

year = {2016},

month = {December},

translation = {0},

school = {RISC, JKU Linz},

length = {154}

}

**phdthesis**{RISC5388,author = {Christoph Fuerst},

title = {{Axiomatic Description of Gröbner Reduction}},

language = {english},

year = {2016},

month = {December},

translation = {0},

school = {RISC, JKU Linz},

length = {154}

}

### Algebraic Geometry methods in Kinematics: Mobile Pods

#### Matteo Gallet

Johannes Kepler University. PhD Thesis. October 2016.@

author = {Matteo Gallet},

title = {{Algebraic Geometry methods in Kinematics: Mobile Pods}},

language = {English},

year = {2016},

month = {October},

translation = {0},

school = {Johannes Kepler University},

length = {82}

}

**phdthesis**{RISC5393,author = {Matteo Gallet},

title = {{Algebraic Geometry methods in Kinematics: Mobile Pods}},

language = {English},

year = {2016},

month = {October},

translation = {0},

school = {Johannes Kepler University},

length = {82}

}

### Computer-Assisted Exploration of Gröbner Bases Theory in Theorema

#### A. Maletzky

RISC, Johannes Kepler University Linz. PhD Thesis. May 2016.@

author = {A. Maletzky},

title = {{Computer-Assisted Exploration of Gröbner Bases Theory in Theorema}},

language = {english},

year = {2016},

month = {May},

translation = {0},

school = {RISC, Johannes Kepler University Linz},

length = {197}

}

**phdthesis**{RISC5361,author = {A. Maletzky},

title = {{Computer-Assisted Exploration of Gröbner Bases Theory in Theorema}},

language = {english},

year = {2016},

month = {May},

translation = {0},

school = {RISC, Johannes Kepler University Linz},

length = {197}

}

### Formally Modeling and Analyzing Mathematical Algorithms with Software Specification Languages & Tools

#### Daniela Ritirc

Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Master Thesis. January 2016. [pdf]@

author = {Daniela Ritirc},

title = {{Formally Modeling and Analyzing Mathematical Algorithms with Software Specification Languages & Tools}},

language = {english},

abstract = {In this thesis the behaviour of software specification languages and tools on mathematicalalgorithms shall be investigated. The main goal is to investigate how tools which havebeen designed for modeling and analyzing software in other application contexts can beapplied to mathematical algorithms. For this purpose, two different mathematical algorithms,namely the DPLL method and Dijkstra’s Shortest Path Algorithm are selected.Furthermore five well-known software specification languages are selected: JML, Alloy,TLA/PlusCal, VDM and Event-B. It shall be examined how far the algorithms can bemodeled and how far model checking respectively verification succeeds. The goal of thethesis is not a proper verification/check of every model with every tool but a survey ofthe potential as well as the difficulties of the usage of software specification languagesfor the analysis of mathematical algorithms.As a starting point for each algorithm a formal specification is derived and the algorithmsare supplied in pseudo-code. A Java prototype is implemented for each algorithmwhich is then specified by JML annotations. Furthermore the algorithms are modelled inTLA/PlusCal, Alloy, VDM and Event-B and for each language the appropriate analysissupported by the tool is selected (visualizing, model checking, verification).The main result of the thesis is that each tool shows some success when it is usedfor specifying and analyzing mathematical algorithms, because modeling the algorithmssucceeded in every language. In TLA, VDM and Alloy it was possible to completelymodel check the specifications. Furthermore it was possible to visualize the algorithmsin Alloy. In JML and Event-B it was possible to verify major parts of the model;},

year = {2016},

month = {January},

translation = {0},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},

keywords = {formal methods, model checking, program verification},

length = {167}

}

**misc**{RISC5224,author = {Daniela Ritirc},

title = {{Formally Modeling and Analyzing Mathematical Algorithms with Software Specification Languages & Tools}},

language = {english},

abstract = {In this thesis the behaviour of software specification languages and tools on mathematicalalgorithms shall be investigated. The main goal is to investigate how tools which havebeen designed for modeling and analyzing software in other application contexts can beapplied to mathematical algorithms. For this purpose, two different mathematical algorithms,namely the DPLL method and Dijkstra’s Shortest Path Algorithm are selected.Furthermore five well-known software specification languages are selected: JML, Alloy,TLA/PlusCal, VDM and Event-B. It shall be examined how far the algorithms can bemodeled and how far model checking respectively verification succeeds. The goal of thethesis is not a proper verification/check of every model with every tool but a survey ofthe potential as well as the difficulties of the usage of software specification languagesfor the analysis of mathematical algorithms.As a starting point for each algorithm a formal specification is derived and the algorithmsare supplied in pseudo-code. A Java prototype is implemented for each algorithmwhich is then specified by JML annotations. Furthermore the algorithms are modelled inTLA/PlusCal, Alloy, VDM and Event-B and for each language the appropriate analysissupported by the tool is selected (visualizing, model checking, verification).The main result of the thesis is that each tool shows some success when it is usedfor specifying and analyzing mathematical algorithms, because modeling the algorithmssucceeded in every language. In TLA, VDM and Alloy it was possible to completelymodel check the specifications. Furthermore it was possible to visualize the algorithmsin Alloy. In JML and Event-B it was possible to verify major parts of the model;},

year = {2016},

month = {January},

translation = {0},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},

keywords = {formal methods, model checking, program verification},

length = {167}

}