Semantic Technologies for Computer Science Education [SemTech]

@inproceedings{RISC5895,
author = {Wolfgang Schreiner},
title = {{Theorem and Algorithm Checking for Courses on Logic and Formal Methods}},
booktitle = {{Post-Proceedings ThEdu'18}},
language = {english},
abstract = {The RISC Algorithm Language (RISCAL) is a language for the formal modeling of theories and algorithms. A RISCAL specification describes an infinite class of models each of which has finite size; this allows to fully automatically check in such a model the validity of all theorems and the correctness of all algorithms. RISCAL thus enables us to quickly verify/falsify the specific truth of propositions in sample instances of a model class before attempting to prove their general truth in the whole class: the first can be achieved in a fully automatic way while the second typically requires our assistance. RISCAL has been mainly developed for educational purposes. To this end this paper reports on some new enhancements of the tool: the automatic generation of checkable verification conditions from algorithms, the visualization of the execution of procedures and the evaluation of formulas illustrating the computation of their results, and the generation of Web-based student exercises and assignments from RISCAL specifications. Furthermore, we report on our first experience with RISCAL in the teaching of courses on logic and formal methods and on further plans to use this tool to enhance formal education.},
series = {Electronic Proceedings in Theoretical Computer Science (EPTCS)},
volume = {290},
pages = {56--75},
publisher = {Open Publishing Association},
isbn_issn = {ISSN 2075-2180},
year = {2019},
month = {April 1},
editor = {Pedro Quaresma and Walther Neuper},
refereed = {yes},
sponsor = {Linz Institute of Technology (LIT), Project LOGTECHEDU “Logic Technology for Computer Science Education” and OEAD WTZ project SK 14/2018 SemTech},
length = {20},
conferencename = {7th International Workshop on Theorem proving components for Educational software, Oxford, United Kingdom, 18 July 2018},
url = {http://dx.doi.org/10.4204/EPTCS.290.5}
}

@inproceedings{RISC5957,
author = {Wolfgang Schreiner},
title = {{Logic and Semantic Technologies for Computer Science Education}},
booktitle = {{Informatics’2019, 2019 IEEE 15th International Scientific Conference on Informatics, Poprad, Slovakia, November 20–22}},
language = {english},
abstract = {We report on some projects to develop software rooted in formal logic andsemantics in order to enhance education in computer science and mathematics.The goal is to let students actively engage with the course material bysolving concrete problems where the correctness of a solution isautomatically checked; furthermore, if a solution is not correct or thestudent gets stuck, the software shall provide additional insight and hintsthat aid the student towards the desired result. In particular, we describeour experience with the RISCAL software, a model checker for mathematicaltheories and algorithms, in university courses on logic, formal methods, andformal modeling.},
pages = {415--420},
publisher = {IEEE},
isbn_issn = {ISBN 978-1-7281-3178-8},
year = {2019},
note = {invited paper},
editor = {William Steingartner and Štefan Korecko and Anikó Szakál},
refereed = {no},
keywords = {logic, semantics, formal verification, model checking, reasoning about programs, computer science education},
length = {6},
url = { https://doi.org/10.1109/Informatics47936.2019.9119285}
}

@inproceedings{RISC5704,
author = {Wolfgang Schreiner},
title = {{Validating Mathematical Theories and Algorithms with RISCAL}},
booktitle = {{Intelligent Computer Mathematics}},
language = {english},
abstract = {RISCAL is a language for describing mathematical algo-rithms and formally specifying their behavior with respect to user-definedtheories in first-order logic. This language is based on a type system thatconstrains the size of all types by formal parameters; thus a RISCALspecification denotes an infinite class of models of which every instancehas finite size. This allows the RISCAL software to fully automaticallycheck in small instances the validity of theorems and the correctness ofalgorithms. Our goal is to quickly detect errors respectively inadequa-cies in the formalization by falsification in small model instances beforeattempting actual correctness proofs for the whole model class.},
series = {Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence},
volume = {11006},
pages = {248--254},
publisher = {Springer},
address = {Berlin},
isbn_issn = {ISBN 978-3-319-96811-7},
year = {2018},
note = {The final authenticated version is available online at Springer},
editor = {F. Rabe and W. Farmer and G. Passmore and A. Youssef},
refereed = {yes},
keywords = {Formal specification, Falsification, Model checking},
sponsor = {Supported by the Johannes Kepler University, Linz Institute of Technology (LIT), project LOGTECHEDU, and by the OEAD WTZ project SK 14/2018 SemTech.},
length = {7},
conferencename = {CICM 2018, 11th Conference on Intelligent Computer Mathematics, Hagenberg, Austria, August 13-17, 2018},
url = {https://doi.org/10.1007/978-3-319-96812-4_21}
}

@inproceedings{RISC5711,
author = {Wolfgang Schreiner},
title = {{Logic as a Path to Enlightenment (Work in Progress Report)}},
booktitle = {{Computer Mathematics in Education - Enlightenment or Incantation?}},
language = {english},
pages = {1--5},
publisher = {CEUR Workshop Proceedings, Volume 2307, http://ceur-ws.org/Vol-2307/},
isbn_issn = {ISSN 1613-0073},
year = {2018},
month = {August},
editor = {Walther Neuper},
refereed = {yes},
keywords = {RISC Algorithm Language, RISCAL, Model Checking, Verification},
sponsor = {Supported by the Johannes Kepler University, Linz Institute of Technology (LIT), project LOGTECHEDU, and by the OEAD WTZ project SK 14/2018 SemTech.},
length = {3},
conferencename = {CME-EI18, Workshop at CICM 2018, 11th Conference on Intelligent Computer Mathematics, Hagenberg, Austria, August 17, 2018.},
url = {http://ceur-ws.org/Vol-2307/paper2.pdf}
}