Theses

See some of the topics offered at RISC for a bachelor/master/PhD thesis. This list is not comprehensive, other topics are also possible. In case there is no suitable topic for you in the list then please contact any of the RISC Faculty directly.

Open Topics

Further development and use of the unification and generalization algorithm library (Advisor: Teimuraz Kutsia). At RISC, we have been developing an open source library of unification and generalization algorithms, currently hosted at http://www.risc.jku.at/projects/stout/ Unification is a process of equation solving, aiming at computing a most general common instance of the terms involved. Anti-unification is its dual process, aiming at computing a least general common generalization of the input terms (retaining their common structure as much as possible). The topics are for one or more bachelor theses: Extend the library by implementing recently developed improvements of some of the algorithms already in the library; add a new algorithm for term-graph generalization; add an algorithm for context sequence matching with regular constraints; experimental applications. Prerequisites: Programming in Java (since the library is written in Java), basic knowledge of logic, some familiarity with declarative programming and automated reasoning is a plus.

Gelenkmechanismen

Bachelor Thesis
Advisor: Josef Schicho
Gelenkmechanismen (Advisor: Josef Schicho). Man konstruiere Familien von Bennett-Mechanismen, die eine vollständige Drehung ohne Kollisionen zulassen.

Hamilton-Mechanik

Bachelor Thesis
Advisor: Josef Schicho
Hamilton-Mechanik (Advisor: Josef Schicho). Man beschreibe die Bewegung zweier fester Körper, die durch ein Drehgelenk miteinander verbunden sind, ohne Einwirkung äußerer Kräfte.
Symbolic computation and positivity of holonomic sequences (Advisor: Veronika Pillwein). Around ten years ago Stefan Gerhold and Manuel Kauers developed a symbolic method to show positivity for sequences defined by a linear recurrence relation with polynomial coefficients. More recently, in the course of a termination analysis, a variation of this method has been introduced. The goal of this thesis is to implement this new procedure in Mathematica and compare its behaviour at some practical examples with the existing implementation of the Gerhold-Kauers method.
Theorema Project: Document Processing (Advisor: Wolfgang Windsteiger). The task in this thesis is to setup an environment for preparing entire (big) mathematical documents in Theorema 2.0. This comprises the design of appropriate Mathematica stylesheets and a mechanism for translating Mathematica notebooks into nicely formatted LaTeX documents

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.

Theorema Project: Specialized Proving Methods (Advisor: Wolfgang Windsteiger). In the frame of this thesis, specialized proving/solving tequniques for particular areas of mathematics (e.g. polynomials, vector spaces, etc.) should be studied and implemented in the frame of Theorema 2.0. Prerequisites: basic knowledge of the Mathematica programming language, interest in logic/proving, working in a bigger team, and structured software development. Working area: 80% mathematics, 20% informatics.

Finished Theses

2023

Algorithms for linear recurrence sequences

P. Nuspl

Johannes Kepler University Linz. PhD Thesis. 2023. [pdf]
[bib]
@phdthesis{RISC6711,
author = {P. Nuspl},
title = {{Algorithms for linear recurrence sequences}},
language = {english},
year = {2023},
translation = {0},
school = {Johannes Kepler University Linz},
length = {129}
}

Formalisation of Relational Algebra and a SQL-like Language with the RISCAL Model Checker

Joachim Borya

Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. Bachelor Thesis. May 2023. Also available as RISC Report 23-06. [doi] [pdf]
[bib]
@misc{RISC6707,
author = {Joachim Borya},
title = {{Formalisation of Relational Algebra and a SQL-like Language with the RISCAL Model Checker}},
language = {english},
abstract = {The relational database model is based on the mathematical concept of relational algebra.Query languages have been developed to make data available quickly without creatingdedicated access procedures that depend on the internal representation of the data. SQL(structured query language) can be seen as a quasi-standard for this. This thesis dealswith the formalization and verification of relational algebra and a small but elementarysubset of SQL with the help of the RISCAL model checker, a software tool for the formalspecification and verification of mathematical theories and algorithms.},
year = {2023},
month = {May},
note = {Also available as RISC Report 23-06},
translation = {0},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria},
keywords = {formal methods, program verification, model checking, automated theorem proving},
length = {77},
url = {https://doi.org/10.35011/risc.23-06}
}

Model Checking Concurrent Systems Under Fairness Constraints in RISCAL

Ágoston Sütő

Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. Master Thesis. May 2023. Also available as RISC Report 23-07. Master's thesis. [doi] [pdf]
[bib]
@misc{RISC6709,
author = {Ágoston Sütő},
title = {{Model Checking Concurrent Systems Under Fairness Constraints in RISCAL}},
language = {english},
abstract = {Model checking is a method for verifying that a program satisfies certain desirable properties formalised using mathematical logic. It is a rigorous method, similar to theorem proving, but it is generally applied when theorem proving would be too difficult due to the complexity of the algorithm, such as in concurrent systems. Model checking is used in the software industry. RISCAL (RISC Algorithm Language) is a language and software system that can be used to describe algorithms over a finite domain, specify their behaviour and then validate the specification. While it mainly focuses on deterministic algorithms, it has limited support for non-deterministic systems as well.The thesis extends the support for non-deterministic systems in RISCAL by allowing the user to specify complex properties about their behaviour in the language of Linear Temporal Logic (LTL) and then to validate them. The core contribution is a model checker implemented in Java using the so-called automaton-based explicit state model checking approach. The software is capable of verifying certain properties that could not be handled by a well-known model checker used in the industry. While in most cases it has underperformed its competitors, our implementation is promising, especially when it comes to properties with certain side conditions, called fairness constraints. The majority of the thesis is be concerned with the theoretical aspects of the automaton-based model checking approach, which is followed by a description of the implementation and various benchmarks.},
year = {2023},
month = {May},
note = {Also available as RISC Report 23-07},
translation = {0},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria},
keywords = {formal methods, model checking, concurrent systems, nondeterminism, linear temporal logic},
sponsor = {Supported by Aktion Österreich–Slowakei project grant Nr. 2019-10-15-003 “Semantic Modeling of Component-Based Program Systems”},
length = {102},
url = {https://doi.org/10.35011/risc.23-07},
type = {Master's thesis}
}

2022

New asymptotics and inequalities related to the partition function

K. Banerjee

Research Institute for Symbolic Computation, Johannes Kepler University. PhD Thesis. 2022. [pdf]
[bib]
@phdthesis{RISC6712,
author = {K. Banerjee},
title = {{New asymptotics and inequalities related to the partition function}},
language = {english},
year = {2022},
translation = {0},
school = {Research Institute for Symbolic Computation, Johannes Kepler University},
length = {333}
}

Symbolic Techniques for Approximate Reasoning

Cleo Pau

RISC, JKU. PhD Thesis. 2022. [pdf]
[bib]
@phdthesis{RISC6513,
author = {Cleo Pau},
title = {{Symbolic Techniques for Approximate Reasoning}},
language = {english},
year = {2022},
translation = {0},
school = {RISC, JKU},
length = {202}
}

2021

Die Newton-Andrews-Zeilberger Methode zur Berechnung von harmonischen Summen Identitäten

Bettina Salomon

-. Bachelor Thesis. 2021.
[bib]
@misc{RISC6644,
author = {Bettina Salomon},
title = {{Die Newton-Andrews-Zeilberger Methode zur Berechnung von harmonischen Summen Identitäten}},
language = {english},
year = {2021},
translation = {0},
institution = {-},
length = {0}
}

Refinement Types for Elm

Lucas Payr

Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. Master Thesis. April 2021. Also available as RISC report no. 21-10. Master Thesis. [pdf]
[bib]
@misc{RISC6304,
author = {Lucas Payr},
title = {{Refinement Types for Elm}},
language = {english},
abstract = {The aim of this thesis is to add refinement types to Elm. Elm is a pure functionalprogramming language that uses a Hindley-Miler type system. Refinement types aresubtypes of existing types. These subtypes are defined by a predicate that specifieswhich values are part of the subtypes. To extend a Hindley-Miler type system, onecan use so-called liquid types. These are special refinement types that come with analgorithm for type inference. This algorithm interacts with an SMT solver to solvesubtyping conditions. A type system using liquid types is not complete, meaning notevery valid program can be checked. Instead, liquid types are only defined for a subsetof expressions and only allow specific predicates. In this thesis, we give a formaldefinition of the Elm language and its type system. We extend the type system withliquid types and provide a subset of expressions and a subset of predicates such thatthe extended type system is sound. We use the free software system “K Framework”for rapid prototyping of the formal Elm type system. For rapid prototyping of thecore algorithm of the extended type system we implemented said algorithm in Elmand checked the subtyping condition in Microsoft’s SMT solver Z3.},
year = {2021},
month = {April},
note = {Also available as RISC report no. 21-10},
translation = {0},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria},
keywords = {formal semantics, formal type systems, programming languages, satisfiability solving},
length = {135},
type = {Master Thesis}
}

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]
[bib]
@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]
[bib]
@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}
}

Computer Algebra with the Fifth Operation: Applications of Modular Functions to Partition Congruences

N. Smoot

Research Institute for Symbolic Computation, JKU Linz. PhD Thesis. 2020. [pdf]
[bib]
@phdthesis{RISC6512,
author = {N. Smoot},
title = {{Computer Algebra with the Fifth Operation: Applications of Modular Functions to Partition Congruences}},
language = {english},
abstract = {We give the implementation of an algorithm developed by Silviu Radu to compute examples of a wide variety of arithmetic identities originally studied by Ramanujan and Kolberg. Such identities employ certain finiteness conditions imposed by the theory of modular functions, and often yield interesting arithmetic information about the integer partition function $p(n)$, and other associated functions. We compute a large number of examples of such identities taken from contemporary research, often extending or improving existing results. We then use our implementation as a computational tool to help us achieve more theoretical results in the study of infinite congruence families. We finally describe a new method which extends the existing techniques for proving partition congruence families associated with a genus 0 modular curve.},
year = {2020},
translation = {0},
school = {Research Institute for Symbolic Computation, JKU Linz},
length = {224}
}

Modelling and Solving a Scheduling Problem by Max-Flow

Moritz Willnauer

RISC Institute, JKU Linz. Bachelor Thesis. March 2020. [pdf]
[bib]
@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]
[bib]
@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. Also available as RISC Report 20-17. [pdf]
[bib]
@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},
note = {Also available as RISC Report 20-17},
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.
[bib]
@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]
[bib]
@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]
[bib]
@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]
[bib]
@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]
[bib]
@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]
[bib]
@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]
[bib]
@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}
}

Loading…