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 a substantial subset of the RISC Algorithm Language (RISCAL). The main goal for this new approach is to speed up checks done in RISCAL. For this purpose we developed a translation from the RISCAL language to the SMT-LIB language (using the QF_UFBV logic). The realisation of this translation in particular required to solve the problems of eliminating RISCAL’s quantifiers and of encoding RISCAL’s types and operations. We formally described core components of this translation, proved some aspects of their correctness, and implemented it in the programming language Java. We tested the implementation together with the SMT solvers Boolector, CVC4, Yices and Z3, on several real world RISCAL specifications. Additionally, we evaluated the performance of our approach by systematic benchmarks and compared it with that of the original RISCAL checking mechanism. Finally, we analysed the tests in order to determine patterns in specifications that could possibly have a negative influence on the performance of the presented method. The tests showed that among the four used SMT solvers, the solver Yices delivered, for almost all, tests the best results. Additionally, the tests indicated that the translation is indeed a viable alternative to RISCAL’s current checking method, especially when used together with Yices. So the translation used with Yices was substantially faster than RISCAL in approximately 75% of the test cases. Nevertheless, the tests also illustrated that RISCAL could still check certain test cases substantially faster. Thus, the translation cannot fully replace RISCAL’s current checking methods.},
year = {2020},
month = {April},
translation = {0},
school = {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},
type = {mathesis}