Seminars

Thursday, August 29, 2024: Zafer Esen (University of Uppsala)

Time:?10:15 - 11:00
Location:??https://uni-regensburg.zoom-x.de/j/67760031082

Title:?Compositional Program Equivalence

Abstract: A straightforward approach to checking program equivalence is, starting from a pair of compared methods, to inline all calls and to unroll all loops, then to check that the methods return the same outputs and mutate shared data in the same way for all possible inputs. This approach does not support unbounded loops and recursion, and does not scale well to real-world programs. Furthermore, it does not exploit the similarities between programs to facilitate equivalence checking. In this talk I will give explain how the approach can be made modular by decomposing the proof (RVT's method by Godlin & Strichman), and also present a few tricks on how unbounded loops can be handled and how structural similarities between the two programs can be exploited.

Thursday, July 25, 2024:?Denghang Hu (Institute of Software Chinese Academy of Science (ISCAS))

Time:?10:15 - 11:00
Location:??BA 607?(Bajuwarenstrasse 4, 6th floor) and?https://uni-regensburg.zoom-x.de/j/9999678980

Title:?Efficient Algorithm for String Constraints with Regex-Counting and String-length

Abstract: Regular expressions (regex for short) and string length are widely used in string-manipulating programs. Counting is a frequently used feature in regexes that counts the number of sub-pattern matchings. However, string constraints with counting and length can not be solved e?iciently, especially when the counting and length bounds are large.

This presentation discusses an automata-theoretic approach to solving such string constraints. The main idea is to symbolically model the counting operators by registers in automata instead of unfolding them explicitly, thus alleviating the state explosion problem. Moreover, the string length function is modeled by a register as well.

As a result, the satisfiability of string constraints with regex counting and string length is reduced to the satisfiability of linear integer arithmetic, which the off-the-shelf SMT solvers can then solve. Various optimization techniques are also proposed to improve performance further.

49,843 string constraints with counting and string length are generated based on real-world regexes or transformed from existing ones. 49,638 of them can be solved by our solver, which is 1,917 more than the second solver ?Z3Str3RE.

Thursday, May 23, 2024: Sergey Goncharov (FAU of Erlangen and Nürnberg)

Time:?10:15 - 11:00
Location:?BA 406 (Bajuwarenstrasse 4, 4th floor) and?https://uni-regensburg.zoom-x.de/j/9999678980
?

Title:?Higher-Order Program Equivalence in the Abstract

Abstract: Reasoning about program equivalence in higher-order setting is one of the central topics in computer science, with the classical lambda-calculus as a prototypical example and with its countless flavors and extensions thereof, all the way up to Haskell and OCaml. A recently emerged program of higher-order mathematical operational semantics aims to abstract and unify reasoning methods for such languages on the basis of two parameters: the language syntax and its (small-step) operational semantics. I will present our latest results within this ongoing effort, namely, a general construction of (step-indexed) logical relations, as an abstract sound method for proving contextual equivalence of programs, i.e. their equivalent behavior under any program context.

Wednesday, March 27, 2024: Simon Guilloud (EPFL)

Time:?10:15 - 11:00
Location:?BA 607?(Bajuwarenstrasse 4, 6th floor) and?https://uni-regensburg.zoom-x.de/j/9999678980
?

Title:?Using Orthologic in Automated Reasoning

Abstract: Orthologic is a logical system whose underlying algebra is that of ortholattices (relaxations of boolean algebras which don't necessarily satisfy the distributive law). Because validity of formulas in orthologic can be decided in polynomial time, we are interested in their applicability to efficient and predictable automated reasoning. This talk will present a collection of algorithmic and logical results about orthologic, and explain how it was implemented in the program verifier Stainless and the proof assistant Lisa.

Thursday, November 30, 2023: Julie Cailler (University of Regensburg)

Time:?10:15 - 11:00
Location:?BA 607?(Bajuwarenstrasse 4, 6th floor) and?https://uni-regensburg.zoom-x.de/j/64045918898
?

Title:?Designing an Automated Concurrent Tableau-Based Theorem Prover for First-Order Logic

Abstract: Automated Theorem Proving (ATP) involves the use of formal methods to automatically (dis)prove logical formulas. Its primary applications include bug detection in critical systems and assistance in demonstrating mathematical proofs.

This talk focuses on the presentation of Goéland, a concurrent automated theorem prover, and the main challenges it encounters. These challenges include implementing a fair tableau-based proof-search procedure, addressing theory reasoning, and ensuring the generation of machine-checkable proofs.

Thursday, November 16, 2023: Franziska Alber (University of Regensburg)

Time:?10:15 - 11:00
Location:?BA 607?(Bajuwarenstrasse 4, 6th floor) and?https://uni-regensburg.zoom-x.de/j/62895178597
?

Title:?Complementation of Parametric Finite State Automata

Abstract: Finite State Automata (FSAs) are a well-researched model of computation where each FSA corresponds to a regular language. In?particular, determinisation and complementation are well-understood: while a FSA may be nondeterministic, it is always possible to?construct an equivalent deterministic FSA and use this construction to?find a FSA that corresponds to the complement language.

Parametric Automata (PAs) are a generalization of finite state automata that are suited for handling infinite alphabets (and?therefore, a wider array of formal languages). Transitions do not simply compare fixed letters, but may contain logical formulae or compare the input to nondeterministically assigned parameters. This?increased power comes at a price: there is no definite, canonical way?to define determinism for PAs, and unlike FSAs, PAs are not closed
under complementation (i.e., a complement may not exist!). We will?explore different kinds of determinism for PAs and define several?classes of PAs that can effectively be complemented.