@thesis{RISC6125,author = {Lucas Payr},
title = {{Formalization and Validation of Fundamental Sequence Algorithms by Computer-assisted Checking of Finite Models}},
language = {english},
abstract = {While common textbooks go into great details when it comes to the analy-
sis of sequence algorithms, they lack in proper proofs and moreover formal
specifications. The most essential part, the loop invariant is either described
very vaguely or is completely missing. This thesis gives those missing spec-
ifications as well as so called verification conditions upon which one can
fully prove an algorithm. Normally such a process is very difficult and it is
easy to wrongly specify an algorithm. With the help of the RISC Algorithm
Language (RISCAL), developed at the Research Institute for Symbolic Com-
putation (RISC), this process is simpler as this system provides additional
checks that help noticing early if a specification is wrong. It uses finite
model checking, which makes it possible to check the adequacy of speci-
fications even if they include general quantifiers, which would be difficult
infinite models.
The result of the thesis is a collection of specifications for various search-
ing and sorting algorithms. The algorithms are implemented for different
data types (array, recursive lists, pointer-linked lists) to serve as an addition
to common textbooks.},
year = {2018},
month = {December},
translation = {0},
school = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
keywords = {formal methods, specification, verification, model checking},
sponsor = {Supported by the Johannes Kepler University, Linz, Institute of Technology(LIT) project LOGTECHEDU "Logic Technologies for Computer Science Education"},
length = {85},
type = {Bachelor Thesis}
}