Theses

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

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

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

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

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

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

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

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

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

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

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