@inproceedings{RISC5531,author = {Wolfgang Schreiner and Alexander Brunhuemer and Christoph Fürst},
title = {{Teaching the Formalization of Mathematical Theories and Algorithms via the Automatic Checking of Finite Models}},
booktitle = {{Post-Proceedings ThEdu'17}},
language = {english},
abstract = {Education in the practical applications of logic and proving such as the formal
specification and verification of computer programs is substantially hampered by
the fact that most time and effort that is invested in proving is actually
wasted in vain: because of errors in the specifications respectively algorithms
that students have developed, their proof attempts are often pointless (because
the proposition proved is actually not of interest) or a priori doomed to fail
(because the proposition to be proved does actually not hold); this is a
frequent source of frustration and gives formal methods a bad reputation. RISCAL
(RISC Algorithm Language) is a formal specification language and associated
software system that attempts to overcome this problem by making logic
formalization fun rather than a burden. To this end, RISCAL allows students to
easily validate the correctness of instances of propositions respectively
algorithms by automatically evaluating/executing and checking them on (small)
finite models. Thus many/most errors can be quickly detected and subsequent
proof attempts can be focused on propositions that are more/most likely to be
both meaningful and true.},
series = {Electronic Proceedings in Theoretical Computer Science (EPTCS)},
volume = {267},
pages = {120--139},
publisher = {Open Publishing Association},
isbn_issn = {ISSN 2075-2180},
year = {2018},
editor = {Pedro Quaresma and Walther Neuper},
refereed = {yes},
keywords = {formal methods, program specification and verification, model checking, computer science education, logic},
sponsor = {Supported by the Johannes Kepler University Linz, Linz Institute of Technology (LIT), Project LOGTECHEDU "Logic Technology for Computer Science Education"},
length = {20},
conferencename = {6th International Workshop on Theorem proving components for Educational software (ThEdu'17), Gothenburg, Sweden, 6 Aug 2017},
url = {http://dx.doi.org/10.4204/EPTCS.267.8}
}