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

### 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, Valerie Novitzká (ed.), pp. 1-6. 2022. IEEE, ISBN XXXXXXXXXX.**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 = {1--6},

publisher = {IEEE},

isbn_issn = {ISBN XXXXXXXXXX},

year = {2022},

editor = {William Steingartner and Valerie Novitzká},

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}

}

### 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 (ed.), pp. 1-4. 2022. IEEE, ISBN XXXXXXXXXX.**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 = {1--4},

publisher = {IEEE},

isbn_issn = {ISBN XXXXXXXXXX},

year = {2022},

editor = {Bruno Buchberger and Mircea Marin},

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}

}

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

}

### McCarthy-Kleene fuzzy automata and MSO logics

#### Manfred Droste, Temur Kutsia, George Rahonis, Wolfgang Schreiner

Information and Computation, pp. -. 2020. Elsevier, ISSN 0890-5401. In Press. [doi]**article**{RISC6011,

author = {Manfred Droste and Temur Kutsia and George Rahonis and Wolfgang Schreiner},

title = {{McCarthy-Kleene fuzzy automata and MSO logics}},

language = {english},

abstract = {We introduce McCarthy-Kleene fuzzy automata (MK-fuzzy automata) over a bimonoid K which is related to the fuzzification of the McCarthy-Kleene logic. Our automata are inspired by, and intend to contribute to, practical applications being in development in a project on runtime network monitoring based on predicate logic. We investigate closure properties of the class of recognizable MK-fuzzy languages accepted by MK-fuzzy automata as well as of deterministically recognizable MK-fuzzy languages accepted by their deterministic counterparts. Moreover, we establish a Nivat-like result for recognizable MK-fuzzy languages. We introduce an MK-fuzzy MSO logic and show the expressive equivalence of a fragment of this logic with MK-fuzzy automata, i.e., a Büchi type theorem.},

journal = {Information and Computation},

pages = {--},

publisher = {Elsevier},

isbn_issn = {ISSN 0890-5401},

year = {2020},

note = {In Press},

refereed = {yes},

keywords = {Bimonoids, McCarthy-Kleene logic, MK-fuzzy automata, MK-fuzzy MSO logic},

sponsor = {Supported by the Austrian Research Promotion Agency (FFG) in the frame of the BRIDGE program 846003 “LogicGuard II”},

length = {23},

url = {https://doi.org/10.1016/j.ic.2019.104499}

}

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

}

### 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]**article**{RISC6117,

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

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

language = {english},

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

journal = {Transactions on Internet Research},

volume = {16},

number = {2},

pages = {4--13},

publisher = {IPSI},

isbn_issn = {ISSN 1820-4503},

year = {2020},

month = {July},

refereed = {yes},

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

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

length = {10},

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

}

### 2019

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

#### David M. Cerna

Submitted to the RISC Report Series. Feburary 2019. [xlsx] [pdf]**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 = {Altenberger Straße 69, 4040 Linz, Austria},

issn = {2791-4267 (online)}

}

### The Castle Game

#### David M. Cerna

Submitted to the RISC Report Series. 2019. [pdf]**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 = {Altenberger Straße 69, 4040 Linz, Austria},

issn = {2791-4267 (online)}

}

### Manual for AXolotl

#### David M. Cerna

Submitted to the RISC Report Series. 2019. [zip] [pdf] [jar]**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 = {Altenberger Straße 69, 4040 Linz, Austria},

issn = {2791-4267 (online)}

}