Formal Methods

At RISC we understand by formal methods the application of methods from symbolic computation (especially from formal logic) to rigorously reason about properties of computer programs, in particular to verify their correctness with respect to a specification.

The term "formal methods" applies to all techniques that make computer software and computing systems subject to formal reasoning. By treating a computer program as a mathematical object with a formal semantics, we can rigorously argue about its behavior, e.g., why it always computes the correct result; this reasoning can be supported or even automated by corresponding software. Formal methods are industrially applied wherever computer/program failures are not acceptable, e.g. to mission-critical software, computer chips, or communication protocols.

Formal methods comprise at least two aspects:

  1. "Specification" means to describe the expected behavior of a program in a mathematically precise way (e.g. as a logic formula, see the "ensures" clause in the attached picture which gives the specification of a program).
  2. "Verification": means to demonstrate with mathematical rigor that every possible execution of the program does not crash and indeed satisfies its specification, preferably with computer support (by reasoners that apply proof-based techniques or by model checkers that investigate the space of all possible executions).

Furthermore, the "Validation" of a specification aims to ensure that this specification actually describes the intended behavior; thus the verification of a program with respect to this specification indeed demonstrates that the program satisfies the properties that we are interested in.

Even if the complete verification of a program may sometimes not be feasible, a "light-weight" application of formal methods may help to increase our confidence in the correctness of a program:

  • "Extended Static Checking" and "Bounded Model Checking" apply logic-based techniques to detect errors in a program; while these techniques do not necessarily ensure that a program is correct (they falsify a program rather than verifying it), they at least raise its quality;
  • "Runtime Verification" supervises the execution of a program by an automatically generated monitor that triggers a warning if the program violates its specification; while this does not rule out possible future errors, it at least ensures that the execution so far has been correct.

The support respectively automation of all these aspects by software (automated program verifiers, interactive verification assistants, model checkers, static program analyzers, specification analyzers) is a hot topic of research.

Software

RISC ProgramExplorer

An Interactive Program Reasoning Environment

The RISC ProgramExplorer is a computer-supported program reasoning environment for a simple imperative programming language "MiniJava"; it incorporates the RISC ProofNavigator as a semi-automatic proving assistant. The environment has been developed mainly for educational purposes (see this paper for a ...

MoreSoftware Website

RISC ProofNavigator

An Interactive Proof Assistant for Program/System Verification

The RISC ProofNavigator is an interactive proof assistant for supporting formal reasoning about computer programs and computing systems, see the README file and this short paper for the main ideas; it is the core reasoning component of the RISC ProgramExplorer. ...

MoreSoftware Website

RISCAL

The RISC Algorithm Language: A Language and Associated Software System for Specifying and Verifying Mathematical Algorithms

The RISC Algorithm Language (RISCAL) is a specification language and associated software system for describing mathematical algorithms, formally specifying their behavior based on mathematical theories, and validating the correctness of algorithms, specifications, and theories by execution/evaluation. The software has been ...

MoreSoftware Website

Publications

2020

[Cerna]

Unital Anti-Unification: Type and Algorithms

David M. Cerna , Temur Kutsia

Technical report no. 20-02 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. RISC Report, Febrary 2020. [pdf]
[bib]
@techreport{RISC6080,
author = {David M. Cerna and Temur Kutsia},
title = {{Unital Anti-Unification: Type and Algorithms}},
language = {english},
abstract = {Unital equational theories are defined by axioms that assert the existence of the unit element for some function symbols. We study anti-unification (AU) in unital theories and address the problems of establishing generalization type and designing anti-unification algorithms. First, we prove that when the term signature contains at least two unital functions, anti-unification is of the nullary type by showing that there exists an AU problem, which does not have a minimal complete set of generalizations. Next, we consider two special cases: the linear variant and the fragment with only one unital symbol, and design AU algorithms for them. The algorithms are terminating, sound, complete and return tree grammars from which set of generalizations can be constructed. Anti-unification for both special cases is finitary. Further, the algorithm for the one-unital fragment is extended to the unrestricted case. It terminates and returns a tree grammar which produces an infinite set of generalizations. At the end, we discuss how the nullary type of unital anti-unification might affect the anti-unification problem in some combined theories, and list some open questions. },
number = {20-02},
year = {2020},
month = {Febrary},
howpublished = {RISC Report},
keywords = {Anti-unification, tree grammars, unital theories, collapse theories},
length = {19},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Cerna]

Aiding an Introduction to Formal Reasoning Within a First-Year Logic Course for CS Majors Using a Mobile Self-Study App

David M. Cerna, Martina Seidl, Wolfgang Schreiner, Wolfgang Windsteiger, Armin Biere

In: ITICSE 2020, ACM (ed.), pp. 1-7. 2020. https://doi.org/10.1145/3341525.3387409.
[bib]
@inproceedings{RISC6096,
author = {David M. Cerna and Martina Seidl and Wolfgang Schreiner and Wolfgang Windsteiger and Armin Biere},
title = {{Aiding an Introduction to Formal Reasoning Within a First-Year Logic Course for CS Majors Using a Mobile Self-Study App}},
booktitle = {{ITICSE 2020}},
language = {english},
abstract = {In this paper, we share our experiences concerning the introduc-tion of the Android-based self-study app AXolotl within the first-semester logic course offered at our university. This course is manda-tory for students majoring in Computer Science and Artificial In-telligence. AXolotl was used as part of an optional lab assignmentbridging clausal reasoning and SAT solving with classical reason-ing, proof construction, and first-order logic. The app provides anintuitive interface for proof construction in various logical calculiand aids the students through rule application. The goal of thelab assignment was to help students make a smoother transitionfrom clausal and decompositional reasoning used earlier in thecourse to inferential and contextual reasoning required for proofconstruction and first-order logic. We observed that the lab had apositive influence on students’ understanding and end the paperwith a discussion of these results.},
pages = {1--7},
isbn_issn = {https://doi.org/10.1145/3341525.3387409},
year = {2020},
editor = {ACM},
refereed = {yes},
length = {7}
}
[Cerna]

Computational Logic in the First Semester of Computer Science: An Experience Report

David M. Cerna, Martina Seidl, Wolfgang Schreiner, Wolfgang Windsteiger, Armin Biere

In: CSEDU 2020, Springer (ed.), pp. 1-8. 2020. not yet known.
[bib]
@inproceedings{RISC6097,
author = {David M. Cerna and Martina Seidl and Wolfgang Schreiner and Wolfgang Windsteiger and Armin Biere},
title = {{Computational Logic in the First Semester of Computer Science: An Experience Report}},
booktitle = {{CSEDU 2020}},
language = {english},
abstract = {Nowadays, logic plays an ever-increasing role in modern computer science, in theory as well as in practice.Logic forms the foundation of the symbolic branch of artificial intelligence and from an industrial perspective,logic-based verification technologies are crucial for major hardware and software companies to ensure thecorrectness of complex computing systems. The concepts of computational logic that are needed for such purposes are often avoided in early stages of computer science curricula. Instead, classical logic education mainlyfocuses on mathematical aspects of logic depriving students to see the practical relevance of this subject. Inthis paper we present our experiences with a novel design of a first-semester bachelor logic course attendedby about 200 students. Our aim is to interlink both foundations and applications of logic within computerscience. We report on our experiences and the feedback we got from the students through an extensive surveywe performed at the end of the semester.},
pages = {1--8},
isbn_issn = {not yet known},
year = {2020},
editor = {Springer},
refereed = {yes},
length = {8}
}
[Cerna]

A Note on Anti-unification and the Theory of Semirings

David M. Cerna

RISC. Technical report, 2020. [pdf]
[bib]
@techreport{RISC6101,
author = {David M. Cerna},
title = {{A Note on Anti-unification and the Theory of Semirings}},
language = {english},
abstract = {It was recently shown that anti-unification over an equational theory consisting of only identity equations (more than one) is nullary. Such pure theories are artificial and are of little effect on practical aspects of anti-unification. In this work, we extend these nullarity results to the theory of semirings, a heavily studied theory with many practical applications. Furthermore, our argument holds over semirings with commutative multiplication and/or idempotent addition. },
year = {2020},
institution = {RISC},
length = {4}
}
[Cerna]

Unital Anti-Unification: Type and Algorithms

David M. Cerna, Temur Kutsia

In: Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), Zena M. Ariola (ed.), Leibniz International Proceedings in Informatics (LIPIcs) 167, pp. 26:1-26:20. 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, ISBN 978-3-95977-155-9, ISSN 1868-8969. [url]
[bib]
@inproceedings{RISC6132,
author = {David M. Cerna and Temur Kutsia},
title = {{Unital Anti-Unification: Type and Algorithms}},
booktitle = {{Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}},
language = {english},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {167},
pages = {26:1--26:20},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
isbn_issn = {ISBN 978-3-95977-155-9, ISSN 1868-8969},
year = {2020},
editor = {Zena M. Ariola},
refereed = {yes},
length = {20},
url = {https://drops.dagstuhl.de/opus/volltexte/2020/12352/}
}
[Reichl]

The Integration of SMT Solvers into the RISCAL Model Checker

Franz-Xaver Reichl

Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. Master Thesis. April 2020. [pdf]
[bib]
@misc{RISC6103,
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 asubstantial subset of the RISC Algorithm Language (RISCAL). The main goal forthis new approach is to speed up checks done in RISCAL. For this purpose wedeveloped a translation from the RISCAL language to the SMT-LIB language (usingthe QF_UFBV logic). The realisation of this translation in particular required to solvethe problems of eliminating RISCAL’s quantifiers and of encoding RISCAL’s typesand operations. We formally described core components of this translation, provedsome aspects of their correctness, and implemented it in the programming languageJava. We tested the implementation together with the SMT solvers Boolector, CVC4,Yices and Z3, on several real world RISCAL specifications. Additionally, we evaluatedthe performance of our approach by systematic benchmarks and compared it withthat of the original RISCAL checking mechanism. Finally, we analysed the testsin order to determine patterns in specifications that could possibly have a negativeinfluence on the performance of the presented method. The tests showed that amongthe four used SMT solvers, the solver Yices delivered, for almost all, tests the bestresults. Additionally, the tests indicated that the translation is indeed a viablealternative to RISCAL’s current checking method, especially when used togetherwith Yices. So the translation used with Yices was substantially faster than RISCALin approximately 75% of the test cases. Nevertheless, the tests also illustrated thatRISCAL could still check certain test cases substantially faster. Thus, the translationcannot fully replace RISCAL’s current checking methods.},
year = {2020},
month = {April},
translation = {0},
institution = {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}
}
[Reichl]

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]
[bib]
@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}
}
[Schreiner]

The Simulation of Finite-Source Retrial Queueing Systems with Collisions and Blocking

Ádam Tóth, Tamas Bérczes, Janos Sztrik, Attila Kuki, Wolfgang Schreiner

Journal of Mathematical Sciences 246(4), pp. 548-559. March 2020. ISSN 1573-8795. [url]
[bib]
@article{RISC6088,
author = {Ádam Tóth and Tamas Bérczes and Janos Sztrik and Attila Kuki and Wolfgang Schreiner},
title = {{The Simulation of Finite-Source Retrial Queueing Systems with Collisions and Blocking}},
language = {english},
abstract = {This paper investigates, using a simulation program, a retrial queuing system with a single server which is subject to random breakdowns. The number of sources of calls is finite, and collisions can take place. We assume that the failure of the server blocks the system’s operation such that newly arriving customers cannot enter the system, contrary to an earlier paper where the failure does not affect the arrivals. All the random variables included in the model construction are assumed to be independent of each other, and all times are exponentially distributed except for the service time, which is gamma distributed. The novelty of this analysis is the inspection of the blocking effect on the performance measures using different distributions. Various figures represent the impact of the squared coefficient of the variation of the service time on the main performance measures such as the mean and variance of the number of customers in the system, the mean and variance of the response time, the mean and variance of the time a customer spends in the service, and the mean and variance of the sojourn time in the orbit.},
journal = {Journal of Mathematical Sciences },
volume = {246},
number = {4},
pages = {548--559},
isbn_issn = {ISSN 1573-8795},
year = {2020},
month = {March},
refereed = {yes},
sponsor = {Austrian-Hungarian Bilateral Cooperation in Science and Tech- nology project 2017-2.2.4-TeT-AT-2017-00010},
length = {12},
url = {https://doi.org/10.1007/s10958-020-04759-4}
}

2019

[Cerna]

Evaluation of the VL Logic (342.208-9) 2018W End of Semester Questionnaire

David M. Cerna

Submitted to the RISC Report Series. Feburary 2019. [pdf] [xlsx]
[bib]
@techreport{RISC5885,
author = {David M. Cerna},
title = {{Evaluation of the VL Logic (342.208-9) 2018W End of Semester Questionnaire}},
language = {english},
abstract = {In this technical report we cover the choice of layout and intentions behind our end of the semester questionnaire as well as our interpretation of student answers, resulting statistical analysis, and inferences. Our questionnaire is to some extent free-form in that we provide instructions concerning the desired content of the answers but leave the precise formulation of the answer to the student. Our goal, through this approach, was to gain an understanding of how the students viewed there own progress and interest in the course without explicitly guiding them. Towards this end, we chose to have the students draw curves supplemented by short descriptions of important features. We end with a discussion of the benefits and downsides of such a questionnaire as well as what the results entail concerning future iterations of the course. },
year = {2019},
month = {Feburary},
length = {17},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Cerna]

The Castle Game

David M. Cerna

Submitted to the RISC Report Series. 2019. [pdf]
[bib]
@techreport{RISC5886,
author = {David M. Cerna},
title = {{The Castle Game}},
language = {english},
abstract = {A description of a game for teaching certain aspects of first-order logic based on the Drink's Paradox. },
year = {2019},
length = {3},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Cerna]

Manual for AXolotl

David M. Cerna

Submitted to the RISC Report Series. 2019. [pdf] [zip] [jar]
[bib]
@techreport{RISC5887,
author = {David M. Cerna},
title = {{Manual for AXolotl}},
language = {english},
abstract = {In this document we outline how to play our preliminary version of \textbf{AX}olotl. We present a sequence of graphics illustrating the step by step process of playing the game. },
year = {2019},
length = {9},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Cerna]

AXolotl: A Self-study Tool for First-order Logic

David Cerna

Submitted to the RISC Report Series. May 2019. [pdf]
[bib]
@techreport{RISC5936,
author = {David Cerna},
title = {{AXolotl: A Self-study Tool for First-order Logic}},
language = {english},
year = {2019},
month = {May},
length = {4},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Cerna]

A Generic Framework for Higher-Order Generalizations

David M. Cerna, Temur Kutsia

In: Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), Herman Geuvers (ed.), Leibniz International Proceedings in Informatics (LIPIcs) 131, pp. 10:1-10:19. 2019. Schloss Dagstuhl, ISSN 1868-8969. [url]
[bib]
@inproceedings{RISC5947,
author = {David M. Cerna and Temur Kutsia},
title = {{A Generic Framework for Higher-Order Generalizations}},
booktitle = {{Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}},
language = {english},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {131},
pages = {10:1--10:19},
publisher = {Schloss Dagstuhl},
isbn_issn = {ISSN 1868-8969},
year = {2019},
editor = {Herman Geuvers},
refereed = {yes},
length = {19},
url = {http://dx.doi.org/10.4230/LIPIcs.FSCD.2019.10}
}
[Cerna]

On the Complexity of Unsatisfiable Primitive Recursively defined $\Sigma_1$-Sentences

David M. Cerna

Submitted to the RISC Report Series. 2019. [pdf]
[bib]
@techreport{RISC5981,
author = {David M. Cerna},
title = {{On the Complexity of Unsatisfiable Primitive Recursively defined $\Sigma_1$-Sentences}},
language = {english},
abstract = {We introduce a measure of complexity based on formula occurrence within instance proofs of an inductive statement. Our measure is closely related to {\em Herbrand Sequent length}, but instead of capturing the number of necessary term instantiations, it captures the finite representational difficulty of a recursive sequence of proofs. We restrict ourselves to a class of unsatisfiable primitive recursively defined negation normal form first-order sentences, referred to as {\em abstract sentences}, which capture many problems of interest; for example, variants of the {\em infinitary pigeonhole principle}. This class of sentences has been particularly useful for inductive formal proof analysis and proof transformation. Together our complexity measure and abstract sentences allow use to capture a notion of {\em tractability} for state-of-the-art approaches to inductive theorem proving, in particular {\em loop discovery} and {\em tree grammar} based inductive theorem provers. We provide a complexity analysis of an important abstract sentence, and discuss the analysis of a few related sentences, based on the infinitary pigeonhole principle which we conjecture represent the upper limits of tractability and foundation of intractability with respect to the current approaches.},
year = {2019},
length = {17},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Cerna]

A Mobile Application for Self-Guided Study of Formal Reasoning

David M. Cerna and Rafael Kiesel and Alexandra Dzhiganskaya

Submitted to the RISC Report Series. October 2019. [pdf]
[bib]
@techreport{RISC5991,
author = {David M. Cerna and Rafael Kiesel and Alexandra Dzhiganskaya},
title = {{A Mobile Application for Self-Guided Study of Formal Reasoning}},
language = {english},
abstract = {In this work we introduce AXolotl, a self-study aid designed to guide students through the basics offormal reasoning and term manipulation. Unlike most of the existing study aids for formal reasoning,AXolotl is an Android-based application with a simple touch-based interface. Part of the design goalwas to minimize the possibility of user errors which distract from the learning process. Such as typosor inconsistent application of the provided rules. The system includes a zoomable proof viewer whichdisplays the progress made so far and allows for storage of the completed proofs as a JPEG or L A TEXfile. The software is available on the google play store and comes with a small library of problems.Additional problems may be opened in AXolotl using a simple input language. Currently, AXolotlsupports problems which can be solved using rules which transform a single expression into a set ofexpressions. This covers educational scenarios found in our first semester introduction to logic courseand helps bridge the gap between propositional and first-order reasoning. Future developments willinclude rewrite rules which take a set of expressions and return a set of expressions, as well as aquantified first-order extension.},
year = {2019},
month = {October},
length = {18},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Cerna]

Idempotent Anti-unification

David Cerna, Temur Kutsia

ACM Transactions on Computational Logic (TOCL) 21(2), pp. 10:1-10:32. 2019. ACM Press, ISSN 1529-3785. [url] [pdf]
[bib]
@article{RISC6023,
author = {David Cerna and Temur Kutsia},
title = {{Idempotent Anti-unification}},
language = {english},
journal = {ACM Transactions on Computational Logic (TOCL)},
volume = {21},
number = {2},
pages = {10:1--10:32},
publisher = {ACM Press},
isbn_issn = {ISSN 1529-3785},
year = {2019},
refereed = {yes},
length = {32},
url = {https://doi.org/10.1145/3359060}
}
[Schreiner]

On the Probabilistic Model Checking of a Retrial Queueing System with Unreliable Server, Collision, and Constant Time Impatience

Wolfgang Schreiner, János Sztrik

Technical report no. 19-11 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. July 2019. [pdf]
[bib]
@techreport{RISC5984,
author = {Wolfgang Schreiner and János Sztrik},
title = {{On the Probabilistic Model Checking of a Retrial Queueing System with Unreliable Server, Collision, and Constant Time Impatience}},
language = {english},
abstract = {We report on initial experiments with the automated analysis of a finite-source queueingsystem with an unreliable server and collisions of service requests that cause clients to bemoved to an orbit until they can be served. However, clients remain in the obit only forsome maximum amount of time before they run out of patience and unsuccessfully aborttheir service request. In contrast to earlier investigations, the duration of their patience isnot exponentially distributed but constrained by a constant time bound, which imposes aproblem for both their manual and automatic analysis. In this paper we address how suchsystems can be nevertheless approximately analyzed to a certain extent with the help of theprobabilistic model checker PRISM.},
number = {19-11},
year = {2019},
month = {July},
keywords = {formal methods, model checking, performance analysis},
sponsor = {Supported by the Austrian-Hungarian Bilateral Cooperation in Science and Technology project 2017-2.2.4-TeT- AT-2017-00010 and the Aktion Österreich-Ungarn project 101öu7.},
length = {21},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[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]
[bib]
@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]
[bib]
@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]
[bib]
@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}
}

Loading…