Home Publications Teaching Service Thesis Contact

TEACHING


STUDENT PROJECT SUPERVISION

2020


We present an implementation of SOTER, a run-time assurance framework for building safe distributed mobile robotic (DMR) systems, on top of the Robot Operating System (ROS). The safety of DMR systems cannot always be guaranteed at design time, especially when complex, off-the-shelf components are used that cannot be verified easily. SOTER addresses this by providing a language-based approach for run-time assurance for DMR systems. SOTER implements the reactive robotic software using the language P, a domain-specific language designed for implementing asynchronous event-driven systems, along with an integrated run-time assurance system that allows programers to use uncertified components but still provide safety guarantees. We describe an implementation of SOTER for ROS and demonstrated its efficacy using a multi-robot surveillance case study, with multiple run-time assurance modules and show, through rigorous simulation, that SOTER enabled systems ensure safety, even when using unknown and untrusted components.

2019


Reactive synthesis transforms a specification of a reactive system, given in a temporal logic, into an implementation. The main advantage of synthesis is that it is automatic. The main disadvantage is that the implementation is usually very difficult to understand. In this paper, we present a new synthesis process that explains the synthesized implementation to the user. The process starts with a simple version of the specification and a corresponding simple implementation. Then, desired properties are added one by one, and the corresponding transformations, repairing the implementation, are explained in terms of counterexample traces. We present SAT-based algorithms for the synthesis of repairs and explanations. The algorithms are evaluated on a range of examples including benchmarks taken from the SYNTCOMP competition.

Automatic approaches to network intrusion detection have become indispens- able for the recognition of malicious activities within a network. With the help of network intrusion detection systems (NIDS), software applications that mon- itor a network for violations, network administrators can monitor the network against predefined attacks. With the rising complexity of modern day cyber at- tacks, there is a demand for more expressive specification languages, that allow us to specify complex attack patterns. In this thesis, we introduce a stream- based approach to network intrusion detection, based on an extension of the real-time stream language RTLola with parameterization. In contrast to most state of the art network intrusion detection systems, RTLola can express state- based properties. We address the interesting challenges posed by this strictly more expressive approach and demonstrate the features of RTLola using differ- ent real-world examples.

2018


In reactive synthesis, an implementation is automatically constructed from a formal specification. The great advantage of reactive synthesis is that the im- plementation inherently satisfies the specification. Although the development of synthesis has made significant progress in the last decade, the returned so- lution is only guaranteed to be as good as its specification. Specifications that under-specify the system may result in implementations that do not perform as intended. Skeletons for reactive systems provide an analysis technique that de- termines which parts of the implementation are determined by the specification. A skeleton is a three-valued labeled transition system that maps the output vari- ables to true, false or open. Open indicates that the value is not determined by the specification and can be chosen by the synthesis tool. An earlier work bases the satisfaction relation for skeletons on traditional word semantics: a skeleton satisfies a specification if the language of its traces satisfies the specification. The disadvantage of this definition is that there does not exist a skeleton that models a given specification if and only if the specification is realizable. In this thesis, we introduce a branching semantics for skeletons of reactive systems such that skeletons get synthesized if and only if the specification is realizable. Further, we present a method to check whether a skeleton models a specification under the branching semantics and show how to synthesize skeletons under the new semantics.

Hyperproperties are sets of sets of computation traces. They allow for formalization of information-flow policies and symmetry requirements, which are not expressible in traditional trace properties. The purpose of our work is to study the automata-theoretic approach for hyperproperties. We introduce a canonical representation for a fragment of hyperproperties and present a learning framework for these automata. The target of our representations are regular k-safety hyperproperties, the class of specifications in which violating system contains a bad-prefix of size at most k and their k-fold form a regular language. These automata represent sets of traces by using the k-fold self composition of their alphabet, we call such automata k-safety. This construction imposes an order on the sets of traces and an automaton accepting every order of traces is denoted permutation-complete. We investigate the construction of permutation-complete automata from various representations, such as HyperLTL, non-deterministic safety automata and deterministic bad-prefix automata. One construction is based on automata-transformations and a second one relies on a learning framework called L*-Hyper that extends the L*-framework for regular languages. In addition to the learner we provide an implementation of the teacher deciding membership and equivalence queries for specifications given in HyperLTL. We conclude our work by presenting new decidability results concerning the learnability of hyper- and trace properties from queries and counterexamples. These include the undecidability of membership queries for safety languages and k-safety hyperproperties and the undecidability of whether a HyperLTL formula expresses a k-safety hyperproperty. Further, we give a decision procedure for whether a HyperLTL formulas using only universal quantifiers expresses a k-safety hyperproperty.

2017


We introduce RTLola, a new stream-based specification language for the description of real-time properties of reactive systems. The key feature is the integration of sliding windows over real-time intervals with aggregation functions into the language. Using sliding windows we can detach fixed-rate output streams from the varying rate input streams. We provide an efficient evaluation algorithm of the sliding windows by partitioning the windows into intervals according to a given monitor frequency. For useful aggregation functions, the intervals allow a more efficient way to compute the aggregation value by dynamically reusing interval summaries. In general, the number of input values within a single window instance can grow arbitrarily large disallowing any guarantees on the expected memory consumption. Assuming a fixed monitor output rate, we can provide memory guarantees which can be computed a-priori. Additionally, for specifications using certain classes of aggregation functions, we can perform a more precise, better memory analysis. We demonstrate the applicability of the new language on practical examples.

2015


LOLA is a stream-based specification language for the online monitoring of synchronous systems. For this, LOLA offers two main functions. On the one hand it can serve as a verification tool and check, whether a single execution path satisfies a certain property. On the other hand it allows for the collection of statistics about the system execution. The monitoring algorithm can become inefficient, if LOLA specifications contain streams that depend on their own future values. In this thesis we will present methods to remove such forward-recursion from LOLA specifications in order to optimize the performance of the monitoring algorithm. We will use an automata-theoretic approach to optimize specifications, which are supposed to check properties, and we will use a mathematical approach to optimize specification that collect statistics. We will also present our implementation of these methods and illustrate experimental results to demonstrate the effectiveness of our optimization procedures.

We consider the model counting problem of linear-time temporal logic (LTL). LTL is a well known specification logic and a standard input language for model checking and synthesis tools of reactive systems. The LTL model counting problem distinguishes two types of models: word and tree models. Word models are labeled sequences that satisfy the formula and are bounded in length. Counting word models can be used in verification to compute the number of errors in an implementation. Tree models are labeled trees that are bounded by depth where each path satisfies the formula. Counting tree models can be seen as a quantitative extension of synthesis in which we determine the number of implementations that satisfy the formula. Unfortunately, the best counting algorithms we know has double exponential complexity in the formula for word models and threefold exponential complexity in the formula for tree models. Although this algorithm improves the naive solution in terms of complexity in the bound, both solutions are impractical and are mostly limited to formulas of small length. In this thesis, we investigate approximative algorithms that efficiently solve the LTL counting problem. We present two main techniques, namely a technique based on the ideas of bounded model checking, where both the model and the LTL formula are transformed into a SAT formula, and another technique based on Monte Carlo methods, where we compute a set of possible solutions and determine proper lower and upper bounds.

COURSES

ST 2021


This course is an introduction to the theory and applications of formal methods, a field of computer science and engineering concerned with the rigorous mathematical specification, design, and verification of systems. At its core, formal methods is about proof: formulating specifications that form proof obligations, designing systems to meet those obligations, and verifying, via algorithmic proof search, that the systems indeed meet their specifications. In particular, the course will cover topics such as model checking, Boolean satisfiability (SAT) solving and satisfiability modulo theories (SMT). These techniques have become essential tools for the design and analysis of hardware, software, and cyber-physical systems. Central themes of the course this year will include (i) the close connections between verification and synthesis, and (ii) the interplay between inductive inference (learning from examples) and deductive reasoning (logical inference and constraint solving). Based on time and interests, we will also cover other current research topics such as combining machine learning and formal methods, formal methods for safe and high assurance artificial intelligence (AI) and robotics, formal methods for building secure systems, formal methods for human-robot (human-CPS) systems, formal methods for education, etc. (Instructor: Prof. Sanjit A. Seshia)

I gave the lectures on Hyperproperties and Runtime Assurance

Click here for the course webpage.

ST 2020


This course is an introduction to the theory and applications of formal methods, a field of computer science and engineering concerned with the rigorous mathematical specification, design, and verification of systems. At its core, formal methods is about proof: formulating specifications that form proof obligations, designing systems to meet those obligations, and verifying, via algorithmic proof search, that the systems indeed meet their specifications. In particular, the course will cover topics such as model checking, Boolean satisfiability (SAT) solving and satisfiability modulo theories (SMT). These techniques have become essential tools for the design and analysis of hardware, software, and cyber-physical systems. Central themes of the course this year will include (i) the close connections between verification and synthesis, and (ii) the interplay between inductive inference (learning from examples) and deductive reasoning (logical inference and constraint solving). Based on time and interests, we will also cover other current research topics such as combining machine learning and formal methods, formal methods for safe and high assurance artificial intelligence (AI) and robotics, formal methods for building secure systems, formal methods for human-robot (human-CPS) systems, formal methods for education, etc. (Instructor: Prof. Sanjit A. Seshia)

I gave the lectures on Temporal Logocs, Hyperproperties and Runtime Assurance

Click here for the course webpage.

WT 2016/17


Runtime verification is a dynamic analysis method, where an execution of a system is checked during runtime against a specification. Runtime verification serves as a supplement to traditional verification methods, such as model checking and testing, and can be used prior to deployment for analysis and debugging purposes. The major advantage of runtime verification, however, emerges in the role it plays after deployment, for ensuring reliability, safety, and security and for providing fault containment and recovery as well as online system repair. In this seminar, we take a look into state-of-the-art methods for runtime verification, study recent developments in this field, and investigate tools for monitoring reactive systems. (Instructor: Prof. Bernd Finkbeiner)

Click here for the course webpage.

ST 2016


Embedded systems are computer systems that are encapsulated into larger products, and that are normally not directly visible to the user. Embedded systems are responsible for the information processing in transportation systems (e.g., airplanes, trains, cars), telecommunication equipment (e.g., mobile phones), and consumer electronics products (e.g., TVs, DVD-players). In this course we study the theoretical foundations and practical tools that are needed to build reliable and efficient embedded systems. An important component of the course is the project, where groups of participants design and build an embedded system. (Instructor: Prof. Bernd Finkbeiner, Dr. Swen Jacobs)

Click here for the course webpage.

WT 2015/16


Program synthesis in its classical formulation is concerned about finding a program that meets a specification given as a logical formula. Recent work on program verification and program optimization have shown potential benefits of allowing the user to supplement the logical specification with a syntactic template that constrains the space of allowed implementations. In this seminar we look into various novel approaches in program synthesis. The topics will be divided mainly into three categories. Deductive Synthesis, where synthesis is regarded as a theorem proving task, syntax-guided synthesis, where a partial program with incomplete information is completed using user-specified assertions and finally, learning-based approaches, where the synthesis procedure is formulated as a learning algorithm between an oracle and the synthesizer. (Instructor: Prof. Bernd Finkbeiner)

Click here for the course webpage.

ST 2015


In diesem Proseminar werden Sie lernen wissenschaftliche Vorträge zu halten. Sie werden sich selbstständig in ein fachliches Gebiet einarbeiten und eine Präsentation dazu ausarbeiten. Der zweistufige Seminaraufbau dient dazu, dass Sie im Laufe der Veranstaltung Rückmeldung bekommen und sich daraufhin verbessern können. Thematisch beschäftigen wir uns mit den Grundlagen von formalen Methoden zur Verbesserung von Softwarezuverlässigkeit. Die folgenden Themen werden wir voraussichtlich behandeln: Logic and Theorem Proving, Modeling Software Systems, Formal Specification, Automatic Verification, Deductive Software Verification, Process Algebra and Equivalences, Timed Automata, Software Testing, Combining Formal Methods, und Visualization (Instructor: Prof. Bernd Finkbeiner)

Click here for the course webpage.

WT 2014/15


Was ist Informatik? Was ist Programmieren? Dieser Kurs bietet eine Einführung in die grundlegenden Konzepte der Informatik und insbesondere der Programmiersprachen. Wir verwenden bewusst die funktionale Programmiersprache Standard ML, da sie die Konzepte der Informatik, insbesondere die Rekursion, einfach und klar umsetzen lässt. Der Fokus der Vorlesung liegt auf der Struktur von Programmiersprachen, welche durch Grammatiken, Inferenzregeln, und das Programmieren von Interpretern, Maschinen und Übersetzern vermittelt wird. Darauf aufbauend werden wir grundlegende Techniken wie Laufzeitbestimmungen und (Korrektheits-)Beweise über Programme behandeln. Am Ende der Vorlesung werden Sie in der Lage sein eigene Programmiersprachen zu definieren und Interpreter dafür zu schreiben. (Instructor: Prof. Bernd Finkbeiner)

Click here for the course webpage.

ST 2014


Many of todays problems in computer science are no longer concerned with programs that transform data and then terminate, but with non-terminating systems which have to interact with a possibly antagonistic environment. The emergence of so-called “reactive systems” requires new approaches to verification and synthesis. Over the course of the last fifty years it turned out to be very fruitful to model and analyze reactive systems in a game-theoretic framework, which captures the antagonistic and strategic nature of the interaction between the system and its environment. In this seminar, we will explore advanced concepts in the theory of infinite games, among them concurrent and probabilistic games, games of imperfect information, and specifications going beyond omega-regular ones. (Instructor: Prof. Bernd Finkbeiner, Dr. Martin Zimmermann)

Click here for the course webpage.

WT 2013/14


In diesem Proseminar werden Sie lernen wissenschaftliche Vorträge zu halten. Sie werden sich selbstständig in ein fachliches Gebiet einarbeiten und eine Präsentation dazu ausarbeiten. Der zweistufige Seminaraufbau dient dazu, dass Sie im Laufe der Veranstaltung Rückmeldung bekommen und sich daraufhin verbessern können. Thematisch beschäftigen wir uns mit den Grundlagen der Modellierung von Zeit in formalen Modellen. Die Literatur ist nur auf Englisch verfügbar, der Vortrag darf jedoch in Deutsch gehalten werden. (Instructor: Prof. Bernd Finkbeiner)

Click here for the course webpage.

ST 2013


How can one ensure that computer programs actually do what they are intended to do? Simply running a program repeatedly with various inputs is inadequate, because one cannot tell which inputs might cause the program to fail. It is possible to tailor a tester to test a given program, but present-day programs are so complex that they cannot be adequately checked through conventional testing, which can leave significant bugs undetected. Program verification uses mathematical and logical methods to prove that a program is correct. This approach was pioneered by, among others, Dijkstra, Floyd, Gries, Hoare, Lamport, Manna, Owicki and Pnueli. Today, we have powerful decision procedures that can, completely automatically, answer basic questions about the data types typically used by programmers. Model Checking is a “push-button” technology that can analyze finite-state abstractions of programs with as many as 1020 states. This course takes an up-to-date look at the theory and practice of program verification. (Instructor: Prof. Bernd Finkbeiner)

Click here for the course webpage.

WT 2012/13


The theory of automata over infinite objects provides a succinct, expressive and formal framework for reasoning about reactive systems, such as communication protocols and control systems. Reactive systems are characterized by their nonterminating behaviour and persistent interaction with their environment. In this course we will study the main ingredients of this elegant theory, and its application to automatic verification (model checking) and program synthesis. (Instructor: Prof. Bernd Finkbeiner)

Click here for the course webpage.

Real-time systems are an interesting class of infinite state systems. We will study timed automata, a popular formalism for the succinct representation of timed systems, featuring a decidable reachability problem. Efficient algorithms and clever data structures support the analysis of systems of larger size. Synthesizing timed controllers for plant models guarantees their correctness. We will investigate classic synthesis problems for (non-terminating) reactive systems, which have the goal to synthesize finite-state automata from temporal logic specifications. In contrast, we will also study program synthesis, which deals with terminating systems. (Instructor: Prof. Bernd Finkbeiner)

Click here for the course webpage.