Research Seminar -- Theoretical Computer Science

Content | Material

About

Members of the chair and students involved in projects at I7 will talk about their current work in an informal setting. The seminar is organized by Maximilian (schlund@model.in.tum.de)-- just write him an e-mail if you would like to participate!

Everybody (Students, Researchers, Professors,...) is cordially invited to attend the talks--especially if you are interested in what we are doing around here!

The seminar takes place in room 03.09.014 on Mondays at 14:00 (s.t.) (deviations from this are highlighted in the table below).

Topics

Date/Time	Speaker	Topic
07.02., 13:00--13:30	Ruslán Ledesma Garza	Binary Reachability Analysis of Higher Order Functional Programs
Wed. 22.02., 16:00--17:00	René Neumann	Generating verified code using DFS as an example
28.02., 14:00--14:30	Maximilian Schlund	On the downward-closure of pumpable languages
06.03., 14:00--14:30	Javier Esparza	A Perfect Model for Bounded Verification
13.03., 14:00--14:30	Philipp Hoffmann	Discrete Strategy Improvement for Parity Games
20.03., 14:00--14:30	Klaus von Gleissenthall	An Epistemic Perspective on Concurrent Correctness
Wed. 21.03., 14:00--14:30	Corneliu Popeea	Synthesizing software verifiers from proof rules
27.03., 14:00--14:30	Corneliu Popeea	Compositional Termination Proofs for Multi-Threaded Programs
03.04., 14:00--14:30	Andreas Gaiser	Proving Termination of Probabilistic Programs Using Patterns
24.04., 14:00--14:30	Andrey Rybalchenko	Inference of Quantified Assertions
Wed. 25.04., 14:00--14:30, Room: 02.07.014	Loïg Jezequl	Modular optimal planning using weighted automata calculus
08.05., 14:00--14:30	Stefan Kugele	Cola-Demo
21.05., 14:00--14:45	Philipp Hoffmann	Determinization of Büchi-Automata

Abstracts

Binary Reachability Analysis of Higher Order Functional Programs

A number of recent approaches for proving program termination rely on transition invariants -- a termination argument that can be constructed incrementally using abstract interpretation. These approaches use a binary reachability analysis that checks if a candiate transition invariant holds for a given program. Scalability of this analysis is an imperative. For imperative programs, its efficient implementation can be obtained by a reduction to the reachability analysis, for which practical tools are available. In our work, we use the binary reachability analysis for proving termination of higher order functional programs. The crux of our approach lies in the treatment of partial application.
This is a joint work with Andrey Rybalchenko.

Generating verified code using DFS as an example

One uses model-checking to verify certain properties about programs. But how does one know that the code used for the model-checking is actually correct? One idea for a solution is to use a theorem-prover to prove correctness of the abstract algorithms paired with a code-generator that allows to create executable implementations of these algorithms.

This talk will give a general introduction to the topic using nested depth-first search as an example algorithm.

On the downward-closure of pumpable languages

The downward-closure of a language L is the set of all subsequences of words in L. It has nice applications as regular overapproximations of system behavior. It is well known that the downward-closure of every language is regular but not necessarily computable. We present a new approach for proving the effective regularity of the downward-closure for languages satisfying a certain kind of pumping lemma. This method can be used to prove the effective regularity of language families like the Context-free, Petri net and Control languages in an easy and uniform way.
This is joint work with Javier Esparza and Jerome Leroux.

A Perfect Model for Bounded Verification

Discrete Strategy Improvement for Parity Games

We discuss an algorithm by Jurdzinski and Vöge that finds winning strategies for parity games a by means of strategy improvement. While prior algorithms use real numbers and suffer from rounding errors, the given algorithm uses discrete encodings and as a result is much more intuitive and understandable.

An Epistemic Perspective on Concurrent Correctness

When we talk about sequential consistency, we usually think about it as a restriction on the order in which a concurrent library may process method calls. In this talk, we look at sequential consistency from a different point of view: that of the threads calling the library's methods. This change of perspective gives us a new understanding of sequential consistency: a computation is sequentially consistent if the threads calling the library's methods cannot distinguish the sequence of methods calls and returns from a sequence that meets the library's specification. We show that our notion of perspective yields a logical characterization of sequential consistency. Finally, we extend our logical framework to incorporate linearizability.
This is joint work with Andrey Rybalchenko.

Synthesizing software verifiers from proof rules

Automatically generated tools can significantly improve programmer productivity. For example, parsers and dataflow analyzers can be automatically generated from declarative specifications in the form of grammars, which tremendously simplifies the task of implementing a compiler.

In this talk, I will present a method for the automatic synthesis of software verification tools. Our synthesis procedure takes as input a description of the employed proof rule, e.g., program safety checking via inductive invariants, and produces a tool that automatically discovers the auxiliary assertions required by the proof rule, e.g., inductive loop invariants and procedure summaries. We show how our method synthesizes automatic safety and liveness verifiers for programs with procedures, multi-threaded programs, and functional programs. Our experimental comparison of the resulting verifiers with existing state-of-the-art verification tools confirms the practicality of the approach.
This talk presents joint work with Sergey Grebenshchikov, Nuno Lopes and Andrey Rybalchenko.

Compositional Termination Proofs for Multi-Threaded Programs

Automated verification of multi-threaded programs is difficult. Direct treatment of all possible thread interleavings by reasoning about the program globally is a prohibitively expensive task, even for small programs. Rely-guarantee reasoning is a promising technique to address this challenge by reducing the verification problem to reasoning about each thread individually with the help of assertions about other threads. In this talk, I will describe a proof rule that uses rely-guarantee reasoning for compositional verification of termination properties. The crux of our proof rule lies in its compositionality wrt. the thread structure of the program and wrt. the applied termination arguments - transition invariants. We present a method for automating the proof rule using an abstraction refinement procedure that is based on solving recursion-free Horn clauses. To deal with termination, we extend an existing Horn clause solver with the capability to handle well-foundedness constraints.
This talk presents joint work with Andrey Rybalchenko.

Proving Termination of Probabilistic Programs Using Patterns

Proving programs terminating is a fundamental computer science challenge. Recent research has produced powerful tools that can check a wide range of programs for termination. The analog for probabilistic programs, namely termination with probability one (``almost-sure termination''), is an equally important property for randomized algorithms and probabilistic protocols. We suggest a novel algorithm for proving almost-sure termination of probabilistic programs. Our algorithm exploits the power of state-of-the-art model checkers and termination provers for nonprobabilistic programs: it calls such tools within a refinement loop and thereby iteratively constructs a ``terminating pattern'', which is a set of terminating runs with probability one. We report on various case studies illustrating the effectiveness of our algorithm. As a further application, our algorithm can improve lower bounds on reachability probabilities.

Modular optimal planning using weighted automata calculus

Modular (or factored) planning is a relatively new domain in planning. It consists in exploiting the possible decomposition of many planning problems into exponentially smaller subproblems in order to efficiently solve them by parts. Even if, in the worst case, the complexity of factored planning is the same than the complexity of classical planning, in many cases of interest it is much more efficient. However, to our knowledge, no factored planning method exists to compute optimal solutions of problems. In this talk we will present a new approach to modular planning allowing to find optimal solutions thanks to the use of weighted automata calculus. The principle of this approach is to represent the set of solutions of each subproblem as a weighted automaton and apply a standard message passing algorithm to the network constituted by all these automata. This allows to compute new automata representing exactly those solutions of subproblems which are part of solutions of the global planning problem, and from that to give a globally optimal solution of this planning problem in a modular way.

Determinization of Büchi-Automata

While determinization of NFAs (=finite words) can be done via the simple powerset construction, this usually does not work for the infinite case. I will explain why and cover the main problems that arise when trying to determinize a Büchi-Automaton. The solution presented will be Safra's construction, which keeps track of all neccesary information for the transformation from nondeterministic Büchi- to deterministic Müller-/Rabin-Automata by using trees as states of the resulting automaton.
You should have basic knowledge about $\omega$-Automata.