Logic Technology for Computer Science Education [LOGTECHEDU]

Project Lead

Project Duration

01/03/2018 - 29/02/2020

Project URL

Project Website

Partners

Publications

2018

Validating Mathematical Theories and Algorithms with RISCAL

Wolfgang Schreiner

In: Intelligent Computer Mathematics, F. Rabe, W. Farmer, G. Passmore, A. Youssef (ed.), Proceedings of CICM 2018, 11th Conference on Intelligent Computer Mathematics, Hagenberg, Austria, August 13-17, 2018, Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence 11006, pp. 248-254. 2018. Springer, Berlin, ISBN 978-3-319-96811-7. The final authenticated version is available online at Springer. [url] [pdf]
[bib]
@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}
}

Logic as a Path to Enlightenment (Work in Progress Report)

Wolfgang Schreiner

In: Computer Mathematics in Education - Enlightenment or Incantation?, Walther Neuper (ed.), Proceedings of CME-EI18, Workshop at CICM 2018, 11th Conference on Intelligent Computer Mathematics, Hagenberg, Austria, August 17, 2018., pp. 1-5. August 2018. To be published at CEUR Workshop Proceedings, http://CEUR-ws.org, ISSN 1613-0073. [pdf]
[bib]
@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 = {To be published at CEUR Workshop Proceedings, http://CEUR-ws.org},
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.}
}

Loading…