Vorträge im SS 2016

Das Oberseminar des Lehrstuhls für Theoretische Informatik findet dienstags 14:15-15:45 in Raum 01.252-128 in der Cauerstr. 11 statt. Es steht Masterstudierenden und Doktoranden sowie bei Interesse Bachelorstudierenden offen. Die Themenwahl erfolgt nach Vereinbarung entsprechend den Schwerpunkten des Lehrstuhls. Nachfragen gerne per Mail an den Leiter des Lehrstuhls (mailto:lutz.schroeder@informatik.uni-erlangen.de).

Voraussichtlicher Plan für SS 2016

—

Bisherige Vorträge

Date	Speaker, Topic	Abstract
28-Jun	Peter Trommler, A Verified Digital Signature Device	Internet banking must operate under the assumption that the customer’s computer is compromised. In my talk I present a digital signature device that offers a secure environment for digital signatures. I demonstrate that in a situation where an attacker has full control over the customer’s computer the attacker cannot compromise the security of the signature device and hence issue no manipulated transactions. The verification is done by proving that the implementation satisfies light-weight behavioral interface specifications given in Frama-C’s ACSL. It must be shown that the security device behaves properly on arbitrary messages i.e. messages of arbitrary content and arbitrary length. Moreover, the security device must cope with messages sent at arbitrary times. The latter property will be shown using the Aorai Plugin for Frama-C.
21-Jun	Julian Jakob, Towards a flowchart diagrammatic language for monad-based semantics [pdf-embedder url=”/wp-content/uploads/media/ss16/ober/jakob.pdf” ]	Graphical languages have a wide range of applications across physics, mathematics, computer science and other disciplines. In my talk I present diagrammatic languages starting from a generic categorical perspective and continuing to more specific settings that represent notions of feedback, fixpoints and iteration, commenting on the known coherence results for all of them. I discuss various axiomatizations possibly including a well-established quasi-equation axiom known as the uniformity principle. Furthermore, I demonstrate the relevance of the presented material to the theory of computational effects formalized as monads and the corresponding algebraic theories. Specifically, I present an alternative direct proof of the duality of algebraic operations and generic effects valid under slightly more liberal assumptions than Plotkin and Power’s original proof.
21-Jun	Michael Banken, Simulation of counter machines	Counter machines were an important part of research on decidability in the 1960ies, as an equivalent alternative to the Turing machine. In order to make these historical models more accessible, this talk introduces Countersim, an easy to use tool for simulating these simplest types of register machines. In its current form the simulator is capable of supporting 3 important machine models, two variants of the Minsky machine, one using two registers and the other using only a single one, and the universal register machine proposed by Shepherdsen and Sturgis, which allows for the use of any number of registers. While there are of course some limitations in the programs and input values that can be accurately simulated, it should be enough for most practical purposes. The simulator is mainly intended as an educational tool, both within and outside the context of academic courses, but it may also prove useful for researchers in this field looking for a simple way to test their ideas. In order to fulfil this purpose, the simulator can be operated both as a command line tool, as well as via a graphical user interface.
14-Jun	Kristof Teichel, Design and Analysis of Cryptographically Secured Time Synchronization Methods – Second Report on the NTS Project []	The Network Time Security (NTS) specification is a collection of mechanisms for cryptographically secured time synchronization message exchanges over packet-based networks. When such measures are employed, the reliability of the clock synchronization clearly depends on the cryptographic measures. Furthermore, cryptographic measures always, to a certain degree, depend on synchronous time. This creates some interesting dependencies between timing and security which cause challenges in both the design of standard documents and the formal analysis (especially with automated tools) of developed protocols. This presentation continues and updates last year’s presentation on the NTS-related work. It provides an introduction to the relevant topics and reports on the current progress of the project. Specifically, it reports on the status of the specification design, and the standardization work that is associated with the development of the NTS documents. The presentation also provides insight on the formal analysis of certain specification parts, in particular on a UPPAAL analysis of timing aspects in broadcast mode that is currently being worked on.
7-Jun	Henning Urbat, Iterative Algebras, uniformly	The theory of iterative algebras and iterative monads, developed in the work of Adamek, Milius and Velebil (2005) and a series of subsequent papers, provides an elegant categorical framework for the study of recursive specifications. It comes in different flavors, depending on which restrictions are imposed on the “objects of variables”. For example, one may consider several types of “finite” specifications, based on either finitely presentable, finitely generated or free finitely generated objects, or make no restriction at all. In this talk, I present ongoing work towards a uniform approach to these developments. Choosing a class of “objects of variables” as a parameter, it turns out that many originally separate definitions and results can be covered in one go. This includes the construction of the rational fixpoint and its variants, as well as the characterization of iterative monads and their algebras.
31-Mai	Thorsten Wißmann, Representing Exponentiation in Nominal Sets [pdf-embedder url=”/wp-content/uploads/media/ss16/ober/wissmann.pdf” ]	Exponentiation by a fixed object E allows us to study various kinds of automata as coalgebras which have an input of type E — not only in sets but also in new settings like nominal sets in order to talk about infinite input alphabets. The exponentiation of two nominal sets X^E is not the nominal set of all maps E → X but only of those maps that are finitely supported. However, in concrete examples and for intuition, working with maps on infinite objects is not feasible. It is more helpful to work with a syntactic description in terms of operations of finite arity and equations on them. The first part of my talk contains a positive result. I will characterize exponentiation by the particular nominal set of atoms as the quotient of a polynomial functor. Then this is generalized in order to describe exponentiation by an arbitrary orbit-finite and strong nominal set E. The second part of the talk shows that the previous conditions on the exponent E are necessary for the exponentiation by E to be a quotient of a polynomial functor. Unsurprisingly, if the exponent E is not orbit-finite, then expontentiation is not finitary. More surprisingly, if the exponent is not a strong nominal set, then the exponentiation functor is not the quotient of any polynomial functor on nominal sets.
24-Mai	Ulrich Dorsch, Partition Refinement Algorithms for Equivalences of Finitary Systems [pdf-embedder url=”/wp-content/uploads/media/ss16/ober/dorsch.pdf” ]	Partition refinement algorithms can be found throughout many areas of Computer Science as efficient methods to compute equivalence relations with specific properties. My interest in partition refinement arises from the study of bisimilarity and behavioural equivalence of finitary systems (coalgebras for finitary functors). I will present the general ideas and reasons for the efficiency of some of the more well-known algorithms for Deterministic Finite Automata (Hopcroft) and Labelled Transition Systems (Paige,Tarjan), developed in the 80s and an improvement of the Paige-Tarjan algorithm for LTS by Valmari (2010). I will then present a first step towards formulating a generic partition refinement algorithm for bisimilarity/behavioural equivalence of finitary systems and a preliminary upper bound of its time complexity.
10-Mai	Daniel Hausmann, Global Caching = game solving on the fly [pdf-embedder url=”/wp-content/uploads/media/ss16/ober/hausmann.pdf” ]	The abstract concept of (infinite) games implements a separation of the structural aspects of logical problems from their algorithmical content: alternating existential and universal requirements are inherent to the related problems of model-checking and deciding satisfiability of many logics; the appropriate type of game varies though, depending on the logics at hand. For fixpoint logics, the corresponding games are (possibly) infinite and the winner of a play is most suitably determined in terms of Büchi or parity conditions. Starting with automata on infinite words, we will progress to infinite games, in particular to model-checking games and satisfiability games for the mu-calculus. Eventually we will be able to see the connection between the global caching algorithm for the flat and alternation-free coalgebraic mu-calculus (as considered in previous talks) and the game-theoretic world; as it turns out, the propagation of our algorithm in fact integrates (while arguably simplifying) several parts of the corresponding game- and automata-theoretic chain in one single step – an observation that gives rise to the title of the talk.
3-Mai	Paul Wild, Logical Relations in Coq [pdf-embedder url=”/wp-content/uploads/media/ss16/ober/wild.pdf” ]	Logical relations are a proof method to show certain properties of well-typed programs in a language, such as type safety or (contextual) equivalence of programs. The proof method works by first constructing a universe of semantic types and then showing that membership in the semantic type implies the desired property. In this talk I will first show how to construct a logical relation for System F extended with existential and recursive types. The latter will require the use of the step-indexing technique: membership in the semantic type is subject to the number of steps a program takes to reduce down to a value – when using a small-step operational semantics. Then I will show how these constructions can be formalized in the Coq proof assistant. The formalization makes use of part of the ModuRes framework for categorical logic, that provides a formalization of the category of complete ordered families of equivalences (cofes). A cofe is a set X equipped with a sequence of equivalences (=n=) such that for all n,x,y: x =(n+1)= y -> x =n= y, together with a completeness condition. Cofes provide a more abstract account of the step-indexing technique: the step index corresponds to the index into the family of equivalences. Finally, I will present some of the examples of program equivalence that can be proved in Coq using the formalization of the logical relation.
26-Apr	Sergey Goncharov, Complete Elgot Monads and Coalgebraic Resumptions [pdf-embedder url=”/wp-content/uploads/media/ss16/ober/goncharov.pdf” ]	Monads are extensively used nowadays to abstractly model a wide range of computational effects such as nondeterminism, statefulness, and exceptions. It turns out that equipping a monad with a (uniform) iteration operator satisfying a set of natural axioms allows for modelling iterative computations just as abstractly. The emerging monads are called complete Elgot monads. It has been shown recently that extending complete Elgot monads with free effects (e.g. operations of sending/receiving messages over channels) canonically leads to generalized coalgebraic resumption monads, previously used as semantic domains for non-wellfounded guarded processes. In this paper, we continue the study of the relationship between abstract complete Elgot monads and those that capture coalgebraic resumptions, by comparing the corresponding categories of (Eilenberg-Moore) algebras. To this end we first provide a characterization of the latter category; even more generally, we formulate this characterization in terms of Uustalu’s parametrized monads. This is further used for establishing a characterization of complete Elgot monads as those monads whose algebras are coherently equipped with the structure of certain algebras of coalgebraic resumption monads.
26-Apr	Christoph Egger, Fast CTL reasoning with COOL [pdf-embedder url=”/wp-content/uploads/media/ss16/ober/egger.pdf” ]	COOL gained the ability to reason in the alternation-free mu-Calculus, including its most contested fragment: CTL. One can already verify the anticipated performance of the global caching algorithm implemented in COOL providing competitive performance for its class of reasoners. I will finish the remarks on COOLs implementation and show some formulas underlining the strength of the algorithm as well as showing some potential optimization an benchmarks.
19-Apr	Stefan Milius, Formal verification of systems of synchronous software components []	Software of distributed, safety-critical embedded systems, as e.g. found in the automotive, railway or avionics domain, has to satisfy very high requirements concerning correctness and fault tolerance. Therefore standards for the development of such systems highly recommend the usage of formal methods. For many complex control tasks the preferred architecture is a system composed from components that operate synchronously but communicate asynchronously with other components — a paradigm called GALS (globally asynchronous — locally synchronous) architecture. In this talk we present an approach to close the “methodological gap” between the formal verification of synchronous components and asynchronous system of components. We mainly focus on systems where the synchronous components are implemented in SCADE (a language and modelling tool for synchronous controller software). The idea is then to abstract such concrete components with contracts, which are a mixture of temporal logic formulas and non-deterministic state machines. Formal verification of global system properties is then done on a network of contracts that has a lower complexity than the original network of concrete components. We will first explain the verfication approach in general. Then we introduce a modelling language for the specification of contracts, and we then explain the transformations used for model checking GALS systems. Our model checking method is based on bounded model checking using SAT and SMT solvers. Finally, we demonstrate the results of our approach and tool on an industrial case study.