Theses

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

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

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

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

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