# Semantic Technologies for Computer Science Education [SemTech]

### Project Lead

### Project Duration

01/01/2018 - 31/12/2019### Project URL

Go to Website## Publications

### 2020

[Schreiner]

### Mathematical Model Checking Based on Semantics and SMT

#### Wolfgang Schreiner, Franz-Xaver Reichl

Transactions on Internet Research 16(2), pp. 4-13. July 2020. IPSI, ISSN 1820-4503. [url]@

author = {Wolfgang Schreiner and Franz-Xaver Reichl},

title = {{Mathematical Model Checking Based on Semantics and SMT}},

language = {english},

abstract = {We report on the usage and implementation of RISCAL, a model checker formathematical theories and algorithms based on a variant of first-order logicwith finite models; this allows to automatically decide the validity of allformulas and to verify the correctness of all algorithms specified by suchformulas. We describe the semantics-based implementation of the checker aswell as a recently developed alternative based on SMT solving, andexperimentally compare their performance. Furthermore, we report on ourexperience with RISCAL for enhancing education in computer science andmathematics, in particular in academic courses on logic, formal methods, andformal modeling. By the use of this software, students are encouraged toactively engage with the course material by solving concrete problems wherethe correctness of a solution is automatically checked; if a solution is notcorrect or the student gets stuck, the software provides additional insightand hints that aid the student towards the desired result.},

journal = {Transactions on Internet Research},

volume = {16},

number = {2},

pages = {4--13},

publisher = {IPSI},

isbn_issn = {ISSN 1820-4503},

year = {2020},

month = {July},

refereed = {yes},

keywords = {model checking, logic, semantics, formal verification, reasoning about programs, computer science education},

sponsor = {Johannes Kepler University, Linz, Institute of Technology(LIT) project LOGTECHEDU and OEAD WTZ project SK 14/2018 SemTech},

length = {10},

url = {http://ipsitransactions.org/journals/papers/tir/2020jul/p2.pdf}

}

**article**{RISC6117,author = {Wolfgang Schreiner and Franz-Xaver Reichl},

title = {{Mathematical Model Checking Based on Semantics and SMT}},

language = {english},

abstract = {We report on the usage and implementation of RISCAL, a model checker formathematical theories and algorithms based on a variant of first-order logicwith finite models; this allows to automatically decide the validity of allformulas and to verify the correctness of all algorithms specified by suchformulas. We describe the semantics-based implementation of the checker aswell as a recently developed alternative based on SMT solving, andexperimentally compare their performance. Furthermore, we report on ourexperience with RISCAL for enhancing education in computer science andmathematics, in particular in academic courses on logic, formal methods, andformal modeling. By the use of this software, students are encouraged toactively engage with the course material by solving concrete problems wherethe correctness of a solution is automatically checked; if a solution is notcorrect or the student gets stuck, the software provides additional insightand hints that aid the student towards the desired result.},

journal = {Transactions on Internet Research},

volume = {16},

number = {2},

pages = {4--13},

publisher = {IPSI},

isbn_issn = {ISSN 1820-4503},

year = {2020},

month = {July},

refereed = {yes},

keywords = {model checking, logic, semantics, formal verification, reasoning about programs, computer science education},

sponsor = {Johannes Kepler University, Linz, Institute of Technology(LIT) project LOGTECHEDU and OEAD WTZ project SK 14/2018 SemTech},

length = {10},

url = {http://ipsitransactions.org/journals/papers/tir/2020jul/p2.pdf}

}

### 2019

[Schreiner]

### Theorem and Algorithm Checking for Courses on Logic and Formal Methods

#### Wolfgang Schreiner

In: Post-Proceedings ThEdu'18, Pedro Quaresma and Walther Neuper (ed.), Proceedings of 7th International Workshop on Theorem proving components for Educational software, Oxford, United Kingdom, 18 July 2018, Electronic Proceedings in Theoretical Computer Science (EPTCS) 290, pp. 56-75. April 1 2019. Open Publishing Association, ISSN 2075-2180. [url] [pdf]@

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**{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}

}

[Schreiner]

### A Categorical Semantics of Relational First-Order Logic

#### Wolfgang Schreiner, Valerie Novitzká, William Steingartner

Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, March 2019. [pdf]@

author = {Wolfgang Schreiner and Valerie Novitzká and William Steingartner},

title = {{A Categorical Semantics of Relational First-Order Logic}},

language = {english},

abstract = {We present a categorical formalization of a variant of first-order logic. Unlike other textson this topic, the goal of this paper is to give a very transparent and self-contained accountwithout requiring more background than basic logic and set theory. Our focus is to showhow the semantics of first order formulas can be derived from their usual deduction rules.For understanding the core ideas, it is not necessary to investigate the internal term structureof atomic formulas, thus we abstract atomic formulas to (syntactically opaque) relations;in this sense our variant of first-order logic is “relational”. While the derived semanticsis based on categorical principles, it is nevertheless “constructive” in that it describesexplicit computations of the truth values of formulas. We demonstrate this by modeling thecategorical semantics in the RISCAL (RISC Algorithm Language) system which allows usto validate the core propositions by automatically checking them in finite models.},

year = {2019},

month = {March},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},

keywords = {first-order logic, formal semantics, category theory, RISC Algorithm Language (RISCAL)},

sponsor = {OEAD WTZ project SK 14/2018 “SemTech — Semantic Technologies for Computer Science Education” and JKU LIT project LOGTECHEDU “Logic Technology for Computer Science Education”},

length = {34}

}

**techreport**{RISC5900,author = {Wolfgang Schreiner and Valerie Novitzká and William Steingartner},

title = {{A Categorical Semantics of Relational First-Order Logic}},

language = {english},

abstract = {We present a categorical formalization of a variant of first-order logic. Unlike other textson this topic, the goal of this paper is to give a very transparent and self-contained accountwithout requiring more background than basic logic and set theory. Our focus is to showhow the semantics of first order formulas can be derived from their usual deduction rules.For understanding the core ideas, it is not necessary to investigate the internal term structureof atomic formulas, thus we abstract atomic formulas to (syntactically opaque) relations;in this sense our variant of first-order logic is “relational”. While the derived semanticsis based on categorical principles, it is nevertheless “constructive” in that it describesexplicit computations of the truth values of formulas. We demonstrate this by modeling thecategorical semantics in the RISCAL (RISC Algorithm Language) system which allows usto validate the core propositions by automatically checking them in finite models.},

year = {2019},

month = {March},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},

keywords = {first-order logic, formal semantics, category theory, RISC Algorithm Language (RISCAL)},

sponsor = {OEAD WTZ project SK 14/2018 “SemTech — Semantic Technologies for Computer Science Education” and JKU LIT project LOGTECHEDU “Logic Technology for Computer Science Education”},

length = {34}

}

[Schreiner]

### Logic and Semantic Technologies for Computer Science Education

#### Wolfgang Schreiner

In: Informatics’2019, 2019 IEEE 15th International Scientific Conference on Informatics, Poprad, Slovakia, November 20–22, William Steingartner, Štefan Korecko, Anikó Szakál (ed.), pp. 415-420. 2019. IEEE, ISBN 978-1-7281-3178-8. invited paper. [url]@

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**{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}

}

[Schreiner]

### A Coalgebraic Operational Semantics for an Imperative Language

#### William Steingartner, Valerie Novitzká, Wolfgang Schreiner

Computing and Informatics, pp. -. 2019. ISSN 1335-9150. To appear.@

author = {William Steingartner and Valerie Novitzká and Wolfgang Schreiner},

title = {{A Coalgebraic Operational Semantics for an Imperative Language}},

language = {english},

abstract = {Operational semantics is a known and popular semantic method fordescribing the execution of programs in detail. The traditional definition of thismethod defines each step of a program as a transition relation. We present a newapproach on how to define operational semantics as a coalgebra over a category ofconfigurations. Our approach enables us to deal with a program that is written in asmall but real imperative language containing also the common program constructsas input and output statements, and declarations. A coalgebra enables to defineoperational semantics in a uniform way and it describes the behavior of the programs.The state space of our coalgebra consists of the configurations modeling theactual states; the morphisms in a base category of the coalgebra are the functionsdefining particular steps during the program’s executions. Polynomial endofunctordetermines this type of systems. Another advantage of our approach is its easy implementationand graphical representation, which we illustrate on a simple program.},

journal = {Computing and Informatics},

pages = {--},

isbn_issn = {ISSN 1335-9150},

year = {2019},

note = {To appear},

refereed = {yes},

length = {28}

}

**article**{RISC5980,author = {William Steingartner and Valerie Novitzká and Wolfgang Schreiner},

title = {{A Coalgebraic Operational Semantics for an Imperative Language}},

language = {english},

abstract = {Operational semantics is a known and popular semantic method fordescribing the execution of programs in detail. The traditional definition of thismethod defines each step of a program as a transition relation. We present a newapproach on how to define operational semantics as a coalgebra over a category ofconfigurations. Our approach enables us to deal with a program that is written in asmall but real imperative language containing also the common program constructsas input and output statements, and declarations. A coalgebra enables to defineoperational semantics in a uniform way and it describes the behavior of the programs.The state space of our coalgebra consists of the configurations modeling theactual states; the morphisms in a base category of the coalgebra are the functionsdefining particular steps during the program’s executions. Polynomial endofunctordetermines this type of systems. Another advantage of our approach is its easy implementationand graphical representation, which we illustrate on a simple program.},

journal = {Computing and Informatics},

pages = {--},

isbn_issn = {ISSN 1335-9150},

year = {2019},

note = {To appear},

refereed = {yes},

length = {28}

}

### 2018

[Schreiner]

### Visualizing Execution Traces in RISCAL

#### Wolfgang Schreiner, William Steingartner

Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, March 2018. [pdf]@

author = {Wolfgang Schreiner and William Steingartner},

title = {{Visualizing Execution Traces in RISCAL}},

language = {english},

abstract = {We report on initial results concerning the visualization of execution traces ofalgorithms that are formally specified and modeled in the RISC AlgorithmLanguage (RISCAL); these algorithms are executed and visualized in theassociated software system which also validates their correctness by checkingthe satisfaction of the formal contracts. This work has been stimulated bycorresponding visualization of Jane, a language with an associated toolkit that has been developed to demonstrate the categorical semantics ofprogramming languages. By the new visualization extension of RISCAL, thesuitability of the software for the purpose of computer science education shallbe improved.},

year = {2018},

month = {March},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},

keywords = {formal methods, verification, model checking},

sponsor = {Austrian OEAD WTZ and Slovak SRDA contract SK 14/2018 "SemTech", JKU Linz Institute of Technology (LIT) project "LOGTECHEDU"},

length = {7}

}

**techreport**{RISC5610,author = {Wolfgang Schreiner and William Steingartner},

title = {{Visualizing Execution Traces in RISCAL}},

language = {english},

abstract = {We report on initial results concerning the visualization of execution traces ofalgorithms that are formally specified and modeled in the RISC AlgorithmLanguage (RISCAL); these algorithms are executed and visualized in theassociated software system which also validates their correctness by checkingthe satisfaction of the formal contracts. This work has been stimulated bycorresponding visualization of Jane, a language with an associated toolkit that has been developed to demonstrate the categorical semantics ofprogramming languages. By the new visualization extension of RISCAL, thesuitability of the software for the purpose of computer science education shallbe improved.},

year = {2018},

month = {March},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},

keywords = {formal methods, verification, model checking},

sponsor = {Austrian OEAD WTZ and Slovak SRDA contract SK 14/2018 "SemTech", JKU Linz Institute of Technology (LIT) project "LOGTECHEDU"},

length = {7}

}

[Schreiner]

### 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]@

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**{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}

}

[Schreiner]

### 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. CEUR Workshop Proceedings, Volume 2307, http://ceur-ws.org/Vol-2307/, ISSN 1613-0073. [url] [pdf]@

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}

}

**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}

}

[Schreiner]

### Visualizing Logic Formula Evaluation in RISCAL

#### Wolfgang Schreiner, William Steingartner

Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, July 2018. [pdf]@

author = {Wolfgang Schreiner and William Steingartner},

title = {{Visualizing Logic Formula Evaluation in RISCAL}},

language = {english},

abstract = {We report on initial results concerning the visualization of the evaluation oflogic formulas that are formulated in the RISC Algorithm Language (RISCAL). Suchformulas usually represent propositions that are supposed to be true; examplesare mathematical theorems or verification conditions of algorithms that havebeen formally modeled and specified in RISCAL. The visualization is intended toaid the user to understand the truth value of a formula, in particular in thosecases where a formula is unexpectedly not valid. To this aim, the visualizationof a formula consists of a pruned evaluation tree that depicts exactly thoseevaluation branches that contribute to the overall truth value.},

year = {2018},

month = {July},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},

keywords = {formal methods, verification, 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 = {13}

}

**techreport**{RISC5721,author = {Wolfgang Schreiner and William Steingartner},

title = {{Visualizing Logic Formula Evaluation in RISCAL}},

language = {english},

abstract = {We report on initial results concerning the visualization of the evaluation oflogic formulas that are formulated in the RISC Algorithm Language (RISCAL). Suchformulas usually represent propositions that are supposed to be true; examplesare mathematical theorems or verification conditions of algorithms that havebeen formally modeled and specified in RISCAL. The visualization is intended toaid the user to understand the truth value of a formula, in particular in thosecases where a formula is unexpectedly not valid. To this aim, the visualizationof a formula consists of a pruned evaluation tree that depicts exactly thoseevaluation branches that contribute to the overall truth value.},

year = {2018},

month = {July},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},

keywords = {formal methods, verification, 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 = {13}

}

[Schreiner]

### WebEx: Web Exercises for RISCAL

#### Wolfgang Schreiner

Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, October 2018. [pdf]@

author = {Wolfgang Schreiner},

title = {{WebEx: Web Exercises for RISCAL}},

language = {english},

abstract = {We report on a software framework "WebEx" for developing web-basedstudent exercises whose correctness is checked with the help of the RISCAL (RISCAlgorithm Language) software. This framework allows to generate from anappropriately annotated RISCAL specification file an HTML file that serves asthe frontend to a remote execution service. Student input (RISCAL fragments) aretransmitted to this execution service which generates from the annotatedspecification file and the input a plain RISCAL specification on which RISCAL isinvoked (in a non-interactive mode); the success status of the execution and theproduced output are reported back to the web interface. For each successfulexercise the server produces a digitally signed certificate that is returned tothe user who may submit this certificate as a proof of successful completion ofthe exercise (which may be subsequently automatically checked). Furthermore eachannotated RISCAL specification may serve as a template that may be instantiatedwith other data to produce a set of exercise instances. The WebEx software ismostly independent of RISCAL; it may be also used to provide a web front end forother scientific software of a similar nature.},

year = {2018},

month = {October},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},

keywords = {formal methods, logic, computer-supported education},

sponsor = {Austrian OEAD WTZ program and the Slovak SRDA agency contract SK 14/2018 SemTech and Johannes Kepler University Linz, Linz Institute of Technology (LIT), Project LOGTECHEDU},

length = {35}

}

**techreport**{RISC5793,author = {Wolfgang Schreiner},

title = {{WebEx: Web Exercises for RISCAL}},

language = {english},

abstract = {We report on a software framework "WebEx" for developing web-basedstudent exercises whose correctness is checked with the help of the RISCAL (RISCAlgorithm Language) software. This framework allows to generate from anappropriately annotated RISCAL specification file an HTML file that serves asthe frontend to a remote execution service. Student input (RISCAL fragments) aretransmitted to this execution service which generates from the annotatedspecification file and the input a plain RISCAL specification on which RISCAL isinvoked (in a non-interactive mode); the success status of the execution and theproduced output are reported back to the web interface. For each successfulexercise the server produces a digitally signed certificate that is returned tothe user who may submit this certificate as a proof of successful completion ofthe exercise (which may be subsequently automatically checked). Furthermore eachannotated RISCAL specification may serve as a template that may be instantiatedwith other data to produce a set of exercise instances. The WebEx software ismostly independent of RISCAL; it may be also used to provide a web front end forother scientific software of a similar nature.},

year = {2018},

month = {October},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},

keywords = {formal methods, logic, computer-supported education},

sponsor = {Austrian OEAD WTZ program and the Slovak SRDA agency contract SK 14/2018 SemTech and Johannes Kepler University Linz, Linz Institute of Technology (LIT), Project LOGTECHEDU},

length = {35}

}