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

### 2024

### Equational Anti-unification over Absorption Theories

#### Mauricio Ayala-Rincón, David M. Cerna, Andres Felipe Gonzalez Barragan, Temur Kutsia

In: Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Christoph Benzmüller, Marijn J. H. Heule, Renate A. Schmidt (ed.), Lecture Notes in Artificial Intelligence 14740, pp. 317-337. 2024. Springer, ISBN 978-3-031-63500-7. [doi]**inproceedings**{RISC7064,

author = {Mauricio Ayala-Rincón and David M. Cerna and Andres Felipe Gonzalez Barragan and Temur Kutsia},

title = {{Equational Anti-unification over Absorption Theories}},

booktitle = {{Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings}},

language = {english},

series = {Lecture Notes in Artificial Intelligence},

volume = {14740},

pages = {317--337},

publisher = {Springer},

isbn_issn = {ISBN 978-3-031-63500-7},

year = {2024},

editor = {Christoph Benzmüller and Marijn J. H. Heule and Renate A. Schmidt},

refereed = {yes},

length = {21},

url = {https://doi.org/10.1007/978-3-031-63501-4_17}

}

### Solving Quantitative Equations

#### Georg Ehling, Temur Kutsia

In: Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Christoph Benzmüller, Marijn J. H. Heule, Renate A. Schmidt (ed.), Lecture Notes in Artificial Intelligence 14740, pp. 381-400. 2024. Springer, ISBN 978-3-031-63500-7. [doi]**inproceedings**{RISC7065,

author = {Georg Ehling and Temur Kutsia},

title = {{Solving Quantitative Equations}},

booktitle = {{Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings}},

language = {english},

series = {Lecture Notes in Artificial Intelligence},

volume = {14740},

pages = {381--400},

publisher = {Springer},

isbn_issn = {ISBN 978-3-031-63500-7},

year = {2024},

editor = {Christoph Benzmüller and Marijn J. H. Heule and Renate A. Schmidt},

refereed = {yes},

length = {20},

url = {https://doi.org/10.1007/978-3-031-63501-4_20}

}

### Semantics-Based Rapid Prototyping of a Machine Controller Language

#### Wolfgang Schreiner, William Steingartner

In: 2024 IEEE 17th International Scientific Conference on Informatics, Poprad, Slovakia, November 13-15, Valerie Novitzká (ed.), pp. -. 2024. IEEE, ISBN XXXX.**inproceedings**{RISC7063,

author = {Wolfgang Schreiner and William Steingartner},

title = {{Semantics-Based Rapid Prototyping of a Machine Controller Language}},

booktitle = {{2024 IEEE 17th International Scientific Conference on Informatics, Poprad, Slovakia, November 13--15}},

language = {english},

abstract = {We present the use of the semantics-based language generator SLANG to implement a machine controller language EFSM which is based on the principle of extended finite state machines. SLANG allows to rapidly prototype EFSM by a formal definition of the language's abstract syntax, concrete syntax, type system, and denotational semantics; from this, SLANG generates a parser, a printer, a type checker, and an interpreter for EFSM. Subsequently we implement in EFSM a controller for an (idealized) robot vacuum cleaner and validate its operation by simulation and visualization. Our presentation may thus also serve as a template for the semantics-based rapid prototyping of other domain-specific languages.},

pages = {--},

publisher = {IEEE},

isbn_issn = {ISBN XXXX},

year = {2024},

editor = {Valerie Novitzká},

refereed = {yes},

keywords = {rapid prototyping, semantics of programming languages, interpreters, automata, embedded systems},

sponsor = {Aktion Österreich-Slowakei grants 2023-03-15-001 and 2024-05-15-001, KEGA project 030TUKE-4/2023},

length = {6}

}

### 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)}

}

### Automated Programming, Symbolic computation, Machine Learning: My Personal View

#### Bruno Buchberger

Ann. Math. Artif. Intell. 91(5), pp. 569-589. 2023. 1012-2443.**article**{RISC6895,

author = {Bruno Buchberger},

title = {{Automated Programming, Symbolic computation, Machine Learning: My Personal View}},

language = {english},

journal = {Ann. Math. Artif. Intell.},

volume = {91},

number = {5},

pages = {569--589},

isbn_issn = {1012-2443},

year = {2023},

refereed = {yes},

length = {21}

}

### International Young Talents Hotspot Austria

#### Bruno Buchberger

In: Ideen, die gehen!, W. Schüssel, G. Kneifel (ed.), pp. 37-39. 2023. Edition Kleine Zeitung, 20234.**incollection**{RISC6896,

author = {Bruno Buchberger},

title = {{International Young Talents Hotspot Austria}},

booktitle = {{Ideen, die gehen!}},

language = {english},

pages = {37--39},

publisher = {Edition Kleine Zeitung},

isbn_issn = {20234},

year = {2023},

editor = {W. Schüssel and G. Kneifel},

refereed = {no},

length = {3}

}

### Wissenschaft und Meditation: Auf dem Weg zur bewussten Naturgesellschaft

#### Bruno Buchberger

1st edition, December 2023. Amazon, 979-8868299117.**book**{RISC6898,

author = {Bruno Buchberger},

title = {{Wissenschaft und Meditation: Auf dem Weg zur bewussten Naturgesellschaft}},

language = {german},

publisher = {Amazon},

isbn_issn = {979-8868299117},

year = {2023},

month = {December},

edition = {1st},

translation = {0},

length = {184}

}

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

}

### Equational Anti-Unification over Absorption Theories

#### Mauricio Ayala-Rincón, David M. Cerna, Andres Felipe Gonzalez Barragan, Temur Kutsia

arXiv:2310.11136. Technical report, 2023. [doi]**techreport**{RISC6884,

author = {Mauricio Ayala-Rincón and David M. Cerna and Andres Felipe Gonzalez Barragan and Temur Kutsia},

title = {{Equational Anti-Unification over Absorption Theories}},

language = {english},

year = {2023},

institution = {arXiv:2310.11136},

length = {23},

url = {https://doi.org/10.48550/arXiv.2310.11136}

}

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

}