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

RISCAL (RISC Algorithm Language) is a language and associated software system for formalizing mathematical models and algorithms and automatically checking the formalization over finite domains. Your task is to study a particular mathematical/computational problem from literature, to develop a formal model of this problem in the RISCAL language, and to validate this model with the RISCAL software. The model may be the specification of a computational problem by a pair of pre/post-conditions; these may be validated by analyzing the inputs/output pairs allowed by the specification and by checking the correctness of an algorithm with respect to this specification. The model may also describe a computational system by an initial state condition and a transition relation; these may be validated by analyzing the sequences of system states arising from this model.
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.

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.
SLANG is a software for generating rapid prototype implementations of formal languages from their specifications. Your task is to study a particular formal language from literature (a simple programming language, a modeling language, a query language, any kind of domain-specific language). You define the syntax of the language,  give it a type system (in the form of a logical inference system), and a semantics (as a mathematical mapping from syntactic domains to semantic domains). You formalize the definitions in the SLANG software and thus generate a prototypical implementation of the language.
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.

The RISCTP theorem proving interface consists of a language for specifying proof problems and of an associated software for solving these problems; it was developed to equip the RISCAL model checker with theorem proving capabilities. Apart from interfaces to external SMT solvers, RISCTP implements an internal prover for first-order logic which also supports equality reasoning based on paramodulation. The goal of this thesis is to extend this reasoning by utilizing the principles of "E-graphs" and "E-matching" that allow to find those terms in a proof problem whose values are equal to the value of a given term; thus we can more easily determine instantiations of quantified variables that are likely to be useful in the further proof. The literature on this topic is to be investigated and the corresponding algorithms are to be implemented (in the programming language Java).
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

2024

Proximity-based matching with arbitrary T-norms

Maximilian Donnermair

RISC, Johannes Kepler University Linz. Bachelor Thesis. 2024. [pdf]
[bib]
@misc{RISC7061,
author = {Maximilian Donnermair},
title = {{Proximity-based matching with arbitrary T-norms}},
language = {english},
year = {2024},
translation = {0},
institution = {RISC, Johannes Kepler University Linz},
length = {38}
}

2023

Symbolic local Fourier Analysis to determine the inf-sup stability of the Stokes equations

Theresa Köfler

Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz. Master Thesis. 2023. [url]
[bib]
@misc{RISC6983,
author = {Theresa Köfler},
title = {{Symbolic local Fourier Analysis to determine the inf-sup stability of the Stokes equations}},
language = {english},
abstract = {We are interested in a stable discretization of the Stokes equations, which arise in fluid mechanics and model the flow of fluids with slow velocities. For the analysis, we are focused on statements on the existence and the uniqueness of a solution. Moreover, we want to have information about the stable dependence of the solution on the data. Brezzi’s theorem guarantees us the existence of a unique solution that depends continuously on the input data, if certain conditions are fulfilled, which hold for the continuous form of the Stokes equations.In order to solve the problem computationally, we have to discretize it, because we have to transfer the problem from an infinite number of degrees of freedom to finitely many ones. Again, we are interested in a result on existence and uniqueness of a solution and its dependence on the data, Moreover, we are focussed in discretization error estimates. Again, we apply Brezzi’s theorem. All conditions immediately carry over to the discrete form, but with one exception, namely the inf-sup condition. So, we want to focus on the constant, which is given by the inf-sup condition for the discrete inf-sup constant that is independent from the mesh size. In the literature, we can find some existing qualitative statements on the discrete inf-sup constant, but we want to get an explicit statement.Such an explicit statement is obtained by local Fourier analysis. In order to get the inf-sup constant, we have to find the minimum of a rational function. We choose cylindrical algebraic decomposition (CAD) to calculate the minimum exactly. Alternatively, a minimum of a function could be derived exactly by curve sketching, but this is computationally too expensive in our case. Another alternative is to approximate the minimum by sampling. This method is fast but it does not deliver an exact solution. Therefore, it is no option for us. So, both of these alternatives are not relevant in our case and we stick to CAD to compute the minimum on a bounded domain. Nevertheless, the task of deriving the minimum with the help of CAD is not easy, because the computation gets more expensive with higher spline degree p. So, it is necessary to do some modifications like splitting the rational function into numerator and denominator, lowering the polynomial degree and using symmetry.In this thesis, all computations are done in Mathematica and the results can be found on the webpage https://www3.risc.jku.at/people/vpillwei/koefler-slFA/.},
year = {2023},
translation = {0},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
length = {98},
url = {https://epub.jku.at/obvulihs/content/pageview/8699174}
}

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}
}

On the Chow ring of (the) moduli space of stable marked curves of genus zero

Jiayue Qi

Research Institute for Symbolic Computation, Johannes Kepler University Linz. PhD Thesis. 2023.
[bib]
@phdthesis{RISC6945,
author = {Jiayue Qi},
title = {{On the Chow ring of (the) moduli space of stable marked curves of genus zero}},
language = {English},
year = {2023},
translation = {0},
school = {Research Institute for Symbolic Computation, Johannes Kepler University Linz},
length = {127}
}

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}
}

Verfahren zum Lösen des Inventory Routing Problems

Sebastian Schmalzer

RISC Institute, Johannes Kepler University Linz. Bachelor Thesis. November 2021. [pdf]
[bib]
@misc{RISC7043,
author = {Sebastian Schmalzer},
title = {{Verfahren zum Lösen des Inventory Routing Problems}},
language = {german},
year = {2021},
month = {November},
translation = {0},
institution = {RISC Institute, Johannes Kepler University Linz},
length = {40}
}

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}
}

Loading…