@thesis{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 central
theories and algorithms in the field of discrete mathematics by using the RISC Algorithm
Language (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 intended
to serve as a foundation layer for further research on the corresponding generalized theories
on infinite models.
This thesis results in a collection of specifications of exemplarily chosen formalized algorithms
of set theory, relation and function theory and graph theory. The algorithms are
specified in different ways (implicit, recursive and procedural), to emphasize the corresponding
connections between them.
The evaluation and validation of implemented theories is demonstrated on Dijkstra’s algorithm
for finding a shortest path between vertices in a graph.},
year = {2017},
month = {September},
translation = {0},
school = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
length = {88},
type = {Bachelor Thesis}
}