## Members

## Bruno Buchberger: Founding Chairman 1987-1998

## Michal Buran

## David Cerna

## Wolfgang Schreiner: Vice Director

## Software

LogicGuard is a stream monitor specification language and system. ...

MiniMaple is a software for formal specification and verification of Maple programs. ...

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 ...

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. ...

### 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 ...

## Publications

### 2023

### Is ChatGPT Smarter Than Master’s Applicants?

#### Bruno Buchberger

Technical report no. 23-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). January 2023. Licensed under CC BY 4.0 International. [doi] [pdf]**techreport**{RISC6684,

author = {Bruno Buchberger},

title = {{Is ChatGPT Smarter Than Master’s Applicants?}},

language = {English},

abstract = {During the selection procedure for a particular informatics fellowship program sponsored by Upper Austrian companies, I ask the applicants a couple of simple technical questions about programming, etc., in a Zoom meeting. I put the same questions to the dialogue system ChatGPT, [ChatGPT]. The result surprised me: Nearly all answers of ChatGPT were totally correct and nicely explained. Also, in the dialogues to clarify some critical points in the answers, the explanations by ChatGPT were amazingly clear and goal-oriented.In comparison: I tried out the same questions in the personal Zoom interviews with approximately 30 applicants from five countries. Only the top three candidates (with a GPA of 1.0, i.e., the highest possible GPA in their bachelor’s study) performed approximately equally well in the interview. All the others performed (far) worse than ChatGPT. And, of course, all answers from ChatGPT came within 1 to 10 seconds, whereas most of the human applicants' answers needed lengthy and arduous dialogues.I am particularly impressed by the ability of ChatGPT to extract meaningful and well-structured programs from problem specifications in natural language. In this experiment, I also added some questions that ask for proofs for simple statements in natural language, which I do not ask in the student's interviews. The performance of ChatGPT was quite impressive as far as formalization and propositional logic are concerned. In examples where predicate logic reasoning is necessary, the ChatGPT answers are not (yet?) perfect. I am pleased to see that ChatGPT tries to present the proofs in a “natural style” This is something that I had as one of my main goals when I initiated the Theorema project in 1995. I think we already achieved this in the early stage of Theorema, and we performed this slightly better and more systematically than ChatGPT does.I also tried to develop a natural language input facility for Theorema in 2017, i.e., a tool to formalize natural language statements in predicate logic. However, I could not continue this research for a couple of reasons. Now I see that ChatGPT achieved this goal. Thus, I think that the following combination of methods could result in a significant leap forward:- the “natural style” proving methods that we developed within Theorema (for the automated generation of programs from specifications, the automated verification of programs in the frame of knowledge, and the automated proof of theorems in theories), in particular, my “Lazy Thinking Method” for algorithm synthesis from specifications- and the natural language formalization techniques of ChatGPT.I propose this as a research project topic and invite colleagues and students to contact me and join me in this effort: Buchberger.bruno@gmail.com.},

number = {23-04},

year = {2023},

month = {January},

keywords = {ChatGPT, automated programming, program synthesis, automated proving, formalization of natural language, master's screening},

length = {30},

license = {CC BY 4.0 International},

type = {RISC Report Series},

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

address = {Altenberger Straße 69, 4040 Linz, Austria},

issn = {2791-4267 (online)}

}

### Anti-unification and Generalization: a Survey

#### David Cerna, Temur Kutsia

In: Proceedings of IJCAI 2023 - 32nd International Joint Conference on Artifical Intelligence, Edith Elkind (ed.), pp. 6563-6573. 2023. ijcai.org, ISBN 978-1-956792-03-4 . [doi]**inproceedings**{RISC6743,

author = {David Cerna and Temur Kutsia},

title = {{Anti-unification and Generalization: a Survey}},

booktitle = {{Proceedings of IJCAI 2023 - 32nd International Joint Conference on Artifical Intelligence}},

language = {english},

pages = {6563--6573},

publisher = {ijcai.org},

isbn_issn = {ISBN 978-1-956792-03-4 },

year = {2023},

editor = {Edith Elkind},

refereed = {yes},

length = {11},

url = {https://doi.org/10.24963/ijcai.2023/736}

}

### Concrete Abstractions

#### Wolfgang Schreiner

Texts & Monographs in Symbolic Computation 1st edition, 2023. Springer, Cham, Switzerland, Hardcover ISBN 978-3-031-24933-4, Softcover ISBN 978-3-031-24936-5, eBook ISBN 978-3-031-24934-1. [doi]**book**{RISC6698,

author = {Wolfgang Schreiner},

title = {{Concrete Abstractions}},

language = {english},

series = {Texts & Monographs in Symbolic Computation},

publisher = {Springer},

address = {Cham, Switzerland},

isbn_issn = {Hardcover ISBN 978-3-031-24933-4, Softcover ISBN 978-3-031-24936-5, eBook ISBN 978-3-031-24934-1},

year = {2023},

edition = {1st},

translation = {0},

keywords = {logic in computer science, model checking, formal modeling and reasoning, program specification and verification, discrete structures and algorithms, nondeterminism and concurrency},

length = {270},

url = {https://doi.org/10.1007/978-3-031-24934-1}

}

### The SLANG Semantics-Based Language Generator

#### Wolfgang Schreiner, William Steingartner

Technical report no. 23-13 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). September 2023. Licensed under CC BY 4.0 International. [doi] [pdf]**techreport**{RISC6749,

author = {Wolfgang Schreiner and William Steingartner},

title = {{The SLANG Semantics-Based Language Generator}},

language = {english},

abstract = {This report documents the SLANG semantics-based language generator. SLANG is a software for generating rapid prototype implementations of programming languages from their formal specifications. Its input is a text file that describes the abstract syntax of a language and its concrete text representation; from this, a parser is generated (utilizing the ANTLR4 tool) that transforms the text representation of a program into its abstract syntax tree and a printer that generates from the abstract syntax tree its text representation. Furthermore, one can equip the language with a formal type system (by logical inference rules) from which a type checker is generated. Finally, one can give the language a formal semantics, in the denotational style (by function equations) and/or in the big-step operational style (by transition steps); from this, a language interpreter is generated. SLANG is implemented in Java and produces Java source code; it should be easy to extend the software also to other target languages.},

number = {23-13},

year = {2023},

month = {September},

keywords = {formal semantics of programming languages, denotational semantics, operational semantics, type systems, interpreters},

sponsor = {Supported by the Slovak Academic Information Agency SAIA project 2023-03-15-001 “Semantics-Based Rapid Prototyping of Domain-Specific Languages”},

length = {59},

license = {CC BY 4.0 International},

type = {RISC Report Series},

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

address = {Altenberger Straße 69, 4040 Linz, Austria},

issn = {2791-4267 (online)}

}

### Formalisation of Relational Algebra and a SQL-like Language with the RISCAL Model Checker

#### Joachim Borya

Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. Bachelor Thesis. May 2023. Also available as RISC Report 23-06. [doi] [pdf]**misc**{RISC6707,

author = {Joachim Borya},

title = {{Formalisation of Relational Algebra and a SQL-like Language with the RISCAL Model Checker}},

language = {english},

abstract = {The relational database model is based on the mathematical concept of relational algebra.Query languages have been developed to make data available quickly without creatingdedicated access procedures that depend on the internal representation of the data. SQL(structured query language) can be seen as a quasi-standard for this. This thesis dealswith the formalization and verification of relational algebra and a small but elementarysubset of SQL with the help of the RISCAL model checker, a software tool for the formalspecification and verification of mathematical theories and algorithms.},

year = {2023},

month = {May},

note = {Also available as RISC Report 23-06},

translation = {0},

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

keywords = {formal methods, program verification, model checking, automated theorem proving},

length = {77},

url = {https://doi.org/10.35011/risc.23-06}

}

### Model Checking Concurrent Systems Under Fairness Constraints in RISCAL

#### Ágoston Sütő

Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. Master Thesis. May 2023. Also available as RISC Report 23-07. Master's thesis. [doi] [pdf]**misc**{RISC6709,

author = {Ágoston Sütő},

title = {{Model Checking Concurrent Systems Under Fairness Constraints in RISCAL}},

language = {english},

abstract = {Model checking is a method for verifying that a program satisfies certain desirable properties formalised using mathematical logic. It is a rigorous method, similar to theorem proving, but it is generally applied when theorem proving would be too difficult due to the complexity of the algorithm, such as in concurrent systems. Model checking is used in the software industry. RISCAL (RISC Algorithm Language) is a language and software system that can be used to describe algorithms over a finite domain, specify their behaviour and then validate the specification. While it mainly focuses on deterministic algorithms, it has limited support for non-deterministic systems as well.The thesis extends the support for non-deterministic systems in RISCAL by allowing the user to specify complex properties about their behaviour in the language of Linear Temporal Logic (LTL) and then to validate them. The core contribution is a model checker implemented in Java using the so-called automaton-based explicit state model checking approach. The software is capable of verifying certain properties that could not be handled by a well-known model checker used in the industry. While in most cases it has underperformed its competitors, our implementation is promising, especially when it comes to properties with certain side conditions, called fairness constraints. The majority of the thesis is be concerned with the theoretical aspects of the automaton-based model checking approach, which is followed by a description of the implementation and various benchmarks.},

year = {2023},

month = {May},

note = {Also available as RISC Report 23-07},

translation = {0},

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

keywords = {formal methods, model checking, concurrent systems, nondeterminism, linear temporal logic},

sponsor = {Supported by Aktion Österreich–Slowakei project grant Nr. 2019-10-15-003 “Semantic Modeling of Component-Based Program Systems”},

length = {102},

url = {https://doi.org/10.35011/risc.23-07},

type = {Master's thesis}

}

### 2022

### The RISCTP Theorem Proving Interface - Tutorial and Reference Manual (Version 1.0.*)

#### Wolfgang Schreiner

Technical report no. 22-07 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). June 2022. Licensed under CC BY 4.0 International. [doi] [pdf]**techreport**{RISC6517,

author = {Wolfgang Schreiner},

title = {{The RISCTP Theorem Proving Interface - Tutorial and Reference Manual (Version 1.0.*)}},

language = {english},

abstract = {This report documents the RISCTP theorem proving interface. RISCTP consists of alanguage for specifying proof problems and of an associated software for solving theseproblems. The RISCTP language is a typed variant of first-order logic whose level ofabstraction is between that of higher level formal specification languages (such as thelanguage of the RISCAL model checker) and lower level theorem proving languages (such asthe language SMT-LIB supported by various satisfiability modulo theories solvers such as Z3).Thus the RISCTP language can serve as an intermediate layer that simplifies the connectionof specification and verification systems to theorem provers; in fact, it was developed toequip the RISCAL model checker with theorem proving capabilities. The RISCTP softwareis implemented in Java with an API that enables the implementation of such connections;however, RISCTP also provides a text-based frontend that allows its use as a theorem proveron its own. RISCTP already implements a backend that translates a proving problem intoSMT-LIB and solves it by the "black box" application of Z3; in the future, RISCTP shall alsoprovide built-in proving capabilities with greater transparency.},

number = {22-07},

year = {2022},

month = {June},

keywords = {automated reasoning, theorem proving, model checking, first-order logic, RISCAL, SMT-LIB, Z3},

length = {31},

license = {CC BY 4.0 International},

type = {RISC Report Series},

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

address = {Altenberger Straße 69, 4040 Linz, Austria},

issn = {2791-4267 (online)}

}

### A Temporal Logic Extension of the RISCAL Model Checker

#### Wolfgang Schreiner, Ágoston Sütő

In: 2022 IEEE 16th International Scientific Conference on Informatics, Poprad, Slovakia, November 23-25, William Steingartner, Štefan Korečko, Anikó Szakál (ed.), pp. 267-272. 2022. IEEE, ISBN 979-8-3503-1034-4. [doi]**inproceedings**{RISC6633,

author = {Wolfgang Schreiner and Ágoston Sütő},

title = {{A Temporal Logic Extension of the RISCAL Model Checker}},

booktitle = {{2022 IEEE 16th International Scientific Conference on Informatics, Poprad, Slovakia, November 23-25}},

language = {english},

abstract = {We report on a new extension of the RISCAL model checker that allows to specify nondeterministic transition systems by formulas in linear temporal logic (LTL) and to verify them under fairness constraints. This extension is based on an automata-theoretic approach to explicit state model checking; the performance of its implementation is in some representative examples competitive with (in fact mostly superior to) that of TLA+, a widely known tool for system modeling and analysis. Thus, while RISCAL was originally developed for describing and analyzing mathematical theories and algorithms over discrete structures, these extensions make RISCAL also a competent checker for formal models of concurrent systems.},

pages = {267--272},

publisher = {IEEE},

isbn_issn = {ISBN 979-8-3503-1034-4},

year = {2022},

editor = {William Steingartner and Štefan Korečko and Anikó Szakál},

refereed = {yes},

keywords = {model checking, first-order logic, linear temporal logic, automata theory, formal specification and verification},

sponsor = {Supported by Aktion Österreich–Slowakei project grant Nr. 2019-10-15-003 “Semantic Modeling of Component-Based Program Systems”},

length = {6},

url = {https://doi.org/10.1109/Informatics57926.2022.10083433}

}

### Implementation Techniques for Mathematical Model Checking

#### Wolfgang Schreiner

In: SYNASC 2022, 24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Hagenberg, Austria, September 12-15, Bruno Buchberger, Mircea Marin, Viorel Negru, Daniela Zaharie (ed.), pp. 12-15. 2022. IEEE, ISBN 978-1-6654-6545-8. [doi]**inproceedings**{RISC6634,

author = {Wolfgang Schreiner},

title = {{Implementation Techniques for Mathematical Model Checking}},

booktitle = {{SYNASC 2022, 24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Hagenberg, Austria, September 12-15}},

language = {english},

abstract = {We report on the various implementation techniques that the model checker RISCAL applies for the formal verification of mathematical algorithms and theorems in finite models of configurable sizes. Originally, RISCAL was based entirely on semantic evaluation where every syntactic phrase is translated to an executable version of its denotational semantics, which allows to execute algorithms and to evaluate first-order formulas. Later this was extended by a translation of formulas from the RISCAL language to an SMT-LIB logic, which enables their decision by the application of external SMT (satisfiability modulo theories) solvers. Subsequently, semantic evaluation was extended to nondeterministic/concurrent transition systems which facilitates the verification of invariance properties by state space exploration; this was recently generalized to an automata-based technique for verifying system specifications expressed in a LTL (linear temporal logic) extension of the RISCAL formula language. Recently, the checking capabilities of RISCAL have been complemented (via an embedding of the RISCTP theorem proving interface) by capabilities for verifying formulas in domains of arbitrary size with the help of external theorem provers. We briefly sketch these techniques and discuss their purpose and relationship within the general problem area of algorithm specification and verification.},

pages = {12--15},

publisher = {IEEE},

isbn_issn = {ISBN 978-1-6654-6545-8},

year = {2022},

editor = {Bruno Buchberger and Mircea Marin and Viorel Negru and Daniela Zaharie},

refereed = {yes},

keywords = {formal specification and verification, model checking, satisfiability solving, theorem proving, first-order logic, linear temporal logic},

sponsor = {Supported by Aktion Österreich–Slowakei project grant Nr. 2019-10-15-003 “Semantic Modeling of Component-Based Program Systems”},

length = {4},

url = {https://doi.org/10.1109/SYNASC57785.2022.00011}

}

### 2021

### Semantic Evaluation versus SMT Solving in the RISCAL Model Checker

#### Wolfgang Schreiner, Franz-Xaver Reichl

Technical report no. 21-11 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). June 2021. Licensed under CC BY 4.0 International. [doi] [pdf]**techreport**{RISC6328,

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

title = {{Semantic Evaluation versus SMT Solving in the RISCAL Model Checker}},

language = {english},

abstract = {In this paper, we compare two alternative mechanisms for deciding the validity of first-order formulas over finite domains supported by the mathematical model checker RISCAL: first, the original built-in approach of “semantic evaluation” (based on an implementation of the denotational semantics of the RISCAL language) and, second, the later implemented approach of SMT solving (based on satisfiability preserving translations of RISCAL formulas to formulas in the SMT-LIB logic QF_UFBV, respectively to quantified SMT-LIB bitvector formulas). After a short presentation of the two approaches and a discussion oftheir fundamental pros and cons, we quantitatively evaluate them, both by a set of artificial benchmarks and by a set of benchmarks taken from real-life applications of RISCAL; for this, we apply the state-of-the-art SMT solvers Boolector, CVC4, Yices, and Z3. Our benchmarks demonstrate that (while SMT solving generally vastly outperforms semantic evaluation), the various SMT solvers exhibit great performance differences. More important, our investigations also identify some classes of formulas where semantic evaluation is able to compete with (or even outperform) satisfiability solving, outlining some room forimprovements in the translation of RISCAL formulas to SMT-LIB formulas as well as in the current SMT technology.},

number = {21-11},

year = {2021},

month = {June},

keywords = {model checking, satisfiability solving, formal specification, formal verficiation},

sponsor = {JKU Linz Institute of Technology (LIT) Project LOGTECHEDU, Aktion Österreich- Slowakei Project 2019-10-15-003, Austrian Science Fund (FWF) grant W1255.},

length = {30},

license = {CC BY 4.0 International},

type = {RISC Report Series},

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

address = {Altenberger Straße 69, 4040 Linz, Austria},

issn = {2791-4267 (online)}

}

### First-Order Logic in Finite Domains: Where Semantic Evaluation Competes with SMT Solving

#### Wolfgang Schreiner, Franz-Xaver Reichl

In: Proceedings of the 9th International Symposium on Symbolic Computation in Software Science (SCSS 2021), Hagenberg, Austria, September 8-10, 2021, Temur Kutsia (ed.), Electronic Proceedings in Theoretical Computer Science 342, pp. 99-113. September 2021. ISSN 2075-2180. [doi]**inproceedings**{RISC6361,

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

title = {{First-Order Logic in Finite Domains: Where Semantic Evaluation Competes with SMT Solving}},

booktitle = {{Proceedings of the 9th International Symposium on Symbolic Computation in Software Science (SCSS 2021), Hagenberg, Austria, September 8-10, 2021}},

language = {english},

abstract = {In this paper, we compare two alternative mechanisms for deciding the validity of first-order formulas over finite domains supported by the mathematical model checker RISCAL: first, the original approach of semantic evaluation (based on an implementation of the denotational semantics of the RISCAL language) and, second, the later approach of SMT solving (based on satisfiability preserving translations of RISCAL formulas to SMT-LIB formulas as inputs for SMT solvers). After a short presentation of the two approaches and a discussion of their fundamental pros and cons, we quantitatively evaluate them, both by a set of artificial benchmarks and by a set of benchmarks taken from real-life applications of RISCAL; for this, we apply the state-of-the-art SMT solvers Boolector, CVC4, Yices, and Z3. Our benchmarks demonstrate that (while SMT solving generally vastly outperforms semantic evaluation), the various SMT solvers exhibit great performance differences. More important, we identify classes of formulas where semantic evaluation is able to compete with (or even outperform) satisfiability solving, outlining some room for improvements in the translation of RISCAL formulas to SMT-LIB formulas as well as in the current SMT technology.},

series = {Electronic Proceedings in Theoretical Computer Science},

volume = {342},

pages = {99--113},

isbn_issn = {ISSN 2075-2180},

year = {2021},

month = {September},

editor = {Temur Kutsia},

refereed = {yes},

keywords = {model checking, SMT solving, first-order logic, automated reasoning, formal methods},

sponsor = {e JKU Linz LIT Project LOGTECHEDU, Aktion Österreich-Slowakei Project 2019-10-15-003, Austrian Science Fund (FWF) grant W1255},

length = {15},

url = {https://doi.org/10.4204/EPTCS.342.9}

}

### Thinking Programs

#### Wolfgang Schreiner

Texts & Monographs in Symbolic Computation 1st edition, 2021. Springer, Cham, Switzerland, Hardcover ISBN 978-3-030-80506-7, Softcover ISBN 978-3-030-80509-8, eBook ISBN 978-3-030-80507-4. [doi]**book**{RISC6371,

author = {Wolfgang Schreiner},

title = {{Thinking Programs}},

language = {english},

series = {Texts & Monographs in Symbolic Computation},

publisher = {Springer},

address = {Cham, Switzerland},

isbn_issn = {Hardcover ISBN 978-3-030-80506-7, Softcover ISBN 978-3-030-80509-8, eBook ISBN 978-3-030-80507-4},

year = {2021},

edition = {1st},

translation = {0},

length = {636},

url = {https://doi.org/10.1007/978-3-030-80507-4}

}

### Refinement Types for Elm

#### Lucas Payr

Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. Master Thesis. April 2021. Also available as RISC report no. 21-10. Master Thesis. [pdf]**misc**{RISC6304,

author = {Lucas Payr},

title = {{Refinement Types for Elm}},

language = {english},

abstract = {The aim of this thesis is to add refinement types to Elm. Elm is a pure functionalprogramming language that uses a Hindley-Miler type system. Refinement types aresubtypes of existing types. These subtypes are defined by a predicate that specifieswhich values are part of the subtypes. To extend a Hindley-Miler type system, onecan use so-called liquid types. These are special refinement types that come with analgorithm for type inference. This algorithm interacts with an SMT solver to solvesubtyping conditions. A type system using liquid types is not complete, meaning notevery valid program can be checked. Instead, liquid types are only defined for a subsetof expressions and only allow specific predicates. In this thesis, we give a formaldefinition of the Elm language and its type system. We extend the type system withliquid types and provide a subset of expressions and a subset of predicates such thatthe extended type system is sound. We use the free software system “K Framework”for rapid prototyping of the formal Elm type system. For rapid prototyping of thecore algorithm of the extended type system we implemented said algorithm in Elmand checked the subtyping condition in Microsoft’s SMT solver Z3.},

year = {2021},

month = {April},

note = {Also available as RISC report no. 21-10},

translation = {0},

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

keywords = {formal semantics, formal type systems, programming languages, satisfiability solving},

length = {135},

type = {Master Thesis}

}

### 2020

### Idempotent Anti-unification

#### David Cerna, Temur Kutsia

ACM Transactions on Computational Logic (TOCL) 21(2), pp. 10:1-10:32. 2020. ACM Press, ISSN 1529-3785. [doi] [pdf]**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 = {2020},

refereed = {yes},

length = {32},

url = {https://doi.org/10.1145/3359060}

}

### 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.), Proceedings of ITICSE, pp. 61-67. 2020. 9781450368742. [doi]**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 = {61--67},

isbn_issn = {9781450368742},

year = {2020},

editor = {ACM},

refereed = {yes},

length = {7},

conferencename = {ITICSE},

url = {https://dl.acm.org/doi/10.1145/3341525.3387409}

}

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

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

In: Proceedings of the 12th International Conference on Computer Supported Education - Volume 2: CSEDU, Springer (ed.), Proceedings of CSEDU, pp. 374-381. 2020. 978-989-758-417-6. [doi]**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 = {{Proceedings of the 12th International Conference on Computer Supported Education - Volume 2: CSEDU}},

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 = {374--381},

isbn_issn = {978-989-758-417-6},

year = {2020},

editor = {Springer},

refereed = {yes},

length = {8},

conferencename = {CSEDU},

url = {https://www.scitepress.org/Link.aspx?doi=10.5220/0009464403740381}

}

### 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]**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/}

}

### Higher-order pattern generalization modulo equational theories

#### David M. Cerna, Temur Kutsia

Mathematical Structures in Computer Science 30(6), pp. 627-663. 2020. ISSN 0960-1295. [url]**article**{RISC6226,

author = {David M. Cerna and Temur Kutsia},

title = {{Higher-order pattern generalization modulo equational theories}},

language = {english},

journal = {Mathematical Structures in Computer Science},

volume = {30},

number = {6},

pages = {627--663},

isbn_issn = {ISSN 0960-1295},

year = {2020},

refereed = {yes},

length = {37},

url = {https://www.cambridge.org/core/services/aop-cambridge-core/content/view/88E26F155F0FD02B3EDD648971D9AD1B/S0960129520000110a.pdf/higher-order-pattern-generalization-modulo-equational-theories.pdf}

}

### Unital Anti-Unification: Type and Algorithms

#### David M. Cerna , Temur Kutsia

In: 5th International Conference on Formal Structures for Computation and Deduction, {FSCD} 2020, June 29-July 6, 2020, Paris, France (Virtual Conference, Zena M. Ariola (ed.), Proceedings of FSCD, LIPICS 16720-02, pp. 1-20. 2020. 1868-8969. [doi]**inproceedings**{RISC6237,

author = {David M. Cerna and Temur Kutsia},

title = {{Unital Anti-Unification: Type and Algorithms}},

booktitle = {{5th International Conference on Formal Structures for Computation and Deduction, {FSCD} 2020, June 29-July 6, 2020, Paris, France (Virtual Conference}},

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. },

series = {LIPICS},

volume = {167},

number = {20-02},

pages = {1--20},

isbn_issn = {1868-8969},

year = {2020},

editor = {Zena M. Ariola},

refereed = {yes},

keywords = {Anti-unification, tree grammars, unital theories, collapse theories},

length = {19},

conferencename = {FSCD},

url = {https://doi.org/10.4230/LIPIcs.FSCD.2020.26}

}

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

}