## Ongoing Projects

### Logic Technology for Computer Science Education [LOGTECHEDU]

### Semantic Technologies for Computer Science Education [SemTech]

### Combinatorics and Codes for Information Security [SBA-K1]

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

### 2019

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

#### David M. Cerna

Feburary 2019. [pdf] [xlsx]**techreport**{RISC5885,

author = {David M. Cerna},

title = {{Evaluation of the VL Logic (342.208-9) 2018W End of Semester Questionnaire}},

language = {english},

abstract = {In this technical report we cover the choice of layout and intentions behind our end of the semester questionnaire as well as our interpretation of student answers, resulting statistical analysis, and inferences. Our questionnaire is to some extent free-form in that we provide instructions concerning the desired content of the answers but leave the precise formulation of the answer to the student. Our goal, through this approach, was to gain an understanding of how the students viewed there own progress and interest in the course without explicitly guiding them. Towards this end, we chose to have the students draw curves supplemented by short descriptions of important features. We end with a discussion of the benefits and downsides of such a questionnaire as well as what the results entail concerning future iterations of the course. },

year = {2019},

month = {Feburary},

length = {17},

type = {RISC Report Series},

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

address = {Schloss Hagenberg, 4232 Hagenberg, Austria}

}

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

#### David M. Cerna

In: T.B.D, T.B.D (ed.), Proceedings of T.B.D, pp. 1-17. 2019. T.B.D. [pdf]**inproceedings**{RISC5841,

author = {David M. Cerna},

title = {{On the Complexity of Unsatisfiable Primitive Recursively defined $\Sigma_1$-Sentences}},

booktitle = {{T.B.D}},

language = {english},

abstract = {We introduce a measure of complexity based on formula occurrence within instance proofs of an inductive statement. Our measure is closely related to {\em Herbrand Sequent length}, but instead of capturing the number of necessary term instantiations, it captures the finite representational difficulty of a recursive sequence of proofs. We restrict ourselves to a class of unsatisfiable primitive recursively defined negation normal form first-order sentences, referred to as {\em abstract sentences}, which capture many problems of interest; for example, variants of the {\em infinitary pigeonhole principle}. This class of sentences has been particularly useful for inductive formal proof analysis and proof transformation. Together our complexity measure and abstract sentences allow use to capture a notion of {\em tractability} for state-of-the-art approaches to inductive theorem proving, in particular {\em loop discovery} and {\em tree grammar} based inductive theorem provers. We provide a complexity analysis of an important abstract sentence, and discuss the analysis of a few related sentences, based on the infinitary pigeonhole principle which we conjecture represent the upper limits of tractability and foundation of intractability with respect to the current approaches.},

pages = {1--17},

isbn_issn = {T.B.D},

year = {2019},

editor = {T.B.D},

refereed = {yes},

length = {17},

conferencename = {T.B.D}

}

### A Generic Framework for Higher-Order Generalizations

#### David M. Cerna, Temur Kutsia

Technical report no. 19-01 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. 2019. [pdf]**techreport**{RISC5883,

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

title = {{A Generic Framework for Higher-Order Generalizations}},

language = {english},

number = {19-01},

year = {2019},

length = {21},

type = {RISC Report Series},

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

address = {Schloss Hagenberg, 4232 Hagenberg, Austria}

}

### The Castle Game

#### David M. Cerna

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 = {Schloss Hagenberg, 4232 Hagenberg, Austria}

}

### Manual for AXolotl

#### David M. Cerna

2019. [jar] [zip] [pdf]**techreport**{RISC5887,

author = {David M. Cerna},

title = {{Manual for AXolotl}},

language = {english},

abstract = {In this document we outline how to play our preliminary version of \textbf{AX}olotl. We present a sequence of graphics illustrating the step by step process of playing the game. },

year = {2019},

length = {9},

type = {RISC Report Series},

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

address = {Schloss Hagenberg, 4232 Hagenberg, Austria}

}

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

#### Wolfgang Schreiner

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

author = {Wolfgang Schreiner},

title = {{Theorem and Algorithm Checking for Courses on Logic and Formal Methods}},

booktitle = {{Post-Proceedings ThEdu'18}},

language = {english},

abstract = {The RISC Algorithm Language (RISCAL) is a language for the formal modeling of theories and algorithms. A RISCAL specification describes an infinite class of models each of which has finite size; this allows to fully automatically check in such a model the validity of all theorems and the correctness of all algorithms. RISCAL thus enables us to quickly verify/falsify the specific truth of propositions in sample instances of a model class before attempting to prove their general truth in the whole class: the first can be achieved in a fully automatic way while the second typically requires our assistance. RISCAL has been mainly developed for educational purposes. To this end this paper reports on some new enhancements of the tool: the automatic generation of checkable verification conditions from algorithms, the visualization of the execution of procedures and the evaluation of formulas illustrating the computation of their results, and the generation of Web-based student exercises and assignments from RISCAL specifications. Furthermore, we report on our first experience with RISCAL in the teaching of courses on logic and formal methods and on further plans to use this tool to enhance formal education.},

series = {Electronic Proceedings in Theoretical Computer Science (EPTCS)},

volume = {290},

pages = {56--75},

publisher = {Open Publishing Association},

isbn_issn = {ISSN 2075-2180},

year = {2019},

month = {April 1},

editor = {Pedro Quaresma and Walther Neuper},

refereed = {yes},

sponsor = {Linz Institute of Technology (LIT), Project LOGTECHEDU “Logic Technology for Computer Science Education” and OEAD WTZ project SK 14/2018 SemTech},

length = {20},

conferencename = {7th International Workshop on Theorem proving components for Educational software, Oxford, United Kingdom, 18 July 2018},

url = {http://dx.doi.org/10.4204/EPTCS.290.5}

}

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

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

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

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

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

language = {english},

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

year = {2019},

month = {March},

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

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

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

length = {34}

}

### A Parallel, In-Place, Rectangular Matrix Transpose Algorithm

#### Stefan Amberger

Research Institute for Symbolic Computatation (RISC), Johannes Kepler University, Linz, Austria. Master Thesis. March 2019. [pdf]**misc**{RISC5916,

author = {Stefan Amberger},

title = {{A Parallel, In-Place, Rectangular Matrix Transpose Algorithm}},

language = {english},

abstract = {This thesis presents a novel algorithm for Transposing Rectangular matrices In-place and in Parallel(TRIP) including a proof of correctness and an analysis of work, span and parallelism.After almost 60 years since its introduction, the problem of in-place rectangular matrix transpositionstill does not have a satisfying solution. Increased concurrency in today's computers, and the need for low overhead algorithms to solve memory-intense challenges are motivating the development of algorithmslike TRIP. The algorithm is based on recursive splitting of the matrix into sub-matrices, independent, paralleltransposition of these sub-matrices, and subsequent combining of the results by a parallel, perfect shuffle.We prove correctness of the algorithm for different matrix shapes (ratios of dimensions), and analyzework and span . Compared to out-of-place algorithms, TRIP, implemented in Cilk, trades work-efficiency for parallelism and for being in-place.},

year = {2019},

month = {March},

translation = {0},

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

keywords = {linear algebra, parallel computation},

length = {67}

}

### Migrating Mathematical Programs to Web Interface Frameworks

#### Hsuan-Ming Chen

Research Institute for Symbolic Computatation (RISC), Johannes Kepler University, Linz, Austria. Master Thesis. April 2019. Internationaler Universitätslehrgang: Informatics: Engineering & Management. [pdf]**misc**{RISC5917,

author = {Hsuan-Ming Chen},

title = {{Migrating Mathematical Programs to Web Interface Frameworks}},

language = {english},

abstract = {A mathematical software system, the RISC Algorithm Language (RISCAL), has beenimplemented in Java; however, it can be only executed on the local machine of the user.The aim of this master thesis is to migrate RISCAL to the web, such that users can accessthe software via a conventional web browser without needing a local installation of thesoftware. In a preparatory phase, this thesis evaluates various web interface frameworksand how these can be executed on the web. Based in the result of this investigation whichcompares the advantages and disadvantages of the frameworks, one framework is selectedas the most promising candidate for future work. The core of the thesis is then themigration of RISCAL to the web on the basis of this framework and the subsequentevaluation of how the demands have been met and how well all of the RISCAL programsare working after the migration.},

year = {2019},

month = {April},

note = {Internationaler Universitätslehrgang: Informatics: Engineering & Management},

translation = {0},

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

length = {85}

}

### 2018

### Idempotent Anti-unification

#### David M. Cerna Temur Kutsia

RISC. Technical report, Feb. 2018. Submitted for review. [pdf]**techreport**{RISC5530,

author = {David M. Cerna Temur Kutsia},

title = {{Idempotent Anti-unification }},

language = {english},

abstract = {In this paper we address two problems related to idempotent anti-unification. First, we show thatthere exists an anti-unification problem with a single idempotent symbol which has an infiniteminimal complete set of generalizations. It means that anti-unification with a single idempotentsymbol has infinitary or nullary generalization type, similar to anti-unification with two idem-potent symbols, shown earlier by Loı̈c Pottier. Next, we develop an algorithm, which takes anarbitrary idempotent anti-unification problem and computes a representation of its solution set inthe form of a regular tree grammar. The algorithm does not depend on the number of idempotentfunction symbols in the input terms. The language generated by the grammar is the minimalcomplete set of generalizations of the given anti-unification problem, which implies that idem-potent anti-unification is infinitary.},

year = {2018},

month = {Feb.},

note = {Submitted for review},

institution = {RISC},

length = {27}

}

### Teaching the Formalization of Mathematical Theories and Algorithms via the Automatic Checking of Finite Models

#### Wolfgang Schreiner, Alexander Brunhuemer, Christoph Fürst

In: Post-Proceedings ThEdu'17, Pedro Quaresma and Walther Neuper (ed.), Proceedings of 6th International Workshop on Theorem proving components for Educational software (ThEdu'17), Gothenburg, Sweden, 6 Aug 2017, Electronic Proceedings in Theoretical Computer Science (EPTCS) 267, pp. 120-139. 2018. Open Publishing Association, ISSN 2075-2180. [url] [pdf]**inproceedings**{RISC5531,

author = {Wolfgang Schreiner and Alexander Brunhuemer and Christoph Fürst},

title = {{Teaching the Formalization of Mathematical Theories and Algorithms via the Automatic Checking of Finite Models}},

booktitle = {{Post-Proceedings ThEdu'17}},

language = {english},

abstract = {Education in the practical applications of logic and proving such as the formalspecification and verification of computer programs is substantially hampered bythe fact that most time and effort that is invested in proving is actuallywasted in vain: because of errors in the specifications respectively algorithmsthat students have developed, their proof attempts are often pointless (becausethe proposition proved is actually not of interest) or a priori doomed to fail(because the proposition to be proved does actually not hold); this is afrequent source of frustration and gives formal methods a bad reputation. RISCAL(RISC Algorithm Language) is a formal specification language and associatedsoftware system that attempts to overcome this problem by making logicformalization fun rather than a burden. To this end, RISCAL allows students toeasily validate the correctness of instances of propositions respectivelyalgorithms by automatically evaluating/executing and checking them on (small)finite models. Thus many/most errors can be quickly detected and subsequentproof attempts can be focused on propositions that are more/most likely to beboth meaningful and true.},

series = {Electronic Proceedings in Theoretical Computer Science (EPTCS)},

volume = {267},

pages = {120--139},

publisher = {Open Publishing Association},

isbn_issn = {ISSN 2075-2180},

year = {2018},

editor = {Pedro Quaresma and Walther Neuper},

refereed = {yes},

keywords = {formal methods, program specification and verification, model checking, computer science education, logic},

sponsor = {Supported by the Johannes Kepler University Linz, Linz Institute of Technology (LIT), Project LOGTECHEDU "Logic Technology for Computer Science Education"},

length = {20},

conferencename = {6th International Workshop on Theorem proving components for Educational software (ThEdu'17), Gothenburg, Sweden, 6 Aug 2017},

url = {http://dx.doi.org/10.4204/EPTCS.267.8}

}

### Idempotent Generalization is Infinitary

#### David M. Cerna and Temur Kutsia

RISC. Technical report, RISC Report, 2018. [pdf]**techreport**{RISC5529,

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

title = {{Idempotent Generalization is Infinitary}},

language = {english},

abstract = {Let §\mathbf{I}_{S}$ be an equational theory s.t. for each $f\in S$, $f(x,x)=x$. Such an equational theory is said to be {\em idempotent}. It is known that the anti-unification problem (AUP) $f(a,b) \triangleq g(a,b)$ modulo $\mathbf{I}_{\lbrace f,g \rbrace}$ admits infinitely many least-general generalizers (lggs)~\cite{LPottier1989}. We show that, modulo $\mathbf{I}_{\lbrace f\rbrace}$, $f(a,f(a,b)) \triangleq f(b,f(a,b))$ admits infinitely many lggs.},

year = {2018},

howpublished = {RISC Report},

institution = {RISC},

length = {1}

}

### WebEx: Web Exercises for RISCAL

#### Wolfgang Schreiner

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

author = {Wolfgang Schreiner},

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

language = {english},

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

year = {2018},

month = {October},

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

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

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

length = {35}

}

### On the Probabilistic Model Checking of Cognitive Radio Networks and Cognitive Infocommunication Systems

#### Wolfgang Schreiner, Tamás Bérczes, János Sztrik, Hamza Nemouchi

Technical report no. 18-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. February 2018. [pdf]**techreport**{RISC5595,

author = {Wolfgang Schreiner and Tamás Bérczes and János Sztrik and Hamza Nemouchi},

title = {{On the Probabilistic Model Checking of Cognitive Radio Networks and Cognitive Infocommunication Systems}},

language = {english},

abstract = {We report on the usage of the probabilistic model checker PRISM to validate respectively falsify previouslypublished results on the performance of cognitive radio networks and other cognitive infocommunicationsystems. For this purpose, we construct formal system models in the PRISM modeling languageas Continuous Time Markov Chains (CTMCs) that are analyzed with the help of queries formulated in avariant of continuous stochastic logic (CSL). It is shown that many results can be accurately reproduced butalso that a few previously reported results are clearly erroneous. Furthermore, we report several deviationsfrom previously reported results where the reasons are unclear and need further investigation. Here a majorproblem is that the systems that have been analyzed in literature are usually just described in informallanguage which leaves ample room for interpretation. This makes the reconstruction of corresponding formalsystem models and the reproduction of performance measures a difficult task and limits the long-termscientific value of the reported results.},

number = {18-04},

year = {2018},

month = {February},

keywords = {formal methods, performance analysis, queueing systems},

sponsor = {Supported by the Stiftung Aktion Österreich-Ungarn project 96öu8 “Engineering Information Technology Modelling and Design of Cognitive Radio Networks”},

length = {24},

type = {RISC Report Series},

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

address = {Schloss Hagenberg, 4232 Hagenberg, Austria}

}

### Visualizing Execution Traces in RISCAL

#### Wolfgang Schreiner, William Steingartner

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

author = {Wolfgang Schreiner and William Steingartner},

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

language = {english},

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

year = {2018},

month = {March},

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

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

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

length = {7}

}

### Validating Mathematical Theories and Algorithms with RISCAL

#### Wolfgang Schreiner

In: Intelligent Computer Mathematics, F. Rabe, W. Farmer, G. Passmore, A. Youssef (ed.), Proceedings of CICM 2018, 11th Conference on Intelligent Computer Mathematics, Hagenberg, Austria, August 13-17, 2018, Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence 11006, pp. 248-254. 2018. Springer, Berlin, ISBN 978-3-319-96811-7. The final authenticated version is available online at Springer. [url] [pdf]**inproceedings**{RISC5704,

author = {Wolfgang Schreiner},

title = {{Validating Mathematical Theories and Algorithms with RISCAL}},

booktitle = {{Intelligent Computer Mathematics}},

language = {english},

abstract = {RISCAL is a language for describing mathematical algo-rithms and formally specifying their behavior with respect to user-definedtheories in first-order logic. This language is based on a type system thatconstrains the size of all types by formal parameters; thus a RISCALspecification denotes an infinite class of models of which every instancehas finite size. This allows the RISCAL software to fully automaticallycheck in small instances the validity of theorems and the correctness ofalgorithms. Our goal is to quickly detect errors respectively inadequa-cies in the formalization by falsification in small model instances beforeattempting actual correctness proofs for the whole model class.},

series = {Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence},

volume = {11006},

pages = {248--254},

publisher = {Springer},

address = {Berlin},

isbn_issn = {ISBN 978-3-319-96811-7},

year = {2018},

note = {The final authenticated version is available online at Springer},

editor = {F. Rabe and W. Farmer and G. Passmore and A. Youssef},

refereed = {yes},

keywords = {Formal specification, Falsification, Model checking},

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

length = {7},

conferencename = {CICM 2018, 11th Conference on Intelligent Computer Mathematics, Hagenberg, Austria, August 13-17, 2018},

url = {https://doi.org/10.1007/978-3-319-96812-4_21}

}

### Visualizing Logic Formula Evaluation in RISCAL

#### Wolfgang Schreiner, William Steingartner

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

author = {Wolfgang Schreiner and William Steingartner},

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

language = {english},

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

year = {2018},

month = {July},

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

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

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

length = {13}

}

### Formalization and Validation of Fundamental Sequence Algorithms by Computer-assisted Checking of Finite Models

#### Lucas Payr

Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, December 2018. Bachelor Thesis. [pdf]**techreport**{RISC5816,

author = {Lucas Payr},

title = {{Formalization and Validation of Fundamental Sequence Algorithms by Computer-assisted Checking of Finite Models}},

language = {english},

abstract = {While common textbooks go into great details when it comes to the analy-sis of sequence algorithms, they lack in proper proofs and moreover formalspecifications. The most essential part, the loop invariant is either describedvery vaguely or is completely missing. This thesis gives those missing spec-ifications as well as so called verification conditions upon which one canfully prove an algorithm. Normally such a process is very difficult and it iseasy to wrongly specify an algorithm. With the help of the RISC AlgorithmLanguage (RISCAL), developed at the Research Institute for Symbolic Com-putation (RISC), this process is simpler as this system provides additionalchecks that help noticing early if a specification is wrong. It uses finitemodel checking, which makes it possible to check the adequacy of speci-fications even if they include general quantifiers, which would be difficultinfinite models.The result of the thesis is a collection of specifications for various search-ing and sorting algorithms. The algorithms are implemented for differentdata types (array, recursive lists, pointer-linked lists) to serve as an additionto common textbooks.},

year = {2018},

month = {December},

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

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

sponsor = {Supported by the Johannes Kepler University, Linz, Institute of Technology(LIT) project LOGTECHEDU "Logic Technologies for Computer Science Education"},

length = {85},

type = {Bachelor Thesis}

}

### 2017

### Measuring the Gap: Algorithmic Approximation Bounds for the Space Complexity of Stream Specifications

#### David M. Cerna , Wolfgang Schreiner

In: Epic series in computer science, Mohamed Mosbah, Michaël Rusinowitch (eds). (ed.), Proceedings of SCSS 2017, 8th International Symposium on Symbolic Computation in Software Science, Epic 45, pp. 1-15. April 2017. Easy chair, ISSN 2398-7340. [url] [pdf]**inproceedings**{RISC5404,

author = {David M. Cerna and Wolfgang Schreiner},

title = {{Measuring the Gap: Algorithmic Approximation Bounds for the Space Complexity of Stream Specifications}},

booktitle = {{Epic series in computer science}},

language = {english},

abstract = {Measuring the Gap: Algorithmic Approximation Bounds for the Space Complexity of Stream Specifications},

series = {Epic},

volume = {45},

pages = {1--15},

publisher = {Easy chair},

isbn_issn = {ISSN 2398-7340},

year = {2017},

month = {April},

editor = {Mohamed Mosbah and Michaël Rusinowitch (eds).},

refereed = {yes},

length = {12},

conferencename = {SCSS 2017, 8th International Symposium on Symbolic Computation in Software Science},

url = {http://easychair.org/publications/download/Measuring_the_Gap_Algorithmic_Approximation_Bounds_for_the_Space_Complexity_of_Stream_Specifications}

}

### Ceres in Intuitionistic Logic

#### David Cerna, Alexander Leitsch, Giselle Reis, Simon Wolfsteiner

Annals of Pure and Applied Logic, pp. 1783-1836. October 2017. Elsevier, ISSN 0168-0072. [url]**article**{RISC5429,

author = {David Cerna and Alexander Leitsch and Giselle Reis and Simon Wolfsteiner},

title = {{Ceres in Intuitionistic Logic}},

language = {english},

abstract = {Abstract In this paper we present a procedure allowing the extension of a CERES-based cut-elimination method to intuitionistic logic. Previous results concerning this problem manage to capture fragments of intuitionistic logic, but in many essential cases structural constraints were violated during normal form construction resulting in a classical proof. The heart of the \{CERES\} method is the resolution calculus, which ignores the structural constraints of the well known intuitionistic sequent calculi. We propose, as a method of avoiding the structural violations, the generalization of resolution from the resolving of clauses to the resolving of cut-free proofs, in other words, what we call proof resolution. The result of proof resolution is a cut-free proof rather than a clause. Note that resolution on ground clauses is essentially atomic cut, thus using proof resolution to construct cut-free proofs one would need to join the two proofs together and remove the atoms which where resolved. To efficiently perform this joining (and guarantee that the resulting cut-free proof is intuitionistic) we develop the concept of proof subsumption (similar to clause subsumption) and indexed resolution, a refinement indexing atoms by their corresponding positions in the cut formula. Proof subsumption serves as a tool to prove the completeness of the new method CERES-i, and indexed resolution provides an efficient strategy for the joining of two proofs which is in general a nondeterministic search. Such a refinement is essential for any attempt to implement this method. Finally we compare the complexity of CERES-i with that of Gentzen-based methods.},

journal = {Annals of Pure and Applied Logic},

pages = {1783--1836},

publisher = {Elsevier},

isbn_issn = { ISSN 0168-0072},

year = {2017},

month = {October},

refereed = {yes},

length = {66},

url = {http://www.sciencedirect.com/science/article/pii/S0168007217300490}

}