Calendar
From PUMA Graduiertenkolleg
Monday 
Tuesday 
Wednesday 
Thursday 
Friday 
Saturday 
Sunday 

20.11

21.11

22.11

23.11

24.11
10:00 Florian Zuleger: Ranking Functions for Vector Addition Systems TUM MI 02.07.034 
25.11

26.11

27.11

28.11

29.11

30.11

01.12

02.12

03.12

Talks
DateTimeTitle
[+] 24.11.2017 10:00 Florian Zuleger: Ranking Functions for Vector Addition Systems
Abstract: Vector addition systems are an important model in theoretical computer science and have been used for the analysis of systems in a variety of areas. Termination is a crucial property of vector addition systems and has received considerable interest in the literature. In this talk we give a complete method for the construction of ranking functions for vectoraddition systems with states. The interest in ranking functions is motivated by the fact that ranking functions provide valuable additional informa
Location: TUM MI 02.07.034
Links:
[+] 04.10.2017 14:00 Axel Legay: On Statistical Model Checking
Abstract:
Model checking offers the possibility to automatically verify the correctness of complex systems or detect bugs. In many practical applications it is also useful to quantify the probability of a property (e.g.,system failure), so the concept of model checking has been extended to probabilistic systems. This form is frequently referred to as numerical model checking.
To give results with certainty, numerical model checkingalgorithms effectively perform an exhaustive traversal of the states of the system. In most real applications, however, the state space is intractable, scaling exponentially with the number of independent state variables (the state explosion problem). Abstraction and symmetry reduction may make certain classes of systems tractable, but these techniques are not generally applicable. This limitation has prompted the development of statistical model checking (SMC), which employs an executable model of the system to estimate the probability of a property from simulations.
SMC is aMonte Carlo method which takes advantage of robust statistical techniquesto bound the error of the estimated result. To quantify a property it is necessary to observe the property, while increasing the number of observations generally increases the confidence of the estimate. Rare properties are often highly relevant to system performance (e.g., bugs and system failure are required to be rare) but pose a problem for statistical model checking because they are difficult to observe. Fortunately, rare event techniques such as importance sampling and importance splitting may be successfully applied to statistical model checking.
Importance sampling and importance splitting have been widely applied to specific simulation problems in science and engineering. Importance sampling works by estimating a result using weighted simulations and then compensating for the weights. Importance splitting works by reformulating the rare probability as a productof less rare probabilities conditioned on levels that must be achieved.
In this talk, we will introduce Statistical Model Checking and summarize our contributions on importance splitting. Then, we discuss their implementation within the Plasma toolset.
Location: TUM MI 03.09.14
Links:
DateTimeTitle
[+] 30.06.2017 08:30 Felix Klaedtke: Runtime Verification of Temporal Properties over Outoforder Streams
Abstract:
In this talk, I will describe a monitoring approach for verifying systems at runtime. The approach targets distributed systems whose components communicate with the monitors over unreliable channels. In particular, I will present the approach's underlying theory, which is based on a new threevalued semantics for the realtime logic MTL. The threevalued semantics is well suited to soundly and completely reason online aboutevent streams in the presence of message delay or loss. I will also sketchits algorithmic realization for the propositional setting and its extension to data values. Furthermore, I will present initial experimental results, obtained by our prototype implementation. When messages are received out of order, the prototype processes thousands of events per second ina propositional setting and hundreds of events per second when accountingfor data values.
This is joint work with David Basin (ETH Zurich) andEugen Zalinescu (TU Munich).
Location: LMU D Z005
[+] 23.06.2017 08:30 Javier Esparza: Static Analysis of Deterministic Negotiations
Abstract:
Negotiation diagrams are a model of concurrent computation akinto workflow Petri nets. Deterministic negotiation diagrams are essentially equivalent to freechoice workflow Petri nets, but with a builtin partition of the workflow. Deterministic negotiations are surprisingly amenable to verification. Soundness and several other fundamental questions canbe decided in PTIME for sound deterministic negotiation diagrams, while they are PSPACEhard in the general case.
In this paper we generalize and explain these results. We introduce a general static analysis frameworkfor negotiations, and define Mazurkiewiczinvariant static analysis problems, which encompass the questions above and new ones.
We show that Mazurkiewiczinvariant analysis problems can be solved in PTIME for sound deterministic negotiations iff they can be solved in PTIME for sequential flowgraphseven though the flowgraph of a deterministic negotiation diagram can be exponentially larger than the diagram itself.
Our result isbased on a novel decomposition theorem, of independent interest, showingthat sound deterministic negotiation diagrams can be hierarchically decomposed into (possibly overlapping) smaller sound diagrams.
Location: LMU D Z005
Links:
[+] 09.06.2017 10:00 Christoph Haase: Presburger arithmetic and semilinear sets: the past, the present and the future
Abstract: Presburger arithmetic, the firstorder theory of the natural numbers with addition and order, is a fragment of number theory that was shown decidable in 1929 by Moj?esz Presburger in his Master's thesis. Seymour Ginsburg and Edwin Spanier showed in 1966 that the sets definable in Presburger arithmetic coincide with semilinear sets, a generalisation of ultimately periodic sets to higher dimensions. The goal of this talk is togive a comprehensive overview about Presburger arithmetic and semilinearsets, about their history and notable results. I will also discuss in more detail some recent work on the descriptive complexity of Boolean operations on semilinear sets. This talk is partly based on joint work with Dmitry Chistikov.
Location: TUM MI 02.13.010
[+] 24.05.2017 10:00 Francesco Leofante: Are you doing what you think are doing? RobustAI via verification, monitoring and repair in robotics
Abstract:
Abstract: Growing application areas for machine learning in robotics require
the exclusion or likely avoidance of unsafe behaviors. Animportant question is then, how confidence
in system behaviors obtainedfrom machine learning can be improved by formal verification.
In this talk, Francesco will overview some results obtained combining machine learning techniques
(e.g., Reinforcement Learning, Support Vector Machines) and formal verification (e.g., model checking, SMT solving)
to ensure sa
Location: TUM MI 02.07.014
DateTimeTitle
[+] 20.03.2017 15:00 David de Frutos: Understanding (Concurrent) Process Semantics [second talk]
Abstract: Once asynchronous parallellsm induces nondeterminism, the semantics of concurrent systems becomes difficult to precise. Several frameworks to state that semantics have been considered, and in any one of thema lot of different semantics have been proposed. In our seminar we will present a unified approach, where all these semantics can be presented, sothat the differences and similarities between them can be captured in aneasy way. Besides, this unified approach allows generic studies where theproperties of all the semantics can be stated and proved once and for all, thus avoiding the disturbing repetitions of the same arguments that weusually find in the literature, when any of these semantics is studied inisolation.
Location: TUM MI 00.09.038
[+] 17.03.2017 10:00 David de Frutos: Understanding (Concurrent) Process Semantics [first talk]
Abstract: Once asynchronous parallellsm induces nondeterminism, the semantics of concurrent systems becomes difficult to precise. Several frameworks to state that semantics have been considered, and in any one of thema lot of different semantics have been proposed. In our seminar we will present a unified approach, where all these semantics can be presented, sothat the differences and similarities between them can be captured in aneasy way. Besides, this unified approach allows generic studies where theproperties of all the semantics can be stated and proved once and for all, thus avoiding the disturbing repetitions of the same arguments that weusually find in the literature, when any of these semantics is studied inisolation.
Location: TUM MI 00.09.038
[+] 03.03.2017 10:00 Edon Kelmendi: Halfpositional Twoplayer Stochastic Games
Abstract: We consider zerosum stochastic games with perfect informationand finitely many states and actions. The payoff is computed by a functionwhich associates to each infinite sequence of states and actions a real number. We prove that if the the payoff function is both shiftinvariant and submixing, then the game is halfpositional, i.e. the first player hasan optimal strategy which is both deterministic and stationary.
Location: TUM MI 00.09.038
Links:
[+] 24.02.2017 10:00 David Müller: Markov Chains and Unambiguous Büchi Automata
Abstract:
Unambiguous automata are automata with at most one accepting run for every word subsuming deterministic automata. They enjoy being applicable in case where nondeterministic automata do not fit, e.g., probabilistic model checking.
In this talk I will explain a polynomial timebounded algorithm for probabilistic model checking of discretetime Markov chains against unambiguous Büchi automata specifications and compare it withknown approaches for deterministic omegaautomata, unambiguous automataover finite words and separated automata.
Location: TUM MI 00.09.038
Links:
[+] 10.02.2017 10:00 Sebastian Söntges: Feasibility Analysis of Trajectory Planning Problems of Automated Vehicles in TimeVarying Environments
Abstract:
Trajectory planning for automated vehicles is a major problem in
robotics. This problem is in particular challenging for timevarying
environments and systems with constraint dynamics. Commonly used
samplingbased planning algorithms are not complete in the sense, that
they cannot report in finite time infeasibility of the planning problem,
i.e. thenonexistence of any solution. They rely on a discretization of
the continuous space of trajectories by deterministic or probabilistic
sampling. Thereby, they discover only a subset of the set of all possible
trajectories and may show feasibility of the planning problem, but fail
to detectinfeasible problems. In this work, I present a method, which
can proveinfeasibility for a class of relevant trajectory planning
problems of twodimensional motion with bounded speed and acceleration
in timevarying environments. The proposed method computes an
overapproximative representation of the set of all reachable states of
the system at discrete pointsin time. Thus,it can formally guarantee,
that no feasible trajectory exists if the computed reachable set becomes
empty at some point in time.
Location: TUM MI 00.09.038
[+] 27.01.2017 10:00 Dmitry Zaitsev: Universal Petri and Sleptsov Nets
Abstract:
A universal Petri net (UPN) represents a processor in the Petrinet paradigm of computing [5].
A UPN executes (runs) a program specifiedby a Petri net (PN) which initial marking represents
input data and final marking represents output data.
A crucial obstacle for application of Petri nets as a generalpurpose language for concurrent
programming [5] consists in the fact they run exponentially slower comparing Turing machines.
A class of place/transition nets with multiple firing of a transition at a step has been called
Sleptsov nets. Sleptsov nets run fast compared to Petri nets [4] that opens prospects for their
practical application [3]and composition of efficient universal Sleptsov nets (USNs) [1].
A serie
Location: TUM MI 00.09.038
[+] 09.01.2017 15:00 Sergiy Bogomolov: Scalable Static Hybridization Methods for Analysis of Nonlinear Systems
Abstract:
Hybridization methods enable the analysis of hybrid automata with complex, nonlinear dynamics through a sound abstraction process. Complex dynamics are converted to simpler ones with added noise, and then analysis is done using a reachability method for the simpler dynamics. Severalsuch recent approaches advocate that only “dynamic” hybridization techniques—i.e., those where the dynamics are abstracted onthefly during a reachability computation— are effective. In this talk, we demonstrate this is not the case, and create static hybridization methods that are more scalable than earlier approaches.
The main insight in our approach is thatquick, numeric simulations can be used to guide the process, eliminating the need for an exponential number of hybridization domains. Transitionsbetween domains are generally timetriggered, avoiding accumulated errorfrom geometric intersections. We enhance our static technique by combining timetriggered transitions with occasional spacetriggered transitions,and demonstrate the benefits of the combined approach in what we call mixedtriggered hybridization. Finally, error modes are inserted to confirmthat the reachable states stay within the hybridized regions.
The developed techniques can scale to higher dimensions than previous static approaches, while enabling the parallelization of the main performance bottlene
Location: tba
Links:
[+] 16.12.2016 10:00 Tobias Heindel: Average motif counts in Markov chains of graph transformation systems
Abstract:
The dynamics of the average molecule count of a chemical species in a test tube over time is the paradigm example for motif counts in continuoustime systems with countable state space. More generally, we can consider average counts of “observable” graph motifs in Markov processes that are specified by graph transformation systems (GTS); chemical reactions are a special case. Further applications of such average counts are measuring network flows, protein production in cells, and speed of DNAwalkers.
Computing expected values of motif counts is typically extremely complicated if possible at all; it often amounts to solving the master equation of the underlying Markov chain with countable state space to suitableprecision. The case is much different if we restrict to the graph transformation analogue of contextfree Chomsky grammars, namely contextfree GTSs, aka hyperedge replacement systems. For these systems, it is alwayspossible to construct for each motif of interest a finite ordinary differential equation (ODE) that captures the time evolution of the average countof the motif precisely. To illustrate the analysis technique using ODEs,the preferential attachment process, a popular model in the context ofcitation networks, will feature as running example. Time permitting, issues of the general graph transformation case and the main ideas of how toresolve them will be overviewed.
Location: TUM MI 00.09.038
[+] 25.11.2016 11:00 Matthias Volk: Analysis of Parametric Markov Chains
Abstract: This talks presents our development in analyzing Parametric Markov Chains (PMC). PMCs extend the wellknown model of DiscreteTime MarkovChains (DTMC) by allowing to leave open certain transition probabilitiesand using parameters instead. The model checking goal then is to compute the probability of reaching certain target states which can be expressed asa rational function over the parameters. We will discuss how to efficiently compute the exact rational function by use of a state elimination approach. For better scalability, a second approximate approach transforms thePMC into a Markov Decision Process (MDP) and yields lower and upper bounds on the resulting probability. Both approaches can be used for the parame
Location: TUM MI 02.07.034
DateTimeTitle
[+] 13.09.2016 15:00 Julia Krämer: The Value of AttackDefence Diagrams
Abstract:
In an increasingly connected world, formal specification and verification of costintensive and missioncritical cyberphysical systemshave become a crucial element of design processes both in industry and research. Especially in the area of securitycritical systems, such as powerplants and water supply works, the application of these techniques can save not only costs but also human lives.
Securitycritical systems focus on robustness against attacks of malicious intruders, which, for instance, try to change the behaviour of the system or to steal secret information from it. Among the most prominent modelling techniques for securitycritical systems are attack trees. To overcome the lack of expressiveness regarding situational conditions such as timing, concurrent countermeasures of the defender, success probabilities and resources (especially costs), several extensions of attack trees have been studied recently.
In this talk, I introduce AttackDefence Diagrams as an extension of attack trees, which can represent all of the aforementioned situational conditionsat the same time. Hence, AttackDefence Diagrams serve as an overarchingnotation with respect to other existing extensions. In addition, they are equipped with a compositional semantics in terms of stochastic timed automata, which can be efficiently analysed using standard model checking tools such as the Modest Toolset. As I demonstrate by a case study from thedomain of cybersecurity, the semantics enables an efficient whatif quantitative evaluation to deliver cost and success estimates for fixed strategies. Finally, I show that the semantics naturally corresponds to a gamewhere its players compete to turn the outcome of the game from undecided to successful attack or defence, respectively. This game formalisation forms a natural basis for future work in the domain of game theory.
Location: TUM 02.07.014
Links:
[+] 24.06.2016 09:00 Sanjiva Prasad: From ABC to a LitTLe logic for mobile networks
Abstract:
We revisit the model of Abstract Switches presented in the axiomatic basis for communication (ABC) proposed by Karsten et al (SIGCOMM 2007), to examine networks whose routing behaviour can vary over time, reformulating the axioms using temporal logic.
In this framework, we examine the essence of the IPv6 protocol, a quintessential model of mobility, presenting a new proof of its correctness, i.e, that if a mobile nodes remains stationed at a host ``long enough’’, data messages addressed toit will eventually get delivered (TGC 2015).
We then show how this correctness of IPv6 (a liveness property) can be established by modelchecking a bounded liveness property on a small model, and using parametric verification techniques. This approach can be applied to IPv6 since the system eventually converges to a ``stable’' subsystem (HVC 2015).
Location: TUM MI 03.09.014
Links:
[+] 17.06.2016 09:00 Martin Hofmann: A quantitative model of the simplytyped lambda calculus
Abstract: Consider the simplytyped lambda calculus over one base type ointerpreted as the natural numbers. Suppose that the only constant is the
Location: LMU H1 1311
Links:
[+] 10.06.2016 09:00 Stefan Jaax: LimitDeterministic Büchi Automata for Linear TemporalLogic
Abstract: A Büchi automaton is said to be limitdeterministic if every state reachable from an accepting state is deterministic. In this talk we are going to present a direct construction from an LTL formula to a limitdeterministic Büchi automaton. Contrary to the indirect approach of constructing a nondeterministic automaton for the input formula and then applying a semideterminisation algorithm, our translation is compositional andhas a clear logical structure. It yields much smaller automata for formulas with deep nesting of modal operators and performs at least as well as the existing approaches on general formulas. Moreover, the resulting automaton can be directly applied to quantitative probabilistic modelchecking,using standard techniques known for deterministic automata.
Location: LMU H1 1311
Links:
[+] 03.06.2016 09:00 Andreas Lochbihler: Probabilistic functions and cryptographic oracles in higher order logic
Abstract: In this talk, I am going to present a shallow embedding of a probabilistic functional programming language in higher order logic. The language yields a framework for conducting cryptographic proofs in the computation model and having them checked by a theorem prover. The language features monadic sequencing, recursion, random sampling, failures and failure handling, and blackbox access to oracles. Oracles are probabilistic functions which maintain hidden state between different invocations. To that end, we propose generative probabilistic systems as the semantic domain in which the operators of the language are defined. We prove that these operators are parametric and derive a relational program logic for reasoning about programs from parametricity.
Location: LMU H1 1311
[+] 11.05.2016 16:00 Michael Blondin: Approaching the Coverability Problem Continuously
Abstract:
The coverability problem for Petri nets plays a central role inthe verification of concurrent sharedmemory programs. However, its highEXPSPACEcomplete complexity poses a challenge when encountered in realworld instances. In this talk, I will present a new approach to this problem which is primarily based on deciding coverability in continuous Petri nets as a pruning criterion inside a backward framework. A cornerstone of this approach is the efficient encoding into SMT of a recently developed polynomialtime algorithm for reachability in continuous Petri nets. We willsee that this approach decides significantly more instances than existingtools on standard benchmarks, and is in addition often much faster.
Joint work with Alain Finkel, Christoph Haase and Serge Haddad
Location: TUM MI 02.07.014
[+] 20.04.2016 15:00 Sander Leemans: Process mining in practice and theory
Abstract: Business processes are everywhere: from calling a bank to buying an air ticket, applying for a mortgage and sending a Whatsapp message.Most processes are supported by information systems, which typically logeverything that happens. Process mining aims to extract information from t
Location: TUM MI 02.07.014
[+] 18.04.2016 14:00 Max Haslbeck: Verified Analysis of List Update Algorithms
Abstract: We present a formalized quantitative analysis of a number of cl
Location: TUM MI 00.09.038
Links:
[+] 14.04.2016 16:00 Reza Sefidgar: Formalizing the FordFulkerson algorithm using Isabelle/HOL
Abstract: The FordFulkerson algorithm is a method for solving the MaximumFlowProblem in networks. I will introduce the idea of the algorithm andthe abstractions that Iused to model this problem in Isabelle. I also sketch the correctness proof of the FordFulkerson algorithm, and present the FordFulkerson theorem in Isablle. In my thesis I developed a verified implementation of the algorithm using refinement techniques. I will overview the steps which were applied during refinement and present the evaluation of the final code in Standard ML.
Location: TUM MI 02.07.014
Links:
[+] 14.04.2016 14:00 André Platzer: Logic of Hybrid Games
Abstract:
Hybrid systems model cyberphysical systems as dynamical systems with interacting discrete transitions and continuous evolutions along differential equations. They arise frequently in many application domains,including aviation, automotive, railway, and robotics. This talk studies hybrid games, i.e. games on hybrid systems combining discrete and continuous dynamics. Unlike hybrid systems, hybrid games allow choices in thesystem dynamics to be resolved adversarially by different players with different objectives.
This talk describes how logic and formal verification can be lifted to hybrid games. The talk describes a logic for hybrid systems called differential game logic dGL. The logic dGL can be used to study the existence of winning strategies for hybrid games, i.e. ways of resolving the player's choices in some way so that he wins by achieving his objective for all choices of the opponent. Hybrid games are determined, i.e. one player has a winning strategy from each state, yet their winning regions may require transfinite closure ordinals. The logic dGL, nevertheless, has a sound and complete axiomatization relative to any expressive logic. Separating axioms are identified that distinguish hybrid games fromhybrid systems. Finally, dGL is proved to be strictly more expressive than the corresponding logic of hybrid systems.
Location: TUM MI 02.07.014
Links:
[+] 08.04.2016 10:00 Lawrence Paulson: The First Mechanised Proof of the Second Incompleteness Theorem
Abstract: Gödel’s incompleteness theorems are famous for what they assertbut also for the elaborate techniques used in the proofs. The first incompleteness theorem (asserting that all reasonable formalisations of arithmetic leave some questions unresolved) involves coding the syntax of a formal system within its own logic to derive a contradiction. The second incompleteness theorem (asserting that no reasonable axiomatic system can proveits own consistency) is variously proved through some sort of metaargument involving the first theorem, or by using a more elaborate encoding, and in either case relying on extended proofs within an extended formal calculus. Three previous researchers formalised the first incompleteness theorem without proceeding to the second. However, the second theorem can be proved with a modest additional effort, given the right techniques. The talk will introduce the theorems and then outline the first ever formalisedproof of the second incompleteness theorem, highlighting the key technical points.
Location: TUM MI 03.09.014
[+] 06.04.2016 10:00 Stefan Hetzl: Inductive theorem proving based on tree grammars
Abstract:
This talk is about an approach to inductive theorem proving which is based on recent prooftheoretic results on the relationship betweeninduction and tree grammars.
These results suggest an algorithm for pro
Location: TUM MI 03.09.014
DateTimeTitle
[+] 30.03.2016 14:30 Rob Lewis: Automation and Computation in the Lean Theorem Prover
Abstract: Lean is a new proof environment being developed at Microsoft Research. Based on dependent type theory, Lean combines an efficient elaboration process with a powerful type class inference mechanism. We describehow these features have been used in the development of the standard library, and why they make Lean a good environment for general automated methods. Ultimately, Lean aims to bridge the gap between usercentric interactive theorem proving and machinecentric automated theorem proving. We alsooutline a novel automated procedure for proving inequalities over the real numbers that is currently being implemented.
Location: TUM MI 00.09.038
Links:
[+] 09.03.2016 10:00 Eugen Zalinescu: Failureaware Runtime Verification
Abstract:
Prior runtimeverification approaches for distributed systems are limited as they do not account for network failures and they assume that system messages are received in the order they are sent. To overcome this limitation, we present an online algorithm for verifying observed system behavior at runtime with respect to specifications written in the realtime logic MTL that efficiently handles outoforder message deliveries andoperates in the presence of failures. It uses a threevalued semantics for MTL, where the third truth value models knowledge gaps, and it resolves knowledge gaps as it propagates Boolean values through the formula structure.
(This is joint work with David Basin and Felix Klaedtke.)
Location: MI 02.07.014
[+] 26.02.2016 10:00 Dmitry Chistikov: Navigating onecounter automata: Directions in the mountains
Abstract: Onecounter automata (OCA) are finitestate automata with a counter that supports increments, decrements, and tests for zero. They correspond to an intermediate class between regular and contextfree languagesand are suitable for modeling ``counting'' phenomena. However, reasoning
Location: TUM MI 02.07.014
Links:
[+] 29.01.2016 14:00 Daniel Neider: Robust Linear Temporal Logic
Abstract: Although it is widely accepted that every system should be robust, in the sense that ``small'' violations of environment assumptions should lead to ``small'' violations of system guarantees, it is less clear how to make this intuitive notion of robustness mathematically precise. Inthis paper, we address this problem by developing a robust version of theLinear Temporal Logic (LTL) fragment that only contains the always and eventually temporal operators. We denote this new logic by rLTL$(\boxdot,\Diamonddot)$. Its formulas are syntactically identical to LTL formulas but are endowed with a manyvalued semantics that encodes robustness. In particular, the semantics of the rLTL formula $\varphi\Rightarrow \psi$ is such that a ``small'' violation of the environment assumption $\varphi$is guaranteed to only produce a ``small'' violation of the system guarantee $\psi$. In addition to introducing rLTL$(\boxdot,\Diamonddot)$, we
Location: TUM MI 02.07.014
Links:
[+] 29.01.2016 10:00 Rüdiger Ehlers: Cooperative Reactive Synthesis
Abstract: A modern approach to engineering correctbyconstruction systems is to synthesize them automatically from formal specifications. Oftentimes, a system can only satisfy its guarantees if certain environment assumptions hold, which motivates their inclusion in the system specification.Experience with modern synthesis approaches shows that synthesized systems tend to satisfy their specifications by actively working towards the violation of the assumptions rather than satisfying assumptions and guarantees together. Such uncooperative behavior is undesirable because it violates
Location: Raum 4981 (Stammgelände) https://portal.mytum.de/displayRoomMap?4981@0509
[+] 15.01.2016 10:00 Doreen Heusel: Weighted Unranked Tree Automata over Tree ValuationMonoids
Abstract: Recently, the investigation of formal languages of unranked trees has found much attention due to the development of XML and the fact that XMLdocuments can be formalized as unranked trees. With the help of weighted automata on unranked trees over semirings which were introduced by Droste and Vogler (2011), one can investigate quantitative questions on XMLdocuments. In order to obtain a logic counterpart for their weighted unranked tree automata, Droste and Vogler presented a weighted monadic second order (MSO) logic for unranked trees. Their automata capture the expressiveness of their logic but surprisingly not the other way around. We introduce a new behavior of weighted unranked tree automata and prove a characterization of this behavior by two fragments of weighted MSO logic and thereby provide a solution of the open equivalence problem of Droste and Vogler. The characterization works for valuation monoids as weight structures;they include all semirings and, in addition, enable us to cope with average. Moreover, we investigate the supports of weighted unranked tree automata and show that the support of a weighted unranked tree automaton overa zerosum free, commutative strong bimonoid is recognizable.
Location: TUM MI 02.07.014
[+] 12.01.2016 15:00 Anca Muscholl: On the verification of parametrized, asynchronous systems with shared memory
Abstract:
Verification of concurrent systems is a difficult problem in general, and this is even more the case in a parametrized setting where unboundedly many concurrent components are considered. Recently, Hague and Esparza et al. considered an architecture with a leader process and unboundedly many copies of a contributor process interacting over a shared memory. All processes in their setting are pushdown automata. Here, we extend the framework and give general languagetheoretical conditions on the classes of transition systems for leader and contributors for which safety is adecidable problem. We also discuss some questions beyond safety. (Joint work with S. LaTorre, I. Walukiewicz and M. Fortin.)
Location: TUM MI 02.07.014
[+] 08.01.2016 10:00 Manfred Kerber: Sound Auction Specification and Implementation using Isabelle
Abstract: We address two problems in auction design and practice: is a given auction design soundly specified, possessing its intended properties; and, is the design faithfully implemented when actually run? Failure oneither front can be hugely costly in large auctions. In the familiar setting of the combinatorial Vickrey auction, we use the Isabelle system to first ensure that the auction has a set of desired properties (e.g. allocating all items at nonnegative prices), and to then generate verified executable code directly from the specified design. Having established the expected results in a known context, we intend to use formal methods to verify new auction designs.
Location: TUM MI 02.07.014
[+] 21.12.2015 16:00 Jerome Leroux: Witnesses for Vector Addition Systems
Abstract: Vector addition systems or equivalently Petri nets are one of the most popular formal models for the representation and the analysis of parallel processes. Many known problems for vector addition systems are shown to be decidable thanks to the theory of wellstructured transition systems. Indeed, vector addition systems with configurations equipped with the classical pointwise ordering are wellstructured transition systems. Based on this observation, problems like the coverability or the termination are shown to be decidable. However, the wellstructured transition systems theory cannot explain the decidability of the reachability problem. Inthis presentation, we show that runs of vector addition systems can be equipped with a well quasiorder that satisfies an amalgamation property. This observation provides a unifying way for solving many problems for vector addition systems including the central reachability problem.
Location: TUM MI 02.07.014
[+] 18.12.2015 10:00 Christian Kern: The Embedded Multicore Building Blocks Library andits Verification
Abstract: In this talk, I will present the Embedded Multicore Building B
Location: TUM MI 02.07.014
Links:
[+] 11.12.2015 10:00 Jan Krcal: Scalable Analysis of Fault Trees with Dynamic Features
Abstract:
Fault trees constitute one of the essential formalisms for static safety analysis of various industrial systems. Dynamic fault trees (DFT) enrich the formalism by timedependent behaviour, e.g., repairs or functional dependencies. Analysis of DFT is so far limited to substantially smaller models than those required for, e.g., nuclear power plants.
We propose a fault tree formalism that combines both static and dynamic features, called SD fault trees. We introduce an analysis algorithm for an important subclass of SD fault trees. The algorithm (1) scales similarly tostatic algorithms and (2) allows for a more realistic analysis compared to static algorithms as it takes into account temporal interdependencies. Finally, we demonstrate the applicability of the method by an experimentalevaluation on fault trees of nuclear power plants.
Location: TUM MI 02.07.014
[+] 27.11.2015 10:00 Stefan Wagner: Empirical Results on Cloning and Clone Detection
Abstract: Cloning means the use of copypaste as method in developing software artefacts. This practice has several problems, such as unnecessaryincrease of these artefacts, and thereby increased comprehension and change efforts, as well as potential inconsistencies. The automatic detectionof clones has been a topic for research for several years now and we havemade huge progress in terms of precision and recall. This led to a seriesof empirical analyses we have performed on the effects and the amount ofcloning in code, models and requirements. We continue to investigate theeffects of cloning and work on extending clone detection to functionally similar code. This talk will give insights into how clone detection works and the empirical results we have gathered.
Location: TUM MI 02.07.014
[+] 13.11.2015 10:00 Anca Muscholl: Word transducers: from 2way to 1way
Abstract:
Twoway finitestate transducers on words are strictly more expressive than oneway transducers. It has been shown recently how to decideif a twoway functional transducer has an equivalent oneway transducer [Gauwin et al 2013], and the complexity of the algorithm is nonelementary. We propose an alternative and simpler algorithm for sweeping functionaltransducers, namely, transducers that can only reverse their head direction at the extremities of the input. Our algorithm works in doubly exponential space and, in the positive case, produces an equivalent oneway transducer of doubly exponential size. We also show that the bound on the size of the transducer is tight, and that the oneway definability problem is undecidable for nonfunctional transducers.
(joint work with F. Baschenis, O. Gauwin, G. Puppis, FSTTCS’15)
Location: TUM MI 02.07.014
[+] 16.10.2015 10:00 Alexandra Silva: NetKAT: A FORMAL SYSTEM FOR THE VERIFICATION OF NETWORKS
Abstract:
NetKAT is a relatively new programming language and logic for
reasoning about packet switching networks that fits well with the
popularsoftware defined networking (SDN) paradigm. NetKAT was
introduced quiterecently by Anderson et al. (POPL 2014) and further
developed by Foster et al. (POPL 2015). The system provides
generalpurpose programming constructs such as parallel and sequential
composition, conditional tests, and iteration, as well as
specialpurpose primitives for querying and modifying packet headers
and encoding network topologies. The language allowsthe desired
behavior of a network to be specified equationally. It has aformal
categorical semantics and a deductive system that is sound and
complete over that semantics, as well as an efficient decision
procedurefor the automatic verification of equationallydefined
properties of networks.
Location:
[+] 02.10.2015 10:00 Stefan Kiefer: On the total variation distance of labelled Markov chains
Abstract: Labelled Markov chains (LMCs) are widely used in probabilisticverification, speech recognition, computational biology, and many other fields. Checking two LMCs for equivalence is a classical problem subject to extensive studies, while the total variation distance provides a n
Location: TUM MI 02.07.014
DateTimeTitle
[+] 31.07.2015 08:00 Zuzana Komarkova: Unified View on Multiple MeanPayoff Objectives in Markov Decision Processes
Abstract: We investigate Markov decision processes (MDPs) with multiple longrun average (also called meanpayoff) objectives. There exist two diff
Location: tba
Links:
[+] 29.07.2015 09:00 Maximilian Claus: Model Checking With HigherOrder Automated Theorem Provers – A Logic Embedding Approach
Abstract:
A model checker takes two inputs: a model description (here: afinitestate imperative program) and a
putative property, which it shallthen verify. The logics in which these properties are stated, such as linear
temporal logic (LTL) or computation tree logic (CTL), are usually hardwired into the model checker to allow
for the use of a heavily optimised decision procedure. Stateoftheart examples include Spin [1] (for LTL), which
uses an automatonbased approach, and SMV [2] (for CTL), which relies on an encoding of transition relations
through binary decision
Location: TUM MI 02.07.014
Links:
20.07.2015 10:00 Sebastian Hack: AnyDSL: Building DomainSpecific Languages for Productivity and Performance
Abstract:
Location: TUM MI 02.07.014
Links:
[+] 17.07.2015 08:30 Martin Hofmann: The groupoid interpretation of type theory  a personal retrospective
Abstract:
This will essentially be the same as my invited talk at TLCA'15in Warsaw, 3rd July 2015
Back in 1994 Thomas Streicher and myself discovered the groupoid interpretation of MartinLöf's type theory which is now seen as a precursor of Homotopy Type Theory and in fact anticipated some simple cases of important ideas of Homotopy Type Theory, notably a special case of the univalence axiom. I will explain how and why we found thegroupoid interpretation, our motivations and results. I will also try togive an informed outsider's view of Homotopy Type Theory as it is today and finally give a glance at a novel application of the groupoid interpretation in the context of denotational semantics (proofrelevant logical relations).
Location: LMU D Z007
Links:
[+] 16.07.2015 14:00 Aymeric Bouzy: Nonprimitive Corecursion in Isabelle/HOL
Abstract: Codatatypes can be used to model possibly infinite data. They have been introduced in Isabelle/HOL in 2013. Since 2014, there has been a“primcorec” command as well, for defining primitively corecursive functions. We implement a foundational framework for corecursion support, corec, that offers a lot more syntactic flexibility. In particular, it allowscorecursion under friendly operations. The command corec results in much
Location: TUM MI 00.09.038
Links:
[+] 14.07.2015 14:00 Jens Oehlerking: Specification Models for CyberPhysical Systems inIndustrial Practice
Abstract:
ABSTRACT:
This talk will focus on the challenges in modeling and verification that need to be overcome to ensure the applicability of research results in industrial practice. A particular focus will be on thespecification of verification conditions, with real life examples that illustrate the limits of differentmodeling formalisms that were encounteredin practice. Based on several representative classes of specifications, this talk will discuss at how they can be modeled and how the resulting model scan be leveraged for verification and testing. The modeling formalismsconsidered in this talk include temporal logics, signal metrics and hybrid automata. Different verification and testing approaches that are of imp
Location: TUM MI 01.07.023
Links:
[+] 10.07.2015 08:30 AnnChristin Knoll: Decision Procedures for the Monadic Fragment and Guarded Negation Fragment in SPASS
Abstract:
The monadic fragment and guarded negated fragment are two decidable fragments of firstorder logic. The monadic fragment has
been knownfor a long time and decision procedures have already been implemented [Har12]. The guarded negation fragment however
has been more recently introduced. Though proven to be decidable [BtCS11], no decision procedure has yet been presented nor imple
mented. This talk gives an overview of clauses classes and decision procedures formed for the monadic fragment using the approaches of splitting and condensing in combination with ordered resolution. Their implementation will be demonstrated in the automated theoremprover SPASS 1 . Furthermore it covers ideas and experiments made to define clauses classes and to find a decision procedure for the guarded negatedfragment. Since this is an active area of research the outcome cannot exactly be predicted but there will definitely be some problems and challenges to overcome and hopefully some solutions found.
Location: LMU D Z007
Links:
[+] 03.07.2015 08:30 Tobias Nipkow: Mining the Archive of Formal Proofs
Abstract: The Archive of Formal Proofs is a vast collection of computerchecked proofs developed using the proof assistant Isabelle. We perform anindepth analysis of the archive, looking at various properties of the proof developments, including size, dependencies, and proof style. This gives some insights into the nature of formal proofs.
Location: LMU D Z007
Links:
[+] 26.06.2015 08:30 Ratul Saha: Distributed Markov Chains
Abstract: The formal verification of large probabilistic models is challenging. Exploiting the concurrency that is often present is one way to address this problem. Here we study a class of communicating probabilistic agents in which the synchronizations determine the probability distribution for the next moves of the participating agents. The key property of this class is that the synchronizations are deterministic, in the sense that anytwo simultaneously enabled synchronizations involve disjoint sets of agents. As a result, such a network of agents can be viewed as a succinct anddistributed presentation of a large global Markov chain. A rich class ofMarkov chains can be represented this way. We use partialorder notions todefine an interleaved semantics that can be used to efficiently verify properties of the global Markov chain represented by the network. To demonstrate this, we develop a statistical model checking (SMC) procedure and use it to verify two large networks of probabilistic agents. In this talk wewill give a brief overview of the model and the verification techniques,and discuss at length about potential advancements and application domains.
Location: LMU D Z007
[+] 19.06.2015 08:30 Matthias Rungger: Feedback Refinement Relations for the Synthesis of Symbolic Controllers
Abstract: We present an abstraction and refinement methodology for the automated controller synthesis to enforce general predefined specifications.The designed controllers require quantized (or symbolic) state information only and can be interfaced with the system via a static quantizer. Bothfeatures are particularly important with regard to any practical implementation of the designed controller and, as we prove, are characterized bythe existence of a feedback refinement relation between plant and abstraction. Feedback refinement relations are a novel concept of system relationsintroduced in this paper. Our work builds on a general notion of system with setvalued dynamics and possibly nondeterministic quantizers to permit the synthesis of controllers that robustly, and provably, enforce thespecification in the presence of various types of uncertainties and disturbances. We identify a class of abstractions that is canonical in a welldefined sense, and provide a method to efficiently compute canonical abstractions of perturbed nonlinear sampled systems. We demonstrate the practicality of our approach on two examples  a path planning problem for a mobile robot and an aircraft landing maneuver.
Location: LMU D Z007
[+] 18.06.2015 16:00 Nathanaël Fijalkow: Trading Bounds for Memory in Games with Counters
Abstract:
We study twoplayer games with counters played on graphs. We investigate a conjecture by Colcombet and Löding which states the existenceof a tradeoff between the size of the memory and the bound achieved on the counters. They proved that this conjecture implies the decidability of cost monadic secondorder logic over infinite trees, as well as the decidability of the RabinMostowski parity index.
We show that unfortunately
Location: TUM MI 02.07.014
Links:
[+] 12.06.2015 08:30 Matthias Althoff: Analysis of Hybrid Systems
Abstract:
In many modern systems, computing elements are tightly connected with physical entities for which the term cyberphysical systems has been established in recent years. Examples are automated vehicles, surgicalrobots, smart grids, and collaborative humanrobot manufacturing. Thislecture series (three lectures) provides the attendees with the required basics to extend formal verification techniques from discrete systems to hybrid systems (mixed discrete and continuous dynamics).
 Stability analysis of hybrid systems
 Reachability analysis of hybrid systems
 Applications
Location: LMU D Z007
[+] 05.06.2015 08:30 Matthias Althoff: Timed Automata + Modeling and Simulation of Hybrid Systems
Abstract:
In many modern systems, computing elements are tightly connected with physical entities for which the term cyberphysical systems has been established in recent years. Examples are automated vehicles, surgicalrobots, smart grids, and collaborative humanrobot manufacturing. Thislecture series (three lectures) provides the attendees with the required basics to extend formal verification techniques from discrete systems to hybrid systems (mixed discrete and continuous dynamics).
 Stability analysis of hybrid systems
 Reachability analysis of hybrid systems
 Applications
Location: LMU D Z007
[+] 29.05.2015 08:30 Matthias Althoff: Modeling and Simulation of Continuous Systems
Abstract:
In many modern systems, computing elements are tightly connected with physical entities for which the term cyberphysical systems has been established in recent years. Examples are automated vehicles, surgicalrobots, smart grids, and collaborative humanrobot manufacturing. Thislecture series (three lectures) provides the attendees with the required basics to extend formal verification techniques from discrete systems to hybrid systems (mixed discrete and continuous dynamics).
 Ordinary differential equations
 Analytical solution of ordinary differential equations
 Numerical solution of ordinary differential equations
[+] 22.05.2015 08:30 Helmut Seidl: Equivalence of Deterministic Topdown Treetostring Transducers is decidable
Abstract: We show that equivalence of deterministic topdown treetostring transducers is decidable, thus solving a long standing open problem informal language theory. We also present efficient algorithms for subclass
Location: LMU D Z007
[+] 08.05.2015 08:30 Javier Esparza: Verification of population protocols
Abstract:
Population protocols (Angluin et al., 2006) are a formal modelof sensor networks consisting of identical mobile devices. When two devices come into the range of each other, they interact and change their states. Computations are infinite sequences of interactions satisfying a strong fairness constraint.
A population protocol is wellspecified if for every initial configuration $C$ of devices, and every computation startingat $C$, all devices eventually agree on a consensus value depending onlyon $C$. If a protocol is wellspecified, then it is said to compute thepredicate that assigns to each initial configuration its consensus value.
While the predicates computable by wellspecified protocols have been e
Location: LMU D Z007
Links:
DateTimeTitle
[+] 13.03.2015 10:00 Alexander Weinert: Automatically Proving Memory Safety and Termination of CPrograms
Abstract:
Even though proving termination of a given program is undecidable in general, several approaches have been developed to show terminationof large classes of programs.
Of special interest is the analysis of realworld languages, such as C, which feature runtime memoryallocation and explicit pointerarithmetic.
In this talk, we present a method for showing termination of Cprograms.
For this, we first introduce SymbolicExecution Graphs, which represent an overapproximation of all runs of theprogram and can be used to show that it is memory safe.
We subsequentlytransform these graphs into Integer Transition Systems, whose terminationimplies termination of the program.
This technique has been implemented in the tool AProVE at RWTH Aachen University.
We also compare its results with those of other verification tools that show termination of Cprograms.
Location: TUM MI 02.07.014
Links:
[+] 16.02.2015 10:15 Andrei Popescu: Consistency of the logic of Isabelle/HOL
Abstract: Gordon's HigherOrder Logic (HOL) extends Church's HOL with rank1 polymorphism and a mechanism for nonempty type definitions carved outof existing types. In turn, the logic of Isabelle/HOL is an extension of
Location: TUM MI 01.09.014
Links:
[+] 16.02.2015 09:30 Wilayat Khan: Clientside enforcement of web session integrity through secure multiexecution
Abstract:
Sessions on the web are fragile. They have been attacked successfully in many ways, by networklevel attacks, by direct attacks on session cookies (the main mechanism for implementing the session concept) andby applicationlevel attacks where the integrity of sessions is violated by means of crosssite request forgery or malicious script inclusion.
Inthis talk, a variant of noninterference is introduced  that can be used to formally define the notion of clientside application  level web session integrity. The work also develops and proves correct an enforcement mechanism. Combined with stateoftheart countermeasures for networkleveland cookielevel attacks, this enforcement mechanism gives very strong assurance about the clientside preservation of session integrity for authenticated sessions.
Location: TUM MI 01.09.014
Links:
[+] 03.02.2015 09:30 David Pichardie: Formal Verification of a C Static Analyzer
Abstract: We report on the design and soundness proof, using the Coq proof assistant, of Verasco, a static analyzer based on abstract interpretation for most of the ISO C 1999 language (excluding recursion and dynamicallocation), which establishes the absence of runtime errors in the analyzed programs. Verasco enjoys a modular architecture that supports the extensible combination of multiple abstract domains, both relational and nonrelational. Verasco integrates with the CompCert C formallyverified compiler so that not only the soundness of the analysis results is guaranteedwith mathematical certitude, but also the fact that these guarantees carry over to the compiled executable code.
Location: TUM MI 02.07.014
[+] 02.02.2015 11:00 Xavier Rival: Construction of modular abstract domains for heterogeneous properties
Abstract: In this talk, we study the construction of shapenumeric static analysers, and the combination of several memory abstractions in a single shape analysis tool. We set up an abstract interpretation framework that allows to reason about simultaneous shapenumeric properties by combining shape and numeric abstractions into a modular, expressive abstract domain. Such a modular structure is highly desirable to make its formalisation, proof and implementation easier to perform and to get correct. Furthermore, we extend this modular abstract domains so as to combine differentmemory abstractions, for better scalability and greater expressiveness. This framework is implemented in the MemCAD static analyser.
Location: TUM MI 02.07.014
[+] 16.01.2015 10:00 Javier Esparza: Deterministic Negotiations: Concurrency for Free
Abstract:
Negotiations are a model of concurrency close to Petri nets, with multiparty negotiation as
primitive. A negotiation is sound if, whatever the current state, there is always a continuation
leading to propertermination.
We recall previous work in which we have designed a complete set of reduction rules for
so called deterministic negotiations that allow one to analyze soundness of negotiations
without explicitely constructing the (possibly exponentially larger) state space,
We then present a programming notation and show that it captures exactly the sound
deterministic negotiations.
Location: TUM MI 02.07.014
Links:
[+] 09.01.2015 10:00 Javier Esparza: Parameterized Verification of Asynchronous SharedMemory Systems
Abstract:
We characterize the complexity of the safety verification problem for
parameterized systems consisting of a leader process and arbitrarily many
anonymous and identical contributors. Processes communicate through a
shared, boundedvalue register. There is no synchronization primitive to
execute a sequence of operations atomically. The model is inspired by
distributed algorithms implemented on sensor
networks.
We analyze the complexity of the safety verification problem when processes aremodeled by finitestate machines, pushdown machines, and Turing machines.Our
proofs use combinatorial characterizations of
computations in the model, and in case of pushdownsystems, some novel
languagetheoretic constructions of independent interest.
This is joint work with Pierre Ganty and Rupak Majumdar.
Location: TUM MI 02.07.014
[+] 19.12.2014 10:00 Deepak D'Souza: Shape Analysis for Concurrent Programs
Abstract:
Shape analysis is a program analysis technique based on abstract interpretation that aims to find invariants on the shape of heap datastructures maintained by the program. Our aim in this talk to describe an efficient way of doing shape analysis for concurrent (or multithreaded) programs. The main idea is to decompose the heap into regions that are accessed in a mutuallyexclusive manner by the threads, to track the shape of these regions separately, and propagate facts about them only along synchronization points between the threads.
This is jointwork (inprogress!)with Arnab De and Suvam Mukherjee.
Location: TUM MI 02.07.014
Links:
[+] 05.12.2014 10:00 Peter Habermehl: Logics and Automata for Multiattributed Data Words
Abstract:
We consider temporal logics on multiattributed data words which are words over a finite alphabet where each position additionally carries multiple data values from an infinite domain. Multiattributed data words can model naturally executions of objectoriented or parallel systems. Recently, BDLTL was introduced as a temporal logic on data words extending LTL by navigation along positions of single data values. Allowing navigation wrt. tuples of data values makes the satisfiability problem undecidable. We therefore introduce NDLTL, an extension of BDLTL by a restrictedform of tuplenavigation. We study several of its fragments and obtain several decidability results. The proof techniques are based on translatingthe satisfiability problems to the emptiness problem of several classes ofData Automata whose emptiness
problems are then further translated intoreachability or coverability problems on counter automata.
Based on joint work with N. Decker, M. Leucker and D. Thoma from University Lübeck.
Location: TUM MI 02.07.014
[+] 07.11.2014 10:00 Marta Kwiatkowska: Automated Verification and Strategy Synthesis for Probabilistic Systems
Abstract: Probabilistic model checking is an automated technique to verify whether a probabilistic system, e.g., a distributed network protocol which can exhibit failures, satisfies a temporal logic property, for example, the minimum probability of the network recovering from a fault in agiven time period is above 0.98. Dually, we can also synthesise, from amodel and a property specification, a strategy for controlling the systemin order to satisfy or optimise the property, but this aspect has received less attention to date. In this paper, we give an overview of methodsfor automated verification and strategy synthesis for probabilistic systems. Primarily, we focus on the model of Markov decision processes and useproperty specifications based on probabilistic LTL and expected reward objectives. We also describe how to apply multiobjective model checking to investigate tradeoffs between several properties, and extensions to stochastic multiplayer games.
Location: TUM MI 02.07.014
[+] 10.10.2014 08:30 PUMA talk by Annette Bieniusa
Abstract: tba
Location: TUM MI 02.07.014
Links:
DateTimeTitle
[+] 23.07.2014 16:00 Jane Hillston: Fluid Approximation for the Analysis of Collective Systems
Abstract:
Stochastic process algebras have been used for more than 20 years for the formal description and analysis of quantitative aspects of system behaviour. However, like all discrete state representations, they suffer from problems of state space explosion, meaning that analysis becomes intractable as the size of the system grows. Nevertheless a process algebra has many attractive features for modelling collective systems which consist of multiple instances f simple components interacting as populations.
In this talk I will briefly introduce the stochastic process algebraPEPA and review its Markovian semantics which can be used to study aspects of dynamic behaviour. I will then explain how these semantics may be rigorously approximated, in the case of collective systems, by a set of ordinary differential equations. These equations which are more efficient to analyse and are scalefree, in the sense that the equations remain thesame as the populations grow.
Location: TUM MI 02.07.014
[+] 16.07.2014 10:00 Anca Muscholl: Distributed synthesis for acyclic architectures
Abstract:
Synthesizing distributed systems from specifications is an attractive
objective, since distributed systems are notoriously difficult toget
right. Unfortunately, there are very few known decidable frameworks
for distributed synthesis. We study a framework for synthesis
of open systems that is based on rendezvous communication and causal
memory. In particular, causal memory implies that specifications can talk about
whena communication takes place, but cannot limit information that is
transmitted during communication. This choice is both realistic and
avoids some pathological reasons for undecidability. We show
a decidability resultfor Zielonka automata with acyclic communication graphs
and local omegaregular specifications. This is joint work with I. Walukiewicz.
Location: TUM MI 02.07.014
[+] 04.07.2014 08:30 Two Worlds Apart: Bridging the Gap Between Physical and Cyber Worlds by Majid Zamani
Abstract: The tight interaction of computational systems within the physical world, known as CyberPhysical Systems (CPSs), is believed to carrygreat promises for the competitiveness of many safety critical industries.Examples of such safety critical systems include aerospace, chemical processes, automotive, energy, robotics, healthcare, etc. Within CPSs,embedded control software plays a significant role by monitoring and adjusting several physical variables through feedback loops. Although CPSs havebecome ubiquitous in modern technology, the design of embedded control software is still based on adhoc solutions. In order to detect and eliminate embedded design flaws, a large portion of the design budget is consumed with validation and verification tests. In this talk, I will propose anew approach for the design of embedded control software by changing the emphasis from verification to design. I will show that it is possible to synthesize correctbydesign embedded control software for CPSs while providing formal guarantees of correctness and preventing the need for costly post facto verifications. In particular, I will show our techniques on thesynthesis of correctbydesign embedded control software enforcing discrete specifications on (stochastic) continuous systems. Case studies from energy systems and motion planning will be employed to elucidate the results.
Location: LMU room E 210, Geschw.SchollPl. 1 (E)
Links:
[+] 27.06.2014 08:30 An SMTbased Approach to Coverability Analysis by Philipp Meyer
Abstract:
Model checkers based on Petri net coverability have been used
successfully in recent years to verify safety properties of concurrent
sharedmemory or asynchronous messagepassing software. We revisit a
constraint approach to coverability based on classical Petri net
analysis techniques. We show how to utilize an SMT solver to implement
the constraint approach, and additionally, to generate an inductive
invariant from a safety proof. We empirically evaluate our procedure
on a large set of existing Petri net benchmarks. Even though our
technique is incomplete, it can quickly discharge most of the safe
instances. Additionally, the inductive invariants computed are usually
orders of magnitude smaller than those produced by existing solvers.
Joint work with Javier Esparza, RuslánLedesmaGarza, Rupak Majumdar
and Filip Niksi, to appear in CAV 2014.
Location: LMU room E 210, Geschw.SchollPl. 1 (E)
Links:
[+] 13.06.2014 08:30 Introducing LoLA 2.0: Explicit State Space Exploration for Petri Nets by Karsten Wolf
Abstract:
This is the first public presentation of a complete reimplementation of
the LoLA (a LOw Level petrin net Analyzer) verification tool. Using this tool as an example, we survey successful techniques in the areaof explicit state space verification. We demonstrate how (and where) to successfully apply these techniques.
Location: LMU
[+] 06.06.2014 14:30 When the decreasing sequence fails by Nicolas Halbwachs
Abstract:
The classical method for program analysis by abstract interpretation
consists in computing a increasing sequence with widening, which converges towards a correct solution, then computing a decreasing sequenceof correct solutions without widening. It is generally admitted that, when the decreasing sequence reaches a fixpoint, it cannot be improved further. As a consequence, all efforts for improving the precision of an analysis have been devoted to improving the limit of the increasing sequence.In this paper, we propose a method to improve a fixpoint after its computation. The method consists in projecting the solution onto wellchosen components and to start again increasing and decreasing sequences from the result of the projection.
Location: Garching  FMI 02.07.014
Links:
[+] 26.05.2014 17:00 Coinduction, Equilibrium and Rationality of Escalation Pierre Lescanne, ENS Lyon
Abstract:
Escalation is the behavior of players who play forever in the same
game. Such a situation is a typical field for application of
coinduction which is the tool conceived for reasoning in infinite
mathematicalstructures. In particular, we use coinduction to study
formally the gamecalled dollar auction, which is considered as
the paradigm of escalation. Unlike what is admitted since 1971, we
show that, provided oneassumes that the other agent will always stop,
bidding is rational, because it results in a subgame perfect
equilibrium. We show that this is not the only rational strategy
profile (the only subgame perfect equilibrium). Indeed if an agent
stops and will stop at every step, whereas theother agent keeps
bidding, we claim that he is rational as well becausethis corresponds
to another subgame perfect equilibrium. In the infinitedollar
auction game the behavior in which both agents stop at each stepis
not a Nash equilibrium, hence is not a subgame perfect equilibrium,
hence is not rational. Fortunately, the notion of rationality based
oncoinduction fits with common sense and experience. Finally the
possibility of a rational escalation in an arbitrary game can be
expressed as a predicate on games and the rationality of escalation in
the dollar auctiongame can be proved as a theorem which we have
verified in the proof assistant COQ. In this talk we will recall the
principles of infinite extensive games and use them to introduce
coinduction and equilibria (Nash equilibrium, subgame perfect
equilibrium). We will show how one can prove that the two strategy
profiles presented above are equilibria and how thisleads to a
rational escalation in the dollar auction. We will show that
escalation may even happen in much simpler game named 0,1game.
Location: TUM Garching  Room 01.11.018
[+] 19.05.2014 15:00 Treffen mit Siemens im PUMA Graduiertenkolleg
Abstract:
Wir betrachten ein verteiltes System an Steuergeräten und betreiben
dieses als nichtfunktionale Plattform. Das bedeutet, dass auf dieser
Mengen an Steuergeräten beliebige Fahr und Assistenzfunktionen
installiert und zusätzliche Steuergeräte ins Netzwerk eingebracht werden
können. Eine SWSchicht (RTE = Runtime Environment) gewährleistet alle
nichtfunktionalen Eigenschaften des Datenaustauschs zwischen Fahr und
Assistenzfunktionen sowie deren Ausführung.
Die RTE entkoppelt die funktionalevon der physikalischen Schicht und
kapselt Mechanismen mit dem Ziel nichtfunktionale Qualitäten
sicherzustellen. Jenseits der RTE betrachten wireine Sensordatenfusion
sowie ein Fahrzeug und Umgebungsmodell.
In allen drei Bereichen würden wir gerne prüfen, in wie weit Methoden
der formalen Verifkation Anwendung finden können.
Location: TUM Garching, room MI 02.07.014
Links:
[+] 09.05.2014 14:00 Utilisation of formal methods for cyber security at FireEye
Abstract:
The talk will first provide some background information about the challenges of
operatingsystem verification and the results achieved so far. I will then
present FireEye's approach for improving cyber security. Finally, I introduce
the new research and development center at Dresden and talk about our goal to
use formal methods to further improve FireEye's products.
Location: TUM Garching  FMI 01.11.018
Links:
[+] 02.05.2014 08:30 On Refinements of Boolean and Parametric Modal Transition Systems
Abstract:
We consider the extensions of modal transition systems (MTS),namely
Boolean MTS and parametric MTS and we investigate the refinement
problems over both classes. Firstly, we reduce the problem of modal
refinement over both classes to a problem solvable by a QBF solver and
provide experimental results showing our technique scales well.
Secondly, we extend the algorithm for thorough refinement of MTS
providing better complexity then via reductions to previously studied
problems. Finally, we investigate the relationship between modal and
thorough refinement on the two classes and show how the thorough
refinement can be approximated by the modal refinement.
Location: LMU E210
Links:
[+] 25.04.2014 08:30 Interprocedural Analysis of HyperSafety Properties
Abstract:
Location:
DateTimeTitle
03.03.2014 10:30 Rizaldi Albert: Logic and Verification of Markov Automata
Abstract:
Location: TUM Garching  02.07.014
Links:
03.03.2014 10:00 Rizaldi Albert: Modelling Environment of Insulin Pumps in EventB.
Abstract:
Location: TUM Garching  02.07.014
Links:
07.02.2014 10:00 König Barbara: Behavioural Metrics  A Coalgebraic Approach
Abstract:
Location: TUM Garching  02.07.014
Links:
[+] 22.01.2014 15:00 Dawar Anuj: On Tractable Approximations of Graph Isomorphism
Abstract:
In this talk I will talk of families of equivalence relations that
approximate graph isomorphism and are polynomialtime decidable. The
WeisfeilerLehman method provides one such family which has a large
variety of equivalent characterisations emerging separately from
algebra,combinatorics and logic, which I will review. It is known
(by CaiFuererImmerman 1992) that no fixed level of the hierarchy
exactly characterises isomorphism. This has recently inspired the
definition of a new hierarchy of equivalences, which I will present,
which can be seen as a strengthening of the WL method to algebras
over finite fields.
This is joint work with Bjarki Holm.
Location: TUM Garching  03.011.018
[+] 10.12.2013 16:00 Thiagarajan P.S.: Distributed Markov CHains
Abstract: TBA
Location: TUM Garching  02.13.010
[+] 09.12.2013 16:00 Thiagarajan P.S.: Analysis of Continuous Dynamical Systems Via Statistical Model Checking
Abstract:
Systems with realvalued variables that evolve continuously w.r.t. time arise
in many settings including cyberphysical systems and biochemical networks.
The dynamics of these variables will be typically specified in terms of differ
ential equations. An important verification taskis to determine whether the
global behavior of the system has the required reachability properties. The
number of the the realvalued variables can be large and their dynamics can
be nonlinear. Further, there can bemultiple modes of behavior where each
mode is governed by a different system of differential equations. Hence such
systems can seldom be analyzedeffectively let alone efficiently.
We advocate statistical model checkingas an approximate but scalable
analysis technique in these settings. Thebasic idea is to assume a proba
bility distribution over the initial states of the system. This in turn under
suitable continuity assumptionsinduces a distribution over the trajectories
generated by the initial states. Hence one can construct a statistical model
checking procedure to verify interesting dynamical properties using a simple
sequential hypothesis testing method. We demonstrate the applicability of
this approach usinga number of large biopathways models.
Location: TUM Garching  03.13.010
[+] 09.12.2013 10:00 Thiagarajan P.S.: Approximate Verification of the Symbolic Dynamicsof Markov Chains
Abstract:
We view a Markov chain as a linear transform operating over probability
distributions over the states of the Markov chain. The iterativeapplications
of the chain M (i.e. its transition matrix) to an initial distribution over
the states will generate the trajectory. Thus a set of initial distributions will
induce a set of trajectories. It is an interesting and useful task to analyze the
dynamics of M as defined by this set of trajectories.
The novel idea here is to carry out this task in a symbolic framework.
Specifically, we discretize the probability value space [0, 1] into a finite set of intervals I. A concrete probability distribution mu over the node of M is then symbolically represented as a tuple of intervals drawn from I where the ith component of the tuple will be the interval in which mu(i) falls. The set of these discretized distributions is afinite alphabet.
Hence each trajectory will induce an infinite string over this alphabet. Given
a set of initial distributions, the symbolic dynamics of M will then consist of
an infinite language L.
The goal is to verify whether L meets a specification given as a linear time
temporal logic formula. In our logic an atomic proposition will assert that
the current probability of a node falls in the interval I. Assuming
L can be computed effectively, one can hope to solve our model checking
problem usingstandard techniques in case L is an omegaregular
language. However we show that this is not always the case. Consequently,
we develop the notionof an epsilonapproximation, based on the transient and long term behaviors of M . Briefly, a symbolic trajectory is an epsilonapproximation ofanother one iff (1) they agree during their transient phases;
and (2) both trajectories are within an epsilonneighborhood at all times after thetransient phase. Our main (related) results are that one can effectively check whether (i) for each infinite word in L, at least one of its epsilonapproximations satisfies the given specification; (ii) for each infiniteword in L, all its epsilonapproximations satisfy the specification. These verification results are strong in that they apply to all finite stateMarkov chains.
Location: TUM Garching  00.12.019
[+] 05.12.2013 16:00 Middeldorp Aart: Beyond Peano Arithmetic  Automatically Proving Termination of the Goodstein Sequence
Abstract:
Kirby and Paris (1982) proved in a celebrated paper that a theorem
of Goodstein (1944) cannot be established in Peano (1889) arithmetic.
We present an encoding of Goodstein's theorem as a termination problem
of a finite rewrite system. Using a novel implementation of ordinal
interpretations, we are able to automatically prove termination of
this system, resulting in the first automatic termination proof for
a system whosederivational complexity is not multiply recursive.
In this talk, whichis based on joint work with Sarah Winkler and
Harald Zankl, we also discuss the challenges when implementing the
elementary interpretations of Lescanne (1995).
Location: TUM Garching  Room 00.09.038
[+] 29.11.2013 10:00 Kretinsky Jan: Some recent advances in probabilistic model checking
Abstract:
Many probabilistic systems ranging from protocols to medical devices
can be
modelled as Markov decision processes (MDP).
Although theanalysis of finitestate MDPs has proved useful and practical
in many cases, it is still impossible to verify complex properties or
MDPswith hugestate spaces. We show some approaches tackling these
problems in
the recent 3 years. Firstly, for checking more complex properties, we show
how to encode them in automata efficiently so that the product of the
MDPand the automaton is smaller and faster to analyze. Secondly, for
huge
MDPs, one can employ statistical model checking based on simulations and
machine learning methods. These approaches have already led to speed
ups in
orders of magnitude, but still offer plenty of open questions and
possibilities for vast improvements.
Location: TUM Garching  02.07.014
[+] 18.11.2013 16:00 Mueller Christian: Modular Interprocedural Verification using Interpolant Function Summaries
Abstract:
When model checking large software projects, one has to deal with the
state space explosion problem. This means we have to rely on finite abstractions of the state space that can be refined gradually.
To be able to reason efficiently about interprocedural traces, it is
neccessaryto abstract away function calls and reuse information on every
call site. This can be accomplished by using Function Summaries, which
should berefinable, reusable and only be computed as needed.
In this thesis, we propose a novel algorithm that uses an SMTSolver to
compute Interpolant Function Summaries which can be refined on demand,
reused in every calling context, and eliminate the need to inline other
functions.
We willshow how this can be used to augment the concept of Trace
Refinement andfind considerable improvements when dealing with function
calls.
Location: TUM Garching  02.07.014
[+]
15.11.2013
10:00
Althoff Matthias: Formal Verification of CyberPhysical Systems
Abstract:
Functionality, autonomy, and complexity of products and production
processes is steadily increasing due to growing computing resources. The
advanced capabilities of new systems make it possible to automate tasks
that were previously performed by humans, such as (semi)automated
operation of road vehicles, surgical robots, smart grids, flight control
systems, and collaborative humanrobot systems, to name only a few.It
is obvious that most of those systems are either safety or
operationcritical, demanding methods that automatically verify their
safety andcorrect operation.
In this talk, I present reachability analysis as amethod to formally
verify cyberphysical systems. I use hybrid automata to jointly model
the discrete behavior of computing elements and the continuous behavior
of the physical elements. Based on this modeling formalism, I present
algorithms for reachability analysis, which automatically explore all
possible states of the system for a given set of initial states,
parameters, and inputs. If the set of reachable states is not in a set
of forbidden states, the correct behavior of the system is proven. Note
that this is not possible with classical simulation techniques, since
they only generate a finite and thus incomplete set of behaviors.
Theapplicability of the method is demonstrated for autonomous driving,
phaselocked loops, and smart grids. In the remainder of the talk,
futureresearch directions for compositional verification, modelbased
design techniques, and faulttolerant systems are suggested.
Location: TUM Garching  02.07.014
DateTimeTitle
[+] 30.08.2013 10:00 Losa Giuliano: Reasoning about adaptive distributed algorithms
Abstract:
To reach practical performance, distributed algorithm must dynamically
adapt to their environment (faults, asynchrony, load, contention...).
Adaptive distributed algorithms often achieve dynamic adaptationby
switching between several modes, each mode being a complex algorithmon
its own. The interaction between modes presents a challenge to formal
verification. Indeed, we do not know of any formally verified adaptive
distributed algorithm.
We present a framework in which each mode of an adaptive distributed
algorithm can be specified and verified independentlyof the other
modes. We demonstrate that our framework enables verifyingadaptive
distributed algorithms using several examples formalized in TLAand
Isabelle/HOL.
Location: TUM Informatik  room 00.09.038 (Garching)
Links:
[+]
23.08.2013
10:00
Tankink Carst: Documentation and Formal Mathematics: Web Technologymeets Proof Assistants
Abstract:
As the field of interactive theorem proving gains more highimpact projects
(both in mathematics and computer science), it becomes a necessity to document
and disseminate the artefacts of formal proof, in particular the proof scripts
used as input to the proof assistant.
In thistalk, I will describe several workflows for describing and publishing
formal proofs, using modern web technologies. These workflows are implemented in
a single prototype 'Wiki' platform, that supports formalizationsin the Coq and
HOL Light proof assistants, and I will use the system todemonstrate some of the
workflows.
Location: Garching FMI 00.09.38
Links:
[+] 21.08.2013 14:00 Kuehlwein Daniel: MaSh: Machine Learning for Sledgehammer
Abstract:
Sledgehammer integrates automatic theorem provers in the proofassistant
Isabelle/HOL. A key component, the relevance filter, heuristically ranks the
thousands of facts available and selects a subset, basedon syntactic similarity
to the current goal. We introduce MaSh, an alternative that learns from
successful proofs. New challenges arose from our
Location: Garching FMI 00.09.38
Links:
[+] 26.07.2013 10:00 Runkler Thomas: Machine Learning, industrial applications at Siemens, and an application to program analysis
Abstract: This talk will start with a short overview on machine learningmethods, from supervised through unsupervised to reinforcement learning.It will then sketch some realworld applications of machine learning at Siemens in the industrial and energy domains. Finally, the talk will focu
Location: LMU main building A020
[+] 17.07.2013 14:00 Avigad Jeremy: Dirichlet's theorem and the evolution of higherorder reasoning in mathematics
Abstract:
In 1837, Peter Gustav Lejeune Dirichlet proved that there areinfinitely many
primes in any arithmetic progression in which the terms do not all have a common
factor. This beautiful and important result was seminal in the use of analytic
methods in number theory.
Contemporary presentations of Dirichlet's proof are manifestly higherorder. To
prove the theorem for an arithmetic progression with common difference k, one
considers the set of Dirichlet characters modulo k\, which are certain types of
functions from the integers to the complex numbers. One defines the Dirichlet
Lseries L(s, chi), where s is a complex number and chi isa character modulo
k. One then sums certain expressions involving the Lseries over the set of
characters.
This way of thinking about characters, which involves treating functions as
objects just like the natural numbers, was not available in the middle of the
nineteenth century. Subsequent presentations of Dirichlet's theorem from
Dedekind to Landau show agradual evolution towards the contemporary viewpoint,
shedding light onthe development of modern mathematical method.
Location: Garching MI 00.09.038
Links:
[+]
12.07.2013
10:00
Broadbent Christopher: CSHORe and HorsSat(T): Saturation based higherorder model checking in practice.
Abstract:
Higherorder recursion schemes (HORS) are a kind of grammar whose nonterminals
are simply typed. They provide a precise model of controlflow in programs featuring
higherorder recursive functions. The modelchecking of HORS has various applications
including the flow analysis andverification of safety properties of such programs.
Collapsible Pushdown Systems (CPDS) are a generalisation of pushdown systems
with a nestedstack structure. CPDS are equiexpressive with HORS. In ICALP 2012
we presented a `saturation algorithm' for checking safety properties of CPDS
(in particular generalising [Bouajjani, J. Esparza, and O. Maler 1997] and
[A. Finkel, B. Willems, and P. Wolper, 1997], which operate on ordinary
pushdown automata).
This talk will present the ideas behind CSHORe, a modelchecking tool for HORS
that is based on CPDS saturation and whose performance is not completely
unpromising!
We will also give an overview of the tool HorsSat(T), which implements
two algorithms, each of which uses saturationlike principles.
In contrast to CSHORe, these operate directly on HORS (rather than CPDS) and
adopt the more traditionalapproach of using intersection types to reason
about their behaviour.
***CSHORe is joint work with Arnaud Carayol, Matthew Hague and OlivierSerre (to appear in ICFP 2013). HorsSat(T) is joint work with Naoki Kobayashi (to appear in CSL 2013)***
Location: LMU main building, A020
[+] 05.07.2013 10:00 Lammich Peter: Dynamic Pushdown Networks with Join and Contextual Locking
Abstract:
Dynamic pushdown networks (DPNs) are a model for concurrent programs
with procedures and threadcreation. In this talk, we present an
extension of DPNs that support joinoperations and contextual locking. A
join operation allows a thread to wait for the threads that it created
toterminate, and contextual locking allows the acquisition and release
oflocks, where a procedure may only release locks that it acquired, and
must release all locks before it returns.
Our main results are that reachability is already PSPACEcomplete for a
constant number of locks and 3processes.
For dynamic thread creation without joining, the problem remains
PSPACEcomplete, if we are only interested in reaching a configuration
where a constantsize subset of the processes is in certain states.
Moreover, reachability of configurations described by a regular language
is still decidable, even if we allow joining of processes.
joint work with Markus MuellerOlm, Helmut Seidl, and Alexander Wenner
Location: LMU main building, A020
[+] 28.06.2013 10:00 Heljanko Keijo: Using Unfoldings in Automated Testing of Multithreaded Programs
Abstract:
In multithreaded programs both environment input data and the nondeterministic interleavings of concurrent events can affect the behaviorof the program. One approach to systematically explore the nondeterminismcaused by input data is dynamic symbolic execution. For testing multithreaded programs we present a new approach that combines dynamic symbolic execution with unfoldings, a method originally developed for Petri nets butalso applied to many other models of concurrency. We provide an experimental comparison of our new approach with existing algorithms combining dynamic symbolic execution and partialorder reductions and show that the new algorithm can explore the reachable control states of each thread with a significantly smaller number of test runs. In some cases the reduction to the number of test runs can be even exponential allowing programs with longtest executions or hardtosolve constrains generated by symbolic execution to be tested more efficiently.
This is joint work with Kari Kaehkoenen and Olli Saarikivi
Location: LMU main building, A020
[+]
21.06.2013
10:00
DurandGasselin Antoine: From Monadic SecondOrder Definable StringTransformations to Transducers
Abstract:
Courcelle (1992) proposed the idea of using logic, in particular
Monadic secondorder logic (MSO), to define graph to graph
transformations. When restricting the input to a string, one can
devise executable machine models to define such
transformations. Engelfriet and Hoogeboom(2001) studied twoway
finite state stringtostring transducers and showed that their
expressiveness matches MSOdefinable transformations (MSOT).
Alur and ?ernÃ½ (2011) presented streaming transducers â??oneway
transducers equipped with multiple registers that can store output
stringsâ?? as an equiexpressive model. Natural generalizations of
streaming transducers to stringtotree (Alur and Dâ??Antoni, 2012) and
infinitestringtostring (Alur, Filiot, and Trivedi, 2012) cases
preserve MSOexpressiveness.
While earlier reductions from MSOT to streaming transducersused twoway
transducers as the intermediate model, I will revisit theearlier
reductions in a more general, and previously unexplored settingof
infinitestringtotree transformations, and provide a direct
reduction. Proof techniques used for this new reduction exploit the
conceptualtools (composition theorem and finite additive coloring
theorem) presented by Shelah (1975) in his alternative proof of Buechiâ??s
theorem. Usingsuch streaming stringtotree transducers yields
nontrivial decidabilityresults for instance the decidability of
functional equivalence for MSOdefinable infinitestringtotree
transformations.
(joint work with Rajeev Alur and Ashutosh Trivedi, to appear in LICS 2013)
Location: LMU main building, A020
[+] 31.05.2013 10:00 Seidl Helmut: How to Combine Widening and Narrowing for Nonmonotonic Systems of Equations.
Abstract:
Nontrivial analysis problems require complete lattices
with infinite ascending and descending chains. In order
to compute reasonably precise postfixpoints of the resulting
systems of equations, Cousot andCousot have suggested accelerated
fixpoint iteration by means of wideningand narrowing.
The strict separation into phases, however, may unnecessarily give up
precision that cannot be recovered later. While wideningis also applicable
if equations are nonmonotonic, this is no longer the case for narrowing.
A narrowing iteration to improve a given postfixpoint, additionally,
must assume that all righthand sides are monotonic.
The latter assumption, though, is not met in presence of widening.
It is also not met by equation systems corresponding to contextsensitive
interprocedural analysis, possibly combining contextsensitive analysisof
local information with flowinsensitive analysis of globals.
As a remedy, we present a novel operator that combines a given widening
operator with a given narrowing operator. We present adapted versions
of roundrobin as well as of worklist iteration, local, and
sideeffecting solving
algorithms for the combined operator and prove that the resulting
solvers always
return sound results and are guaranteed to terminate for monotonic systems
whenever only finitely many unknowns (constraint variables)are encountered.
Location: LMU main building, A020
[+] 24.05.2013 10:30 Bouajjani Ahmed: Verifying Concurrent Programs against Sequential Specifications.
Abstract:
We investigate the algorithmic feasibility of checking whetherconcurrent
implementations of sharedmemory objects adhere to their givensequential
specifications; sequential consistency, linearizability, and conflict
serializability are the canonical variations of this problem.While verifying
sequential consistency of systems with unbounded concurrency is known to be
undecidable, we demonstrate that conflict serializability, and linearizability
with fixed linearization points are EXPSPACEcomplete, while the general
linearizability problem is undecidable.
Our (un)decidability proofs, besides bestowing novel theoretical results,also
reveal novel program explorations strategies. For instance, we show that every
violation to conflict serializability is captured by a conflict cycle whose
length is bounded independently from the number of concurrent operations. This
suggests an incomplete detection algorithm which only remembers a small subset
of conflict edges, which can be made complete by increasing the number of
remembered edges to the cyclelength bound.Similarly, our undecidability proof
for linearizability suggests an incomplete detection algorithm which limits the
number of ``barriers'' bisecting nonoverlapping operations. Our decidability
proof of boundedbarrier linearizability is interesting on its own, as it
reduces the consideration of all possible operation serializations to numerical
constraint solving. The literature seems to confirm that most violations are
detectableby considering very few conflict edges or barriers.
(Joint work with Constantin Enea, Michael Emmi, and Jad Hamza. Published in ESOP'13.)
Location: LMU Main Building, A020
Links:
[+] 17.05.2013 10:00 Pérez Juan Navarro: Separation Logic Modulo Theories
Abstract: The aim of this talk is to describe a number of recent developments on the integration of Separation Logic, a prominent logic for statically reasoning about the memory usage of computer programs, and Satisfiability Modulo Theories (SMT). By leveraging on the power of SMT solvers, our reasoning tools are able to simultaneously handle supported theory assertions between data and pointer variablesincluding e.g. integer and real arithmetic, bitvectors and arraysand the shape of the data structures referenced by those pointers. The talk will include motivating examplesand encouraging experimental results obtained with Asterix, an implementation of our entailment checking algorithm that relies on Z3 as the theory reasoning backend. This is joint work with Andrey Rybalchenko.
Location: LMU main building, A020
[+] 03.05.2013 10:00 Cyriac Aiswarya: Model Checking Languages of Data Words
Abstract:
We consider the modelchecking problem for data multi pushdownautomata (DMPA). DMPA generate data words, i.e, strings enriched with values from an infinite domain. The latter can be used to represent an unbounded number of process identifiers so that DMPA are suitable to model concurrent programs with dynamic process creation. To specify properties of data words, we use monadic secondorder (MSO) logic, which comes with a predicate to test two word positions for data equality. While satisfiability for MSO logic is undecidable (even for weaker fragments such as firstorder logic), our main result states that one can decide if all words generated by a DMPA satisfy a given formula from the full MSO logic.
This isa joint work with Benedikt Bollig, Paul Gastin and K. Narayan Kumar.
Location: LMU main building, A020
[+]
26.04.2013
10:00
Esparza Javier: On Negotiation as Concurrency Primitive
Abstract: We introduce negotiations, a model of concurrency close to Pet
Location: LMU main building A020
Links:
[+]
19.04.2013
10:00
Esparza Javier: Parameterized Verification of Asynchronous SharedMemory Systems
Abstract: We characterize the complexity of the safety verification problem forparameterized systems consisting of a leader process and arbitrarilymanyanonymous and identical contributors. Processes communicate through ashared, boundedvalue register. While each operation on the registeris atomic, there is no synchronization primitive to execute a sequenceof operations atomically. The model is inspired by distributedalgorithms implemented on sensor networks.We analyze the complexity of the safety verificationproblem whenprocesses are modeled by finitestate machines, pushdown machines, andTuring machines. Our proofs use combinatorial characterizationsofcomputations in the model, and in case of pushdownsystems, some novellanguagetheoretic constructions of independent interest.
Location: LMU A020
DateTimeTitle
[+]
28.03.2013
10:00
Marian Dan Andrei: Predicate Abstraction for Relaxed Memory Models
Abstract: We present a novel approach for predicate abstraction of programs running on relaxed memory models. Our approach consists of two steps. First, we reduce the problem of verifying a program P running on a memorymodel M to the problem of verifying a program PM that captures an abstraction of M as part of the program. Second, we show how to discover new predicates that enable verification of PM . The core idea is to extrapolate from the predicates used to verify P under sequential consistency. A key new
Location: Garching, MI.02.07.014
[+] 27.03.2013 15:00 Genaim Samir: On the Linear Ranking Problem for Integer LinearConstraint Loops
Abstract:
We study the complexity of the Linear Ranking problem: given aloop,
described by linear constraints over a finite set of integer
variables, is there a linear ranking function for this loop? While
existenceof such a function implies termination, this problem is not
equivalentto termination. When the variables range over the rationals
or reals, the Linear Ranking problem is known to be PTIME decidable.
However, when they range over the integers, whether for singlepath or
multipath loops, the complexity of the Linear Ranking problem has not
yet been determined. We show that it is coNPcomplete. However, we
point out some specialcases of importance of PTIME complexity. We
also present complete algorithms for synthesizing linear ranking
functions, both for the general case and the special PTIME cases.
(joint work with Amir M. BenAmram)
Location: Garching MI 02.07.014
[+] 13.03.2013 14:00 Terauchi Tachio: A Templatebased Approach to Complete Predicate Refinement
Abstract:
Predicate abstraction has proven successful for the verification of
software programs, especially when it is combined with a
counterexampleguided predicate refinement (i.e., predicate inference)
method. However, except for a few restricted firstorder theories,
the current predicate refinement methods are incomplete in that
the counterexampleguided abstractandrefine loop may fail to
converge even when an abstraction that is sufficient for verifying the
program exists in the theory. Predicate refinement is said to be
complete when it is guaranteed to eventually discover a sufficient
abstraction, when one exists in the underlyingfirstorder theory.
This talk presents a predicate refinement approachthat is
complete for the quantifierfree theory of linear real arithmetic
with uninterpreted functions and arrays, extending the previous
stateof the art on complete predicate refinement which was only
complete formore limited theories. Our approach is
templatebased, inspired by thework on templatebased (or,
``constraintbased'') program verification.To make the approach
scale, we make an important observation that the firstorder
logic constraints that are solved to infer the predicates are
always repetitions of certain patterns (they are generated from a
set of``Hornclause like'' rules), so as to limit the expensive
templatebased inference to a small number predicate variables in
the constraints.
This is a joint work with Hiroshi Unno and Naoki Kobayashi.
Location: Garching MI 02.07.014
[+] 01.03.2013 10:00 Albarghouthi Was: From SMT Solvers to Interpolators to Verifiers
Abstract:
SMT solvers have become the standard tools underlying many
symbolic execution engines and bounded model checkers. Whereas these
techniques do not give guarantees on absence of errors, it has been
shown thatCraig interpolants mined from unsatisfiability proofs can
be used as guesses for inductive invariants (correctness proofs). In
this talk, I willdescribe our interpolationbased verification
techniques, and how combining interpolation with abstract
interpretation can be quite advantageous.I will also describe our
experience implementing these techniques in theUFO framework, an
opensource C verification framework we built in theLLVM compiler
infrastructure. This is joint work with Arie Gurfinkel (SEI, CMU) and
Marsha Chechik (Univ. of Toronto).
Location: Garching MI 02.07.014
[+] 08.02.2013 10:00 Terepeta Michal Tomasz: Recursive Advice for Coordination
Abstract:
Aspectoriented programming is a programming paradigm that is often praised for the ability to create modular software and separate crosscutting concerns. Recently aspects have been also considered in thecontext of coordination languages, offering similar advantages. However, introducing aspects makes analyzing such languages more difficult due to the fact that aspects can be recursive â?? advice from an aspect must itself beanalyzed by aspects â?? as well as being simultaneously applicable in concurrent threads. Therefore the problem of reachability of various states ofa system becomes much more challenging. This is important since ensuringthat a system does not contain errors is often equivalent to proving thatsome states are not reachable.
In this paper we show how to solve these challenges by applying a successful technique from the area of software model checking, namely communicating pushdown systems. Even though primarilyused for analysis of recursive programs, we are able to adapt them to fit this new context.
Location: Garching MI 02.07.014
01.02.2013 10:00 VogelHeuser Birgit: Requirements for modeling and estimating runtime behavior in automation
Abstract:
Location: Garching, MI 02.07.014
Links:
[+] 18.01.2013 10:00 Hofmann Martin: TypeBased Enforcement of Secure Programming Guidelines Code Injection Prevention at SAP
Abstract:
Code injection and crosssite scripting belong to the most common security vulnerabilities in modern software, usually caused by incorrect string processing. These exploits are often addressed by formu latingprogramming guidelines or â??best practicesâ?.
In this paper, we studythe concrete example of a guideline used at SAP for the handling of untrusted, potentially executable strings that are embedded in the output of aJava servlet. To verify adherence to the guideline, we present a type system for a Javalike language that is extended with refined string types,output effects, and polymorphic method types.
The practical suitabilityof the system is demonstrated by an imple mentation of a corresponding string type verifier and contextsensitive inference for real Java programs.
Location: Garching MI 02.07.014
Links:
[+]
11.01.2013
10:00
Zimmerman Martin: CostParity Games and CostStreett Games
Abstract:
We consider twoplayer games played on finite graphs with costson edges
and introduce two wining conditions, costparity and costStreett, which
require bounds on the costs between requests and their responses.
For costparity games we show that the first player has positionalwinning
strategies and that determining the winner lies in NP intersection coNP.
For costStreet games we show that the first player has finitestate
winning strategies and that determining the winner is EXPTIMEcomplete.
Location: Garching MI 02.07.014
Links:
[+] 14.12.2012 10:00 Kiefer Stefan: On the equivalence problem for probabilistic automata
Abstract:
Deciding equivalence of probabilistic automata is a key problemfor
establishing various behavioural and anonymity properties of probabilistic
systems. In particular, it is at the heart of the tool APEX, ananalyser
for probabilistic programs. APEX is based on game semantics andanalyses a
broad range of anonymity and termination properties of randomised
protocols and other open programs.
In recent experiments a randomised equivalence test based on polynomial
identity testing outperformed deterministic algorithms. We show that
polynomial identity testing yields efficient algorithms for various
generalisations of the equivalence problem. First, we provide a randomized
NC procedure that also outputs a counterexample trace in case of
inequivalence. Second, we consider equivalence of probabilistic cost
automata. In these automata transitions are labelled with integer costs
and each word is associated with a distribution oncosts, corresponding to
the cumulative costs of the accepting runs on that word. Two automata are
equivalent if they induce the same cost distributions on each input word.
We show that equivalence can be checked in randomised polynomial time.
Finally we show that the equivalence problem for probabilistic visibly
pushdown automata is logspace equivalent to the problem of whether a
polynomial represented by an arithmetic circuit is identically zero.
Location: Garching, MI 02.07.014
Links:
[+]
12.12.2012
10:30
Brazil Tomas: Efficient Controller Synthesis for Consumption Gameswith Multiple
Resource Types
Abstract:
We introduce consumption games, a model for discrete interactive system with
multiple resources that are consumed or reloaded independently. More
precisely,
a consumption game is a finitestate graph whereeach transition is
labeled by a
vector of resource updates, where everyupdate is a nonpositive number or
omega. The omega updates model the reloading of a given resource. Each
vertex
belongs either to player Box orplayer Diamond, where the aim of player
Box is
to play so that the resources are never exhausted. We consider several
natural
algorithmic problems about consumption games, and show that although these
problems arecomputationally hard in general, they are solvable in
polynomial
time for every fixed number of resource types (i.e., the dimension of
the update
vectors) and bounded resource updates.
This is a joint work with Krishnendu Chatterjee, Antonin Kucera and
Petr Novotny.
Location: Garching MI 02.07.014
Links:
[+] 30.11.2012 11:00 Krcal Jan: Fixeddelay Events in Generalized SemiMarkov ProcessesRevisited
Abstract:
In the area of probabilistic verification and performance evaluation, the behavior of
reallife systems such as queues, assembly linesor communication protocols are
analyzed using formal mathematical models, such as Generalized SemiMarkov
Processes (GSMP). We consider a previously studied class of GSMP extended
with events that occur after a fixeddelay. Disproving several previous results, we
show that such GSMP can exhibit a surprisingly unstable behavior in the longrun.
The instabilityis caused by properties of the model not found in reallife. To avoid
this undesirable situation, we also provide syntactical conditions upon which a GSMP
model has always a stable behavior.
Location: Garching, MI 02.07.014
Links:
[+] 30.11.2012 10:00 Tribastone Mirco: Continuous limits for massivescale stochastic models of computing systems
Abstract:
Fluid (or meanfield) techniques, rooted in statistical mechanics and physical chemistry, provide accurate deterministic approximationsto massivescale Markov chain models of interacting agents. The originaldiscretestate model is properly scaled in such a way that it converges tothe solution of a compact system of differential equations (ODEs) whose size is independent from the population of agents.
In this seminar I will overview recent results which relate the fluid approach and informaticswithin the context of a stochastic process algebra, as a means to dealingwith the infamous stateexplosion problem of Markovian models of computing systems.
Then, I will introduce the concept of 'continuousstate explosion', which is exhibited by certain models that describe 'systems of systems', for instance when a model comprises a large number of compositeprocesses and each consists of smaller processes which are themselves massively replicated. In such conditions, even fluid techniques are not scalable because the ODE system size grows polynomially with the population ofcomposite processes. Motivated by the fact that such a scenario is of practical relevance (e.g., server farms and biological systems), I will discuss a novel notion of behavioural equivalence for ODEs that induces an exact form of aggregation, leading to a reduced ODE system which is completely independent from all replicas.
If time permits, I will then discussongoing work which is pushing the limits of differential aggregations. Iwill introduce a stochastic model that captures processes evolving spatially over a discrete lattice. Whilst the analysis of such a model is computationally infeasible even for coarse lattices, I will present a form of aggregation that scales very well with the lattice size, by capturing the inherently discrete movement in a continuous fashion via partial differential equations of reactiondiffusion type.
Location: Garching, MI 02.07.014.
Links:
23.11.2012 10:00 Hofmann Martin: Tutorial on type and effect systems
Abstract:
Location: Garching, MI 02.07.014
Links:
09.11.2012 10:00 Martin Hofmann: Tutorial on type and effect systems
Abstract:
Location: Garching, MI 02.07.014.
Links:
26.10.2012 08:30 Hofmann Martin: Tutorial on type and effect systems
Abstract:
Location: Garching, MI 02.07.014.
Links:
DateTimeTitle
[+]
01.08.2012
14:30
Giro Sergio: Verification of distributed probabilistic systems under partial information
Abstract:
Abstract:
In the verification of systems that involve probabilities, it is
crucial to study qualitative properties concerning the probability of
certain events as, for instance, the probability that a failure
occurs is less that 0.01. In case the system under consideration is
distributed, each of the components of the system might have a partial
view of the information available to other components. The analysis of
these systems is carried out by considering distributed adversaries
withrestricted observations. In this talk I will summarise six years
of research on automatic verification of distributed probabilistic
systems. On the negative side, we proved the verification problem to
be undecidable ingeneral and NPcomplete for some restricted systems.
Nevertheless, we also introduced some techniques for overestimation of
worstcase probabilities, and showed that the concept of distributed
adversaries can be usedto improve existing techniques such as partial
order reduction.
Location: TUM Garching  Room 00.09.055
Links:
[+] 27.06.2012 16:00 Koen Claessen: Automated firstorder reasoning for Haskell programverification
Abstract:
We have recently developed various techniques for reasoning about
Haskell programs which are all based on a translation from Haskell
programs to firstorder logic and then using automated firstorder
tools toreason about these. In this way, we have built a contract
checker for Haskell programs, an automated induction tool for Haskell
programs, andan automated counter example finder for Haskell
programs. I will discusssuccesses and challenges; all this is ongoing
work.
This is joint wor
Location: TUM Garching  Room 00.09.055
Links:
[+] 15.06.2012 08:30 Philipp Hoffmann: Strategy Iteration on the Graphics Card
Abstract:
Compared to standard CPUs, graphic processing units (GPUs) offer much
higher raw computational power at a lower price and energy
consumption. But in order to take full advantage of the GPU, the
computational problem has to be suited for parallelization using
vector operations which makes GPUs particularly wellsuited for
problems relying largely on linear algebra. Generalpurpose computing
on the GPU is therefore widely used today in computational sciences
e.g. for simulation of physical systems.
In this bachelor thesis the use of the GPU for solving fixedpoint
Location: Amalienstr. 73, Room 101
Links:
[+] 13.06.2012 14:00 Rafal Kolanski: Mechanised Separation Algebra for Isabelle/HOL
Abstract:
I will be presenting our work on a Isabelle/HOL library with ageneric type class implementation of separation algebra based on the formulation by Calcagno et al. Our library features the basic separation logicconcepts developed on top of the separation algebra, and contains automated tactic support that can be used directly for any instantiation of the library.
Location: TUM Garching  Room 00.09.055
Links:
[+] 25.05.2012 08:30 Kramer Simon: A Logic of Interactive Proofs (Formal Theory of Knowledge Transfer)
Abstract: We propose a logic of interactive proofs as the first and mainstep towards an intuitionistic foundation for interactive computation to be obtained via an interactive analog of the G\odelKolmogorovArt\\emovdefinition of intuitionistic logic as embedded into a classical modal logic of proofs, and of the CurryHoward isomorphism between intuitionisticproofs and typed programs. Our interactive proofs effectuate a persistentepistemic impact in their intended communities of peer reviewers that consists in the induction of the (propositional) knowledge of their proof goalby means of the (individual) knowledge of the proof with the interpretingreviewer. That is, interactive proofs effectuate a transfer of propositional knowledge (knowable facts) via the transfer of certain individual knowledge (knowable proofs) in distributed and multiagent systems. In otherwords, we as a community can have the formal common knowledge that a proof is that which if known to one of our peer members would induce the knowledge of its proof goal with that member.
Location: tba.
Links:
DateTimeTitle
[+] 24.02.2012 10:00 Traytel Dmitriy: Extending HindleyMilner Type Inference with Coercive Structural Subtyping
Abstract:
Coercions allow to convert between different types, and theirautomatic
insertion can greatly increase readability of terms. We present
a type inference algorithm that, given a term without type information,
computes a type assignment and determines at which positions in the
term coercions have to be inserted to make it typecorrect according to
thestandard HindleyMilner system (without any subtypes). The algo
rithm is sound and, if the subtype relation on base types is a disjoint
union of lattices, also complete. The algorithm is used in the proof
assistantIsabelle.
Location: TUM Garching  Room 02.07.014
Links:
[+] 17.02.2012 10:00 Hoefner Peter: Formal Methods for Wireless Mesh Networks
Abstract:
Wireless Mesh Networks (WMNs) have recently gained considerable
popularity and are increasingly deployed in a wide range of application
scenarios, including emergency response communication, intelligent
transportation systems, mining, video surveillance, etc. WMNs are
essentially selforganising wireless adhoc networks that can provide
broadbandcommunication without relying on a wired backhaul
infrastructure. This has the benefit of rapid and lowcost network
deployment. Traditionally,the main tools for evaluating and validating
network protocol are simulation and testbed experiments. The key
limitations of these approaches are that they are very expensive, time
consuming and nonexhaustive. As aresult, protocol errors and
limitations are still found many years afterthe definition and
standardisation.
Formal methods have a great potential in helping to address this
problem, and can provide valuable tools for the design, evaluation and
verification of WMN routing protocols. Theoverall goal is to reduce the
``timetomarket'' for better (new or modified) WMN protocols, and to
increase the reliability and performance of the corresponding networks.
In this talk I describe the importance of WM
Location: TUM Garching  Room 01.11.018
Links:
[+] 16.02.2012 17:00 Broadbent Christian: Approaches to ModelChecking HigherOrder Recu
Abstract:
Higherorder recursion schemes (HORS) can be viewed as simply typed terms in
the lambdacalculus with recursion and thereby provide a useful model for the
behaviour of higherorder functional programs. SinceOng's original proof
[LICS 2006] that the mucalculus modelchecking is decidable on structures
generated by HORS, a number of alternative algorithms have been developed. In
particular variants of Kobayashi's algorithm based on intersection types [POPL
2009] have been implemented andshow promise as being usable in practise.
Another way of looking at theproblem is to consider a different but equivalent
model to HORSnamely `collapsible pushdown automata' (CPDA) [Hague et al.
LICS 2008]. A CPDA has a memory consisting of a `pushdown of pushdowns.... of
pushdown stacks' together with additional structure in the form of `links'.
One candefine a natural class of automata recognising sets of CPDA
configurations that provide a way to represent a solution to the global mu
calculusmodelchecking problem for CPDA (and hence HORS) [B. et al. LICS
2010].
In this talk we will introduce HORS and CPDA together with a brief overview of
the techniques mentioned above. Our main focus will, however, be on CPDA; in
particular we will outline some very recent work in progress [joint with
Arnaud Carayol, Matthew Hague, Olivier Serre] to develop a saturation
algorithm for CPDA, which we eventually hope to implement to provide a point
of comparison with the intersection type algorithms that work directly on
HORS. We will conclude by highlighting some possible deep connections between
the intersection type and CPDA approaches, which suggest that further down the
line the two techniques may beable to inform each other.
Location: TUM Garching  Room 03.09.014
Links:
[+] 10.02.2012 08:30 Rossberg Andreas: Nonparametric Parametricity
Abstract:
Type abstraction and intensional type analysis are features seemingly at
odds  type abstraction is intended to guarantee parametricityand
representation independence, while type analysis is inherently
nonparametric. A way to reconcile these features is to generate a fresh
type name at run time when one defines an abstract type. That type
name maysafely be used as a dynamic representative of the abstract type for
purposes of type analysis.
But does dynamic type generation provide us withthe same kinds of
abstraction guarantees that we get from parametric polymorphism? To give an
answer to that question, we definene a stepindexedKripke logical
relation for a language with both nonparametric polymorphism (in the form
of typesafe cast) and dynamic type generation. Our logical relation enables
us to establish parametricity and representation independence results, even
in a nonparametric setting, by attaching arbitrary relational
interpretations to dynamicallygenerated type names.
In addition, we explore how programs that are provably equivalent in a more
traditional parametric logical relation may be wrapped;
systematically to produce terms that are related by our nonparametric
relation, andvice versa. This leads us to develop a polarized;
variant of our logical relation, which enables us to distinguish formally
between positive and negative notions of parametricity.
Location: TUM Garching  Room 02.07.014
Links:
[+] 06.02.2012 16:15 Moser Georg: Predicative Recursion and Register Machines
Abstract:
In this talk I will propose a termination order, dedicated for
complexity analysis, the small polynomial path order (sPOP* for short).
This order provides a new characterisation of the class of polytime
computable function via term rewrite systems. Based on sPOP*, we'll
study a class of rewrite systems, dubbed systems of predicative
recursionof degree d, such that for rewrite systems in this class we
obtain thatthe runtime complexity lies in O(n^d). We show that
predicative recursive rewrite systems of degree d define functions
computable on a registermachine in time O(n^d). This result emphasises
the fact that (innermost) runtime complexity of a rewrite system is an
invariant cost model.
Location: Oettingerstr., L109
Links:
[+] 03.02.2012 08:30 Zeller Andreas: Experimental Program Analysis, and how to get an ERC grant
Abstract:
In the past decade, static validation of software systems hasmade spectacular
progresses. However, these techniques face enormous issues with the advent of
multisite, multilanguage, multivendor programs such as Web applications,
which come with no specifications to rely on. In this talk, I present an
experimental approach to software analysis, where we generate executions to
systematically explore the space of software behavior ? and we use the outcome
of these executions to guide the search even further. In contrast to static
techniques, experimental techniques are applicable to arbitrary executable
programs; in contrast to dynamic techniques, they are not limited to just the
observed runs. Eventually, experimental techniques will provide precise
specifications to allow for largescale formal verification.
Andreas Zeller is a full professor for Software Engineering at Saarland
University in Saarbruecken, Germany. His research concerns the analysis of large
software systems and their development process; his students are funded by
companies likeGoogle, Microsoft, or SAP. In 2010, Zeller was inducted as
Fellow of the ACM for his contributions to automated debugging and mining
software archives. In 2011, he received an ERC Advanced Grant for work on
specification mining and test case generation ? the topics of the above talk.
Location: TUM Garching  Room 02.07.014
Links:
[+] 27.01.2012 08:30 Klaedtke Felix: Policy Monitoring with Firstorder Temporal Logic
Abstract:
In security and compliance, it is often necessary to ensure that
agents and systems comply to complex policies. An example of such a
policy from financial reporting is the requirement that every
transactionof a customer c, who has within the last 30 days been
involved in a suspicious transaction, must be reported as suspicious
within 2 days. In this talk, I will give an overview of our approach
to automated compliance checking. In particular, I will present our
monitoring algorithm forchecking properties specified in a fragment
of metric firstorder temporal logic. I will also report on case
studies, conducted together with Nokia, in security and compliance
monitoring and use these to evaluate both the suitability of this
fragment for expressing complex, realistic policies and the efficiency
of our tool MONPOLY, which implements our monitoring algorithm.
Joint work with David Basin, Matus Harvan, Samuel Mueller, and
Eugen Zalinescu.
Location: TUM Garching  Room 02.07.014
Links:
[+] 25.01.2012 17:00 Maneth Sebastian: Fast InMemory XPath Search using Compressed Indexes
Abstract:
A large fraction of an XML document typically
consists of textdata. The XPath query language allows to
search such text via its equal, contains, and startswith predicates
These predicates can be efficiently implemented using
a compressed selfindex of the document's text data.
Location: TUM Garching  Room 02.07.014
Links:
[+] 20.01.2012 08:30 Katoen JoostPieter: Formal Verification and Performability Analysi
Abstract:
The engineering process of onboard critical embedded systems involves a wide range of diverse approaches and techniques for systemlevelaspects such as functional correctness, dependability and safety, as well as
performance. Establishing these properties in a trustworthy manner is a highly challenging task. This is severely complicated by the heterogeneous character of onboard systems involving software, sensors, actuators, electrical components, etc., that each has its own specific development approach supported by different modeling and analysis techniques.
In this talk, we will report on a serious attempt to develop an integrated approach for all aforementioned aspects. The key is a generalpurposemodeling and specification formalism based on AADL, enriched with a
rich palette of formal analysis techniques for all properties and measures ofinterest. It is supported by an advanced toolset which is centered around stateoftheart symbolic and stochastic model checking. We present ourAADL dialect, its formal semantics, its main analysis features, and the extensive evaluation of our approach in an industrial context.
(The work has been conducted in the context of several projects that are fundedby the European Space Agency.)
Location: TUM Garching  Room 02.07.014
Links:
[+] 19.01.2012 08:30 Barth Stephan: SATbased minimization for nondeterministic Buechi automata
Abstract:
Buechi Automata are an automaton model for describing infinitelanguages.
Despite its similarities to finite automata determinisation isnot
always possible in this model and no canonical minimization algorithm
exists.
This work describes SATbased minimization procedure for nondeterministic Buechi automata (NBA).
For a given NBA A the procedure finds an equivalent NBA A_min
with the minimal number of states. This is done by successively
computing automata A' that approximate A in the sensethat they
accept a given finite set of positive examples and reject a given
finite set of negative examples. In the course of the procedure these
example sets are successively increased. Thus, our method can be seen
as an instance of a generic learning algorithm based on a
minimally adequate teacher in the sense of Angluin.
We use a SAT solver to find NBA forgiven sets of positive and
negative examples. We use Ramseybased complementation to check
candidates computed in this manner for equivalence with A. Failure
of equivalence yields new positive or negative examples. Our method
proved successful on a series of small examples that are nontrivial in
the sense that they are difficult or impossible to minimize by
hand. In particular, we succeed in minimizing all NBA with two states
andtwoletter alphabet as well as some instances of Michel's NBA
which wereintroduced to establish an n!
lower bound on complementation of NBA.
Location: LMU, Oettingenstr 67, L109
Links:
[+] 13.01.2012 08:30 Senjak ChristophSimon: Minimal from Classical Proofs
Abstract:
While minimal and intuitionistic derivability implies classical
derivability, the converse only holds for special cases. One such case
is Barr's theorem, which states that this converse holds for geometric
implications derivable from geometric theories, another is the full
classification by means of positiveness of connectives, given by
Orevkov (1968) and Nadathur (2000). We have a look at the runtime of
the algorithmsthat the proofs of these theorems yield. For one of
Glivenko's classes ofsuch sequents, we can give an algorithm of
quadratic runtime, providedit is in long normal form and given in a
slightly weaker version of classical logic. This is of interest for
computational uses of classical proofs.
Location: TUM Garching  Room 02.07.014
Links:
[+] 09.12.2011 08:30 Mihaila Bogdan: Static Analysis of Binaries for Reverse Engineering
Abstract:
The security of commercial software is determined by manually
inspecting the machine code of the software. Finding a security vulnerability
equates to singling out a fragment containing a handful of instructions out of
millions and has been likened to finding the needle in the haystack. Our
project will equip the security engineer with tools toautomatically identify
code as free from vulnerabilities and to addressthe construction of attacks
for dubious code fragments.
In order to make our tools scale, we introduce a method to focus a
forward static analysis on relevant parts of the program. This method is based
on recording a trace up to an interesting function f of the program under test
andthen rerunning this trace in the static analyser. The benefit is that f
can be analysed with a small abstract context that is easier to comprehend
than the actual program state and that is realistic in that it includes at
least one actual trace of the program.
Location: TUM Garching  Room 02.07.014
Links:
[+] 02.12.2011 08:30 Vytiniotis Dimitrios: Stop when you are AlmostFull Adventures in constructive termination
Abstract: Disjunctive wellfoundedness (used in Terminator), sizechangetermination, and wellquasiorders (used in supercompilation and termrewrite systems) are examples of techniques that have been successfully applied to automatic proofs of program termination and online termination testing, respectively. Although these works originate in different communities, there is an intimate connection between them ? they rely on closely related principles and both employ similar arguments from Ramsey theory. Atthe same time there is a notable absence of these techniques in programming sys tems based on constructive type theory. In this paper we?d like tohighlight the aforementioned connection and make the core ideas widely accessible to theoreticians and Coq programmers, by offer ing a Coq development which culminates in some novel tools for performing induction. The benefit is nice composability properties of termination arguments at the cost of intuitive and lightweight user obligations. Inevitably, we have to p
Location: TUM Garching  Room 02.07.014
Links:
[+] 18.11.2011 08:30 Schwoon Stefan: Efficient contextual unfolding
Abstract:
A contextual net is a Petri net extended with read arcs, which
allow transitions to check for tokens without consuming them.
Contextual nets allow for better modelling of concurrent read
access than Petri nets, and their unfoldings can be
exponentially more compact than those ofa corresponding Petri
net. A constructive but abstract procedure for generating those
unfoldings was proposed in earlier work; however, no concrete
implementation existed. Here, we close this gap providing two
concrete methods for computing contextual unfoldings, with
a view to efficiency. We report on experiments carried out on
a number of benchmarks. These show that not only are
contextual unfoldings more compact than Petri net unfoldings,
but they can be computed with the same or better efficiency, in
particular with respect to the placereplication encoding of
contextual nets into Petri nets.
Location: TUM Garching  Room 02.07.014
Links:
[+] 28.10.2011 08:30 Li Xin: Precision & Scalability of Stackingbased Java Program Analysis
Abstract:
Pushdown systems (PDSs) are known to be natural models of programs with
recursive procedures. However, it pose new challenges to precisely and
efficiently analyze largescale programs with objectoriented features by PDSs.
In this talk, I will introduce our efforts and preliminary results on designing
precise yet scalable stackingbased program analysis for Java, mainly including
conditional weighted PDSs that enhance theexpressiveness of weighted PDSs and
yield more precise Java program analysis, and a modular model checking
algorithm on weighted PDSs, to reduce both time and memory cost of Java
pointsto analysis in practice.
Location: TUM Garching  Room 02.07.014
Links:
[+] 21.10.2011 08:30 Fisher Jasmin: Model Checking Cell Fate Decisions
Abstract: As time goes by, it becomes more and more apparent that the puzzles of life involve more and more molecular pieces that fit together inincreasingly complex ways. Biology is not an exact science. It is messy and noisy, and most often vague and ambiguous. We cannot assign clear rulesto the way cells behave and interact with one another. And we often cannot quantify the exact amounts of molecules, such as genes and proteins, in the resolution of a single cell. To make matters worse (so to speak), the combinatorial complexity observed in biological networks is staggering, which renders the comprehension and analysis of such systems a major challenge. Recent efforts to create executable models of complex biological phenomena  an approach called Executable Biology  entail great promise for new scientific discoveries, shading new light on the puzzle of life. Atthe same time, this 'new wave of the future' forces computer science tostretch far and beyond, and in ways never considered before, in order todeal with the enormous complexity observed in biology. In this talk, I will summarize some of the success stories in using formal verification toreason about mechanistic models in biology. In particular, I will focus on models of cell fate decisions during development and cancer, and their
Location: TUM Garching  Room 02.07.014
Links:
[+] 14.10.2011 15:00 Hoffmann Jan: Types with Potential: Polynomial Resource Bounds viaAutomatic Amortized Analysis
Abstract:
A primary feature of a computer program is its quantitative
pe
Location: Room 151 (Oettingenstr. 67)
Links:
[+] 13.10.2011 14:00 LedesmaGarza Ruslan: Simplification of Horn clauses over unknown predicates
Abstract:
The temporal verification of functional programs can be reduced
to constraint solving. The combination of our work on instrumenting
functional programs and the Liquid Types inference system is a
technique for the verification of temporal properties of higherorder
programs. Theefficient solving of the subtyping constraints
generated during type inference is an important problem. There are
common program features that originate subtyping constraints with
redundant information. In this talk wepresent a simplification rule
over sets of subtyping constraints. Subtyping constraints are
interpreted as Horn clauses over unknown predicates. We state our
rule as a simplification rule over sets of Horn clauses thatpreserves
satisfiability.
Location: Fakultaet fuer Informatik Garching, room 03.09.014
Links:
DateTimeTitle
[+] 26.09.2011 14:00 Ka I Pun Violet: Polymorphic behavioural lock effects for deadlockchecking
Abstract:
Deadlocks are a common problem for concurrent programs, in particular where
multiple threads are accessing shared mutually exclusive resources synchronized
by locks. We use a behavioural type and effect system to statically determine
potential interaction of each thread with locks. Based on that threadlocal
lock interaction, we explore the state space on the global level to detect
potential deadlocks. In the presence of recursion, we use two sound
abstractions to keep the state space finite, namely restricting the upper bound
of reentrant lock counters, andabstracting the behavioural effect into a
coarser, tail recursive description.
Location: TUM Garching  Room 03.09.014
Links:
[+] 19.08.2011 08:30 Talcott Carolyn: Pathway Logic: A Symbolic Systems Biology Framework for Modeling Biological Processes
Abstract:
Symbolic systems biology (SSB) is an approach to computationalmodeling of biological
systems that builds on logical representations anduses the symbolic reasoning tools
developed for analysis of complex hardware and software systems. Pathway Logic is an
approach to SSB based on Rewriting Logic, a simple formalism for describing concurrent
processes,such as cellular signaling. Process steps/reactions and related information
are collected as a network of in a knowledge base. Subnets and pathways are assembled
as answers to queries (specifying desired outcomes or situations to avoid) rather than
being predefined. The Pathway Logic Assistant provides a graphical interface for
browsing and analyzing such networks.
In this talk we will explain the basics of Pathway Logic and give an overview of our
curated knowledge base of mamalian signaling reactions, including response to Egf, Il1,
Tnfalpha. Then we will illustrate the use of the Pathway Logic Assistant to browse the
reaction network, andfind and compare pathways satisfying different constraints.
Location: TUM Garching  Room 03.09.014
Links:
[+] 29.07.2011 10:30 Malkis Alexander: A generic privacy policy language
Abstract:
We present a declarative language with a formal semantics for specifying both
users' privacy preferences and services' privacy policies.Expressiveness and
applicability are maximized by keeping the vocabularyand semantics of service
behaviours abstract. A privacycompliant datahandling protocol for a network
of communicating principals is described.
Location: TUM Garching  Room 03.09.014
Links:
[+] 15.07.2011 08:30 Klein Gerwin: Towards formally verifying security properties of microkernelbased systems
Abstract:
This talk presents our current work on the verification of security
and safety properties on the codelevel of embedded systems measuring
on the order of a million lines of code ore more. The key idea is to
use the formally correct seL4 microkernel for reducing and analysing
the trusted computing base of such system. I will give an overview of
the current status of this work, including an abstract security
analysis for acasestudy system, and the proof that seL4 enforces the
highlevel security property 'integrity' down to the C code
implementation. I will sketch how this property helps us in
reasoning about the behaviour of untrusted legacy system components.
Location: LMU Main Building  A U117
Links:
[+] 08.07.2011 10:00 Cook Byron: A new approach to temporal property verification
Abstract: In recent work we have found new approaches to the old problemof automatic temporal property verification. As well as leading to dramatic performance improvements, this work also helps to clarify some ageold questions about the connections between seemingly disparate historic approaches.
Location: LMU, Schellingstr. 5  Room 204
Links:
[+] 17.06.2011 08:30 Patrick Regan: Engaging the World Beyond Your Field: communicatingwith the media, the public, and other nonexpert stakeholders.
Abstract: tba.
Location: LMU Main Building  A U117
Links:
[+] 14.06.2011 14:00 King Andy: Existential Quantification as Incremental SAT
Abstract:
I shall present an algorithm for existential quantifier elimination using incremental SAT solving. This approach contrasts with existingtechniques in that it is based solely on manipulating the SAT instance rather than requiring any reengineering of the SAT solver or needing an auxiliary datastructure such as a BDD. The algorithm combines model enumeration with the generation of shortest prime implicants so as to converge ontoa quantifierfree formula presented in CNF.
This is joint work with Joerg Brauer and Jael Kriener.
Location: TUM Garching, Room 02.07.034
Links:
[+] 10.06.2011 08:30 Meyer Roland: Deciding robustness against total store ordering
Abstract:
joint work with Ahmed Bouajjani (LIAFA) and Eike Moehlmann (University of
Oldenburg)
Sequential consistency (SC) is the classical model for shared memory
concurrent programs. It corresponds to the interleaving semantics where the
order of actions issued by a component is preserved. For performance reasons,
modern processors adopt relaxed memory models that may execute actions out of
order. We address the problem of deciding robustness of a program against the
total store ordering (TSO) memory model, i.e., we check whether the behaviour
under TSO coincides with the expected SC semantics. We prove that this problem
is PSPACEcomplete. The key insight is that violations to robustness can be
detected on pairs of SC computations.
Location: LMU Main Building  A U117
Links:
[+] 03.06.2011 08:30 Jacobs Bart: VeriFast: a Powerful, Sound, Predictable, Fast Verifier for C and Java
Abstract:
VeriFast is a verifier for singlethreaded and multithreaded Cand Java programs annotated with preconditions and postconditions writtenin separation logic. To enable rich specifications, the programmer may define inductive datatypes, primitive recursive pure functions over these datatypes, and abstract separation logic predicates. To enable verification of these rich specifications, the programmer may write lemma functions, i.e., functions that serve only as proofs that their precondition implies their postcondition. The verifier checks that lemma functions terminateand do not have sideeffects. Verification proceeds by symbolic execution, where the heap is represented as a separation logic formula. Since neither VeriFast itself nor the underlying SMT solver do any significant search, verification time is predictable and low. We are currently using VeriFast to verify finegrained concurrent data structures, unloadable kernelmodules, and JavaCard programs.
Location: LMU Main Building  A U117
Links:
[+] 20.05.2011 08:30 Kuncar Ondrej: Proving Valid Quanti?ed Boolean Formulas in HOL Light
Abstract:
I am going to describe the integration of Squolem, Quanti?ed
Boolean Formula (QBF) solver, with the interactive theorem prover HOL
Light in my talk. Squolem generates certi?cates of validity, which are
based on Skolem functions as witnesses. The certi?cates are checked in
HOL Light by constructing proofs based on these certi?cates. The
presented approach allows HOL Light users to prove larger valid QBF
problems than before and provides correctness checking of Squolem?s
outputs based on the LCF approach. An error in Squolem was discovered
thanks to the integration.Experiments show that the feasibility of the
integration is very sensitive to implementation of HOL Light and used
inferences. This resulted in improvements in HOL Light?s inference kernel.
Location: LMU Main Building  A U117
Links:
[+]
13.05.2011
08:30
Maffei
Matteo: Formal Methods for the Design and Verification ofCryptographic
Applications
Abstract:
Designing security protocols is notoriously errorprone and
security proofs of such protocols are awkward for
humans. Several techniques based on formal methods were recently
proposed to automate protocol analysis. Despite these promising
results, the design and verification of modern cryptographic
applications is still an open issue. First, the design of
cryptographic protocols is driven by best practices and human
expertise and there exist virtually no techniques to automate this
task. Second, modern protocols rely on complex cryptographic
primitives and achieve sophisticated security properties that are
mostly not supported by existing verification tools. Finally, current
automated analysis techniquesdo not provide endtoend security
guarantees, since they focus on the logic of the protocol and tend to
abstract away from its implementation.
In this talk, I will present some recent work on formal methods for
the design and verification of cryptographic applications. I will
focus,in particular, on two fundamental, and seemingly contradictory,
properties in the design of secure systems, namely, authorization and
privacy. On the one hand, the access to sensitive resources should be
grantedonly to authorized users; on the other hand, these users would
like toshare as little personal information as possible with third
parties.
Iwill present a framework for the specification and
enforcement of privacyaware authorization policies in decentralized
systems. These policies
are specified as a set of logical rules, in which the traditional says
modality from authorization logics is accompanied by existential
quantification in order to express the secrecy of sensitive
information. The realization of these policies is obtained by a
powerful combination of digital signatures and zeroknowledge
proofs. We developed a compiler to automatically generate
cryptographic implementations (i.e.,
cryptographic library and source code) from highlevel logical
specifications. The security of these implementations is enforced
by a type system based on refinement, union, and intersection types.
Location: LMU Main Building  A U117
Links:
DateTimeTitle
[+] 18.02.2011 10:00 Kuncak Viktor: Implicit Programming through Automated Reasoning
Abstract:
We argue for a programming model where automated reasoning plays
a key role during (1) interactive program development, (2)
program compilation, and (3) program execution. I will focus on
our recent resultsin complete functional synthesis for integer
arithmetic, which is a form of program compilation based on
decision procedures. For program development, I outline our
ongoing work on resolution theorem proving for interactive
synthesis. For program execution, I describe the UDITA system
based on Java Pathfinder, and argue that programming models
related to constraint logic programming should play a bigger
role in mainstream softwa
Location:
TUM Garching, Room 03.09.014
Links:
[+] 11.02.2011 10:00 Baier Christel: On Model Checking Techniques for Randomized Distributed Systems
Abstract:
The automatabased model checking approach for randomized
distributed systems relies on an operational interleaving
semantics of the system by means of a Markov decision process
and a formalization of the desired event E by an
omegaregular lineartime property, e.g., an LTL formula.
The task is then to compute the greatest lower bound for the
probability for E that can be guaranteed even in worstcase
scenarios. Such bounds can be computed by a combination of
polynomially timebounded graphalgorithm with methods for
solving linear programs. In the classical approach, the
worstcase is determined when ranging over all schedulers
that decide which action to perform next. In particular, all
possible interleavings and resolutions of other nondeterministic
choices in the system model are taken into account.
As in the nonprobabilistic case, the commutativity of
independent concurrent actions can be used to avoid redundancies
in the system model and to increase the efficiency of the
quantitative analysis. However, there are certain phenomena that
are specificfor the probabilistic case and require additional
conditions for the reduced model to ensure that the worstcase
probabilities are preserved. Related to this observation is also
the fact that the worstcase analysis that ranges over all
schedulers is often too pessimistic and leads to extreme
probability values that can be achieved only by schedulers that
are unrealistic for parallel systems. This motivates the switch
to more realistic classes of schedulers that respect the fact
that the individual processes only have partial information
about the global system states. Suchclasses of
partialinformation schedulers yield more realistic worstcase
probabilities, but computationally they are much harder. A wide
range of verification problems turns out to be undecidable when
the goal is to check that certain probability bounds hold under
all partialinformation schedulers.
Location:
TUM Garching, Room 03.09.014
Links:
[+] 04.02.2011 10:00 Beyer Dirk: AdjustableBlock Encoding: Towards a Unified Frameworkfor Software Verification
Abstract:
Several successful software model checkers are based on a technique called
singleblock encoding (SBE), which computes costly predicateabstractions after
every single program operation. Largeblock encoding(LBE) computes
abstractions only after a large number of operations, and it was shown that
this significantly improved the verification performance. In this work, we
present adjustableblock encoding, a unifying framework that allows to express
both previous approaches. In addition, it provides the flexibility to specify
any block size between SBE and LBE, and also beyond LBE, through the adjustment
of several parameters. Such a unification of different concepts makes it
easier to understand thefundamental properties of the analysis, and makes the
differences of thevariants more explicit. Adjustableblock encoding (ABE) is
implementedas a configurable program analysis (CPA) in the verification
framework CPAchecker. We will also explain the architecture of that software
and demonstrate how easy it is to plugin new program analyses into this
framework.
Location:
TUM Garching, Room 03.09.014
Links: http://www.sosylab.org/
[+] 02.02.2011 17:00 Perst Thomas: Banking IT or how to run a changing system
Abstract: With the subprime crisis of 2007 it became clear that financialinstitutions have to steer their risks with sophisticated methods on thebasis of consolidated information about the managed business. This requirement has to be supported by an integrative and robust IT architecture which can smoothly react on a change in the business strategy. The talk will present risk steering methods, modelling techniques, and IT strategies toface the challenges of modern banking.
Location: TUM Garching, Room 02.07.014
Links:
[+] 21.01.2011 10:00 Chakraborty Samarjit: Automatatheoretic Modeling of Streaming Applications
Abstract:
Lately, there has been a considerable amount of interest in design
methodologies for embedded systems that are specifically targeted
towards stream processing, e.g., audio/video applications and control
applications processing sensor data. Streams processed by such
applicationstend to be highly bursty and exhibit a high
datadependent variability in their processing requirements. As a
result, classical event and service models such as periodic, sporadic,
etc. can be overly pessimistic when dealing with such applications. In
this talk I will discuss some of ourrecent work on using
automatatheoretic models for this domain. In particular, I will
present a new model called Event Count Automata for capturing the
timing properties and execution requirements of irregular/bursty
streams. This model can be used to cleanly formulate properties
relevantto stream processing on heterogeneous multiprocessor
architectures, such as buffer overflow/underflow constraints. Apart
from discussing the basic model, I will also talk about some
techniques to tradeoff between itsexpressiveness and analysis
complexity.
This talk is based on joint work with PS Thiagarajan from the National
University of Singapore, and L
Location:
TUM Garching, Room 03.09.014
Links:
[+] 17.12.2010 10:15 I6 application talk
Abstract:
Simon Barner (Easykit  model driven development for embedded software)
Markus Rickert (the Robotics library  open source software in robotics)
Suraj Nair (OpenTL  a general purpose tracking library)
[Optional] Sarah DiotGirard (Festo MPS systems  examples and programming language)
During the talk, each presenter will first give a general statement on his/her work, followed by showing you a small segment of the code and explain its use.
Location:
TUM Garching, Room 03.09.014
Links:
[+] 10.12.2010 10:00 Blanchet Bruno: Automatically Verified Mechanized Proof of OneEncryption Key Exchange
Abstract:
We report on a case study of OneEncryption Key Exchange (OEKE), a variant of
the Encrypted Key Exchange (EKE) protocol, using CryptoVerif. This work
essentially consists in redoing the manual proof done byBresson et al
(CCS'03), with the help of the automatic, computationallysound prover
CryptoVerif, which provides additional confidence that theproof is correct.
This case study is an opportunity for important extensions of CryptoVerif,
which we will present. These extensions include support for the computational
DiffieHellman assumption and for proofs thatrely on Shoup's lemma. They also
include additional game transformationsthat insert case distinctions manually
or merge cases that no longer needto be distinguished. Eventually, the
computation of the probability bounds for attacks has also been improved,
providing better reductions.
(joint work with David Pointcheval)
Location:
TUM Garching, Room 03.09.014
Links:
[+] 09.12.2010 17:15 Leroux Jèrôme: Vector Addition System Reachability Problem (A ShortSelfContained Proof)
Abstract:
The reachability problem for Vector Addition Systems (VASs) isa
central problem of net theory. The general problem is known decidable
by algorithms exclusively based on the classical
KosarajuLambertMayrSacerdoteTenney decomposition (KLMTS
decomposition). Recently from this decomposition, we deduced that a
final configuration is not reachable froman initial one if and only
if there exists a Presburger inductive invariant that contains the
initial configuration but not the final one. Sincewe can decide if a
Preburger formula denotes an inductive invariant, wededuce from this
result that there exist checkable certificates of nonreachability in
the Presburger arithmetic. In particular, there exists a simple
algorithm for deciding the general VAS reachability problem based on
two semialgorithms. A first one that tries to prove the reachability
by enumerating finite sequences of actions and a second one that tries
toprove the nonreachability by enumerating Presburger formulas. In
this paper we provide the first proof of the VAS reachability problem
that is not based on the KLMST decomposition. The proof is based on
the notion ofproduction relations inspired from Hauschildt that
directly provides theexistence of Presburger inductive invariants.
Location: 00.08.038
Links:
[+] 03.12.2010 10:00 Majumdar Rupak: Model Checking using Bounded Languages
Abstract:
Abstract:
Bounded languages, introduced by Ginsburg and Spanier, are subsets of regular
languages of the form w1*w2*... wk* for some words w1,...,wk. Bounded languages
have nice structural and decidability properties.
We show two applications of bounded languages in model
Location:
TUM Garching, Room 03.09.014
Links:
[+]
26.11.2010
10:00
Kostic
Dejan: Predicting Faults in Heterogeneous, Federated Distributed Systems
Abstract:
Abstract:
It is notoriously difficult to make distributed systems reliable. This becomes
even harder in the case of the widelydeployed systems that become
heterogeneous and federated. The set of routers incharge of the interdomain
routing in the Internet is a prime example ofsuch a system. The unanticipated
interaction of nodes under seemingly valid configuration changes and local
faulthandling can have a profound effect. For example, the Internet has
suffered from multiple IP prefix hijackings, as well as performance and
reliability problems due to emergentbehavior resulting from a local session
reset.
We argue that the keystep in making these systems reliable is the need to
automatically predict faults. In this talk, I will describe the design and
implementation of DiCE, a system that uses temporal and spatial awareness to
predict faults in heterogeneous, federated systems. Our live evaluation in the
testbed shows that DiCE quickly and successfully predicts two important classes
of faults, operator mistakes and programming errors, that have plagued BGP
routing in the Internet.
Joint work with Marco Canini, Vojin Jo
Location:
TUM Garching, Room 03.09.014
Links:
[+] 15.11.2010 16:00 Tuerk Thomas: Holfoot  a separation logic tool in HOL4
Abstract: I'm developing a separation logic framework based on Abstract Separation Logic inside the HOL4 theorem prover. This framework is instantiated to build Holfoot, a formalisation of Smallfoot. In this talk, I wil
Location: TUM Garching, Room 00.09.055
[+] 12.11.2010 10:00 Malacaria Pasquale: Quantifying Information Leaks in Software
Abstract: Abstract: Leakage of confidential information represents a serious security risk. Despite a number of number of recent advances, both theoretical and algorithmic, it has been unclear if and how quantitative approaches to measuring leakage of confidential information could be appliedto substantial, realworld programs. This is mostly due to the high complexity of computing precise leakage quantities. We introduce a technique which makes it possible to decide if a program conforms to a quantitative policy which scales to large statespaces with the help of the bounded model checker CBMC. Our technique is applied to a number of officially reported information leak vulnerabilities in the Linux Kernel. Additionally, wealso analysed authentication routines in the Secure Remote Password suiteand of a Internet Message Support Protocol implementation. Our technique shows when there is unacceptable leakage; the same technique is also usedto verify, for the first time, that the applied software patches indeedplug the information leaks. This is the first demonstration of quantitative information flow addressing security concerns of realworld industrial programs.
Location: TUM Garching, Room tba.
21.10.2010 10:00 Kennedy Andrew: F# and Units of Measure
Abstract:
Location: LMU Institut fuer Informatik, Oettingenstr. 67, Muenchen, L109
Links:
DateTimeTitle
[+] 17.09.2010 14:00 Manuel Fahndrich: Microsoft ResearchVortrag zur automatischen Verifizierung von Software Contracts mit Microsoft Clousot
Abstract:
Im Zuge immer komplexerer und umfangreicherer Softwareentwicklungsprojekte wird es zunehmend wichtiger, entwickelte Software von Anfangan umfangreich und effektiv zu testen, um ein qualitativ hochwertiges Produkt herzustellen. Kunden erwarten Software mit einem grossen Funktionsumfang und Komponenten, die optimal aufeinander abgestimmt sind und die dabei noch ein Hoechstmass an Sicherheit bietet.
Die Foerderinitiative Microsoft Student Partners und das Graduiertenkolleg PUMA veranstalten am 17. September 2010 einen Vortrag zum Thema Software Contracts mit Microsoft Clousot, einem kostenfreien Tool zur automatischen Verifizierung von SoftwareContracts. Manuel Fahndrich von Microsoft Research aus Redmond stellt Microsoft Clousot vor und bietet damit einen Einblick, wie Entwickler ihre Programme durch Software Contracts sicherer gestalten koennen. Der ResearchVortrag an der InformatikFakultaet der Technischen Universitaet Muenchen
Location: TUM Garching, Hoersaal 2
Links:
18.08.2010 16:00 Dullien Thomas: Analysis of binaries
Abstract:
Location: TUM Garching, 02.07.014
Links:
18.07.2010 08:30 Seidl Helmut: Fancy fixpoint algorithms for interprocedurally analyzing dataraces
Abstract:
Location: LMU Main Building  A 011
Links:
[+] 12.07.2010 14:00 Hack Sebastian: Instruction Selection by Partitioned Boolean Quadratic Programming (PBQP)
Abstract:
Since long, instruction selection for expression trees is well
understood and efficient algorithms exist based on dynamic programming,
possibly compiled into tree automata. Modern compilers, however, relyon
graphbased program representations where instruction selection is NPhard.
In this talk we present a formulation of instruction selection byPBQP and
show how the resulting instances occurring in practice can be solved efficiently.
Location: TUM Garching, 02.07.014
Links:
[+] 08.07.2010 15:00 Falk Heiko: Compilation and Optimization for hard RealTime Systems
Abstract:
During the design of software for hard realtime systems, theworstcase execution time (WCET) of a program plays an important role. Only if the WCET is known, it can be guaranteed that the software of a realtime system always terminates within given timing constraints.
However, the current state of the art in designing software for hard realtime systems is heavily unsafe. On the one hand, the actual industrial design practice relies on measurements or simulations so that no guarantees about the worstcase timing of a piece of software can be derived. On the other hand, current compilers usually optimize the averagecase execution time (ACET) of a program, instead of the WCET. Again, there is no way to derive conclusions about a program's worstcase timing if the program is optimized w.r.t. the ACET.
This talk presents a WCETaware compiler for hardrealtime systems. By tightly coupling the compiler with a tool for staticWCET analysis, it is possible for the very first time to integrate a formal WCET timing model into a compiler. This WCET timing model provides thecompiler with valuable data about the worstcase behavior of a program tobe compiled and optimized.
This timing model is then used by specialized optimizations which achieve a fully automatic minimization of the WCET.In this talk, two WCET minimizing optimizations are presented which focu
Location: TUM Garching, 02.07.014
Links:
[+] 08.07.2010 10:15 Mnich Matthias: Feedback Vertex Sets in Tournaments
Abstract: Abstract: For a tournament $T$, a feedback vertex set is a subset of vertices intersecting every directed cycle of $T$. We prove that every tournament on $n$ vertices has at most $1.6740^n$ minimal feedback vertex sets and some tournaments have $1.5448^n$ minimal feedback vertex sets. This improves an old result by Moon from 1971. Moreover, we give the first polynomialspace polynomialdelay algorithm for enumerating all minimal feedback vertex sets. As corollary we derive the fastest exponentialtime algorithm for finding a feedback vertex set of minimum size. (Joint workwith Serge Gaspers, Universidad de Chile)
Location: Room 02.04.011 at TUM Garching
Links:
[+] 01.07.2010 16:00 Droste Manfred: Weighted automata and quantitative logics
Abstract:
In automata theory, a classical result of B\uchi states that
the recognizable languages are precisely the ones definable by
sentences of monadic second order logic. We will present a
generalization of this result to the context of weighted automata.
A weighted automaton is aclassical nondeterministic automaton
in which each transition carries aweight describing e.g. the
resources used for its execution\, the length of time needed\, or
its reliability. The behavior (language) of such a weighted automaton
is a function associating to each word the weight of its execution.
We develop syntax and semantics of a quantitative logic\;
the semantics counts 'how often' a formula is true.
Our main results show that if the weights are taken either in
an arbitrary semiring or in an arbitrary bounded lattice\,
then the behaviors of weighted automata are precisely the
functions definable by sentences of our quantitative logic.
The methods also apply to recent quantitative automatamodel
of Henzinger et al. where weights of paths are determined\, e.g.\,
as the average of the weights of the path's transitions.
B\\uchi's result follows by considering the classical
Boolean algebra {0,1}.
Joint work with Paul Gastin (ENS Cachan), Heiko Vogler (TU Dresden),
resp. Ingmar Meinecke (Leipzig).
Location: TUM Garching, 02.07.014
[+] 25.06.2010 08:30 Sewell Thomas: L4.verified: An Overview, Partial Automation of Invariant Proofs in Isabelle/HOL
Abstract:
1) L4.verified: An Overview
The L4.verified project, demonstrating the functional correctness of the
seL4 microkernel, was recentlycompleted by NICTA. This makes seL4 the
world's first verified generalpurpose operating system kernel, and
marks a significant step forward inthe application of formal methods to
system software. In this talk I willgive an overview of the project,
including an introduction to the various specifications of seL4's
behaviour used in the project and an outlinethe methodology used in
proving refinement between them. I will concludeby discussing three
directions in which the verification is being extended, and the evolving
direction in which we aim to put the verification into practical use.
2) Partial Automation of Invariant Proofs in Isabelle/HOL
In this talk I will focus on a single aspect of the L4.verified pr
Location: LMU Main Building  A 011
Links:
[+] 11.06.2010 08:30 Rybalchenko Andrey: A proof rule for multithreaded programs
Abstract: I will present a proof rule for the verification of temporal safety and liveness properties of multithreaded programs that facilitates modular reasoning when possible, and provides for nonmodular reasoning when unavoidable. Then, I will show how this rule can be transformed into an automatic method
Location: LMU Main Building  A 011
Links:
[+] 26.05.2010 09:30 Noschinski Lars: Automated Complexity Analysis of Term Rewrite Systems
Abstract: Term Rewrite Systems are a simple calculus used for automated reasoning and termination analysis of programs. For terminating rewrite systems, the runtime complexity is of particular interest. I present Complexity Dependency Tuples, a modular framework for deriving feasible complexity bounds for innermost TRS. CDTs are inspired by the successful Dependency Pairs Framework for termination. They are designed to allow an easy adaption of existing techniques for this Framework.
Location: TUM Garching, 00.09.055
Links:
[+] 14.05.2010 08:30 Brauer Joerg: Automatic Abstraction for Intervals using Boolean Formulae
Abstract:
Traditionally, transfer functions have been manually designedfor each
operation in a program. Recently, however, there has been growing
interest in computing transfer functions, motivated by the desire to
reason about sequences of operations that constitute basic blocks.
Our work focuses on deriving transfer functions for intervals â?? possibly
the most widely used numeric domain â?? and shows how they can be
computed from Boolean formulae which are derived through
bitblasting. This approach is entirely automatic, avoids complicated
elimination algorithms,and provides a systematic way of handling
wraparounds (integer overflowsand underflows) which arise in
machine arithmetic.
Location: LMU Main Building  A 011
Links:
[+] 10.05.2010 16:00 Stolz Volker: The rCOS Modeler  from Software Engineering to Verification
Abstract:
In this presentation we give an overview of use casedriven development of component and object based system using Refinement of Component and Objectbase Systems, rCOS. The tool supports model construction,analysis, verification and correctness preserving transformations, andit generate verifiable code from design models.
We also report on a recent project of integrating Runtime Verification into the software engineering process.
Location: LMU Oettingerstr. 67, 151
Links:
[+] 10.05.2010 16:00 Avigad Jeremy: Decision procedures, heuristic procedures, and formally verified mathematics
Abstract:
I will describe a mixedbag of decidability results, some practical, and some not, loosely related to problems that arise in the formal verification of mathematics. First, I will discuss a decision procedurefor a fragment of a theory of asymptotic big O equations. Next, I will discuss NelsonOppen combination methods in the context of theories of thereal numbers. Finally, I will discuss the geometric proofs one finds in Euclid's *Elements*, and procedures that read information off from the diagram.
(These various projects involve joint work with Ed Dean, Kevin Donnelly, Harvey Friedman, and John Mumma).
Location: TUM Garching, 01.09.014
Links:
DateTimeTitle
[+] 26.03.2010 10:00 King Andy: Automatic Abstraction for Congruences
Abstract:
One approach to verifying bittwiddling algorithms is to deriveÂ
invariants between the bits that constitute the variables of a Â
program. Such invariants can often be described with systems of Â
congruences where in each equation $\vec{c} \cdot \vec{x} = d \mod m
$, (unknown variable m)$ is a power of two, $\vec{c}$ is a vector of Â
integer coefficients, and $\vec{x}$ is a vector of propositional Â
variables (bits). Because of the lowlevel nature of these Â
invariants and thelarge number of bits that are involved, it is Â
important that the transfer functions can be derived automatically. Â
We address this problem,showing how an analysis for bitlevel Â
congruence relationships can be
Location: TUM Garching, 02.07.014
Links:
17.03.2010 14:00 Appel Andrew: Program Logics for Foundational Static Analysis
Abstract:
Location: LMU Oettingerstr. 67, L109
Links:
[+] 29.01.2010 14:15 Hofmann Martin: What is a pure functional?
Abstract: We investigate the following question. Given a higherorder SML
Location: LMU Oettingerstr. 67, L109
Links:
[+] 13.01.2010 14:30 Dubslaff Clemens: Transition System Semantics of Message Sequence Charts
Abstract: Message Sequence Charts (MSCs) provide an intuitive notation ofcommunication systems and are used in early steps of requirement specification. The simplest form of MSCs considers only exchange of messages between several processes and its semantics is given by some partial order. Combining MSC scenarios can be conveniently done using MSCgraphs (MSGs). Since errors in early design steps have heavy impact to development costs andreliability, MSCs are popular subject of verification. Whereas model checking single MSCs is decidable, it is well known that it is undecidable for asynchronous semantics of MSG. We will present a transition system representation of MSC (and MSG) where the traces are equal to partial order linearizations. These transition systems allow us to employ model checking results for transition systems such as reachability analysis in wellstructured transition systems.
Location: TUM Garching  03.09.014
Links:
[+] 23.12.2009 09:00 Gupta Ashutosh: From tests to proofs
Abstract:
We describe the design and implementation of an automatic
invariant generator for imperative programs. While automatic
invariant generation through constraint solving has been
extensively studied from a theoretical viewpoint as a classical
means of program verification, in practice existing tools do not
scale even to moderately sized programs. This isbecause the
constraints that need to be solved even for small programs are
already too difficult for the underlying (nonlinear) constraint
solving engines. To overcome this obstacle, we propose to
strengthen staticconstraint generation with information obtained
from static abstract interpretation and dynamic execution of the
program. The strengthening comesin the form of additional linear
constraints that trigger a series of simplifications in the solver,
and make solving more scalable. We demonstrate the practical
applicability of the approach by an experimental evaluation on
a collection of challenging benchmark programs and comparisons
with related tools based on abstract interpretation and software
model checking.
Location: seminar room 02.07.014
Links:
[+] 15.12.2009 10:00 DurandGasselin Antoine: Nondeterministic automata for PresburgerArithmetic
Abstract:
The use of automata to decide Presburger Arithmetic (PA) has been
introduced by Buechi in 1960. Henceforth we represent PA's formula bythe
(minimal deterministic finite) automaton that encodes its solutions,we
therefore have a canonic representation of PA's formula. We got
interested in the use of nondeterministic automata for Presburger
arithmeticas they can be exponentially smaller.
We restrained ourselves to the class of RFSA (residual finite state
automata  automata for which the residual language of each state is a
residual of the recognized langage),for they also admit a canonical
form which is computable and minimal w.r.t. the number of states. We
give a compared study of the number of statesof the minimal
deterministic finite automaton and of the canonical RSFA, for some
simple fragments of PA.
Location: TUM Garching  01.09.014
Links:
[+] 11.11.2009 10:00 Logozzo Francesco: Clousot
Abstract: tba.
Location: tba.
Links:
[+] 30.10.2009 10:00 Hoare Tony: tba.
Abstract: tba.
Location: tba.
Links:
DateTimeTitle
[+] 26.08.2009 16:00 Hack Sebastian: Register Allocation for Programs in SSA Form
Abstract:
Register allocation is one of the most important optimizationsin a modern
compiler. It maps the variables of a program to the processor's registers in
order to accelerate the program's execution.
Graph coloring, as introduced by Chaitin, has been the most popular and most
successful register allocation technique since its introduction in the late
1970s. It reduces the assignment problem to coloring the socalled
interference graph that is constructed from the program to compile. Since
graphcoloring is NPcomplete and each undirected graph can occur as an
interference graph, register allocation is NPcomplete, too.
However, if we require the program to be in static singleassignment form
(SSA), a widely used program representation, interference graphs are no longer
general. As we will show, they belong to the class of chordal graphs. Their
most appealing property is that they can be colored optimally in quadratic
time.
We present the theoretical properties of the interference graphs of SSA
programs, outline the differences to nonSSA programs, and show how the
properties of chordal graphs help to overcome the deficienciesof traditional
register allocators.
Location: TUM Garching  02.07.014
Links:
[+] 23.07.2009 14:30 Paulson Larry: An Automatic Theorem Prover for RealValued SpecialFunctions
Abstract: Logical formulas involving special functions such as ln, exp a
Location: TUM Garching  03.09.14
Links:
[+] 17.06.2009 16:00 Maneth Sebastian: MSO Definable Tree Transductions
Abstract: One of the fundamental connections between logic and automata w
Location: TUM Garching  02.07.034
Links:
[+] 08.06.2009 17:15 Best Elke: Cyclic Structure and Separability of Persistent Petri Nets
Abstract:
We prove that the reachability graph of a persistent and bounded
Petri net can be decomposed into basic cycles which are either
Parikhdisjoint or Parikhequivalent. Based on this result, we also
prove
that a persistent, bounded, reversible and plain Petri net is
(weakly and
strongly) separable, revealing a relationship between a marking and
the
marking divided by ist least common multiple.
Location: HS2
Links:
[+] 26.05.2009 16:00 Bouajjani Ahmed: ContextBounded Analysis for Concurrent Programs with Dynamic Creation of Threads
Abstract: Contextbounded analysis has been shown to be both efficient and effective at finding bugs in concurrent programs. According to its original definition, contextbounded analysis explores all behaviors of a concurrent program up to some fixed number of context switches between threads. This definition is inadequate for programs that create threads dynamically because bounding the number of context switches in a computation also bounds the number of threads involved in the computation. In this paper, we propose a more general definition of contextbounded analysis useful forprograms with dynamic thread creation. The idea is to bound the number ofcontext switches for each thread instead of bounding the number of switches of all threads. We consider several variants based on this new definition, and we establish decidability and complexity results for the analysisinduced by them.
Location: TUM Garching  02.07.014
Links:
[+] 06.05.2009 14:15 Sassone Vladimiro: Permissionbased separation logic for messagepassing concurrency
Abstract:
The talk presents new local reasoning techniques for message
passing concurrent programs based on ideas from separation logics and
resource usage analyses. We propose a twostep analysis in which
concurrentprocesses are first analysed for confluent behaviour using
a type and effect system which provides a foundation for establishing
correctness through logical, separationbased reasoning.
Location: Oettingenstrasse 67, Raum Z1.09
Links:
DateTimeTitle
[+] 26.02.2009 16:00 Friedmann Oliver: A SuperPolynomial Lower Bound for the Parity Game Strategy Improvement Algorithm as We Know it.
Abstract: We present a new lower bound for the discrete strategy improvement algorithm for solving parity games due to Voege and Jurdzinski. First, we informally show which structures are difficult to solve for the algorithm. Second, we outline a family of games of quadratic size on which thealgorithm requires exponentially many strategy iterations, answering inthe negative the longstanding question whether this algorithm runs in polynomial time. Additionally we note that the same family of games can be used to prove a similar result w.r.t. the strategy improvement variant by Schewe.
Location: LMU  Oettinger Str. 67, room Z1.09
Links:
[+] 22.01.2009 16:00 Gast Holger: Approaches to Automated Reasoning about HeapManipulating Programs
Abstract:
Software verification in the large is feasible only with substantial automation of proofs. Due to the details of aliasing, pointer arithmetic, and data structure invariants, the challenge is specifically pronounced in the treatment of heapmanipulating programs.
The first part of the talk gives a highlevel overview of fundamental approaches and their
Location: Garching, room MI 01.11.018
Links:
[+] 15.01.2009 16:00 Sutcliffe Geoff: TPTP, TSTP, CASC, etc.  Automated Reasoning inPractice
Abstract: This talk gives an overview of activities and products that stem from the Thousands of Problems for Theorem Provers (TPTP) problem library for Automated Theorem Proving (ATP) systems. These include the TPTP itself, the Thousands of Solutions from Theorem Provers (TSTP) solution library, the TPTP language, the CADE ATP System Competition (CASC), tools such as my semantic Derivation Verifier (GDV) and the Interactive DerivationViewer (IDV), metaATP systems such as the Smart Selective Competition Parallelism (SSCPA) system and the Semantic Relevance Axiom Selection System (SRASS), online access to automated reasoning systems and tools throughthe SystemOnTPTP web service, and applications in various domains. Current work extending the TPTP to higherorder logic will be introduced.
Location: Garching, room MI 01.11.018
Links:
DateTimeTitle
[+] 12.04.2008 16:00 Kammueller Florian: ASPfun: Ein Kalkuel fuer Verteilte Aktive Objekte in Isabelle/HOL
Abstract:
Im Zeitalter des Internet muss sich das verteilte Rechnen mit asynchronen parallelen Aktivitaeten, Codeverteilung und komplexen Aufrufstrukturen auseinandersetzen. Wir stellen in diesem Vortrag den Kalkuel ASPfun fuer funktionale, aktive Objekte vor. ASPfun erweitert die Theorie derObjekte um eine Kommunikation mit einem RequestReplyMechanismus, basierend auf sogenannten Futures. Futures repraesentieren erwartete Antwortenvon Requests; Replies geben das Ergebnis eines Requests an das Objekt zurueck, das die entsprechende Future enthaelt.
Dieser Vortrag stellt zuerst den ASPfunKalkuel und seine Semantik vor. Danach praesentieren wir ein Typsystem fuer ASPfun, das Progress  und damit Verklemmungsfreiheit sicherstellt. ASPfun und seine Eigenschaften sind formalisiert und bewiesen mit dem Theorembeweiser Isabelle.
Location:
Links:
Workshops
DateTimeTitle
[+] 24.09.2012 09:00 PUMA Workshop 2012  Goldegg
Abstract:
Location: Goldegg
DateTimeTitle
[+] 03.10.2011 00:00 PUMA Workshop 2011  Traunkirchen
Abstract:
Location: Traunkirchen
DateTimeTitle
[+] 10.10.2010 00:00 PUMA Workshop 2010  Szentendre
Abstract:
Location: Szentendre
DateTimeTitle
[+] 10.07.2010 11:00 TruSoft meets PUMA
Abstract:
TrustSoft meets PUMA

Beg
Location: TUM Garching, 02.07.014
DateTimeTitle
[+] 04.10.2009 00:00 PUMA Workshop 2009  Venice
Abstract:
Location: Venice
DateTimeTitle
[+] 17.08.2009 00:00 PUMA Sponsored Talks at TPHOL
Abstract:
Location: http://www.novotel.com/gb/hotel3280novotelmuenchencity/index.shtml
Links: http://tphols.in.tum.de/
[+] 10.07.2009 00:00 PUMA Reading Group
Abstract:
Location:
DateTimeTitle
[+] 13.11.2008 08:00 DTUM workshop
Abstract:
Location:
DateTimeTitle
[+] 28.09.2008 00:00 PUMA Workshop 2008  Spitzingsee
Abstract:
Location: Spitzingsee
[+] 08.09.2008 08:00 Workshop lightweight verification
Abstract:
Location: GI Jahrestagung 2008
Links: http://www4.in.tum.de/LV08/
Ringvorlesung
DateTimeTitle
[+] 08.02.2012 15:30 Hoder Krystof: Interpolants, FixedPoints and Verification
Abstract:
The talk will consist of two parts. The first will give a brief
introduction on interpolation
and present a technique for interpolant generation based on local
proofs. We will also talk about
some recent extensions of this method, such as interpolant minimization
which uses pseudoboolean
optimization to generate better interpolants.
In the second part we will present Ã?Â¼Z, a tool built on the top of the
Z3 SMT solver,
with Dataloglike interface, support for theories and abstract
interpretations, and with
a portfolio of solving strategies. We will briefly mention our recent
work on a property directed reachability algorithm formodel checking.
Location: TUM Garching  Room 00.09.055
Links:
[+] 07.02.2012 15:30 Hoder Krystof: The Vampire Theorem Prover
Abstract:
Vampire ( http://vprover.org ) is one of the best performing firstorder
theorem provers,
consistently winning several divisions of the CASC theorem prover
championship for the past ten years.
This talk will give a basic overview of its internals, such as the
resolution and superposition calculus,
preprocessing, indexing structures and splitting.A particular attention
will be given to the Sine axiom
selection algorithm which helps with reasoning on problems with large
amounts of axioms.
Location: TUM Garching  Room 00.09.055
Links:
[+] 20.01.2012 10:00 Lange Martin: Temporal Logics and Related Automata Theory
Abstract:
The purpose of this tutorial is to introduce temporal logics asformal languages
for the specification and verification of programs. Wewill consider the main algorithmic
problems that come with temporal logics like satisfiability and model checking, as well as
more pragmatic aspects like their expressive power. Automata theory has proved to be
very useful as a toolbox for answering corresponding questions. We aim to give abroad
overview over the known results and techniques used in these areas.
The first part (~ Thursday) will deal with lineartime logics, mainly LTL and PSL, and
automata on infinite strings. Branchingtime logics willbe covered in the second part
(~ Friday).
Location: TUM Garching  Room 02.07.014
Links:
[+] 19.01.2012 16:00 Lange Martin: Temporal Logics and Related Automata Theory
Abstract:
The purpose of this tutorial is to introduce temporal logics asformal languages
for the specification and verification of programs. Wewill consider the main algorithmic
problems that come with temporal logics like satisfiability and model checking, as well as
more pragmatic aspects like their expressive power. Automata theory has proved to be
very useful as a toolbox for answering corresponding questions. We aim to give abroad
overview over the known results and techniques used in these areas.
The first part (~ Thursday) will deal with lineartime logics, mainly LTL and PSL, and
automata on infinite strings. Branchingtime logics willbe covered in the second part
(~ Friday).
Location: TUM Garching  Room 01.10.011
Links:
[+] 11.11.2011 08:30 Neumann Thomas: Algebraic Join Order Optimization in Databases
Abstract:
When compiling users queries into imperative execution plans,query optimizers
use a wide range of optimization techniques to speed upthe resulting plan.
Join queries are a particular interesting class of queries, as they are
common, often expensive to execute, and hard to optimize.
Location: TUM Garching  Room 02.07.014
Links:
[+] 04.11.2011 08:30 Neumann Thomas: Algebraic Join Order Optimization in Databases
Abstract:
When compiling users queries into imperative execution plans,query optimizers
use a wide range of optimization techniques to speed upthe resulting plan.
Join queries are a particular interesting class of queries, as they are
common, often expensive to execute, and hard to optimize.
Location: TUM Garching  Room 02.07.014
Links:
DateTimeTitle
[+] 08.07.2011 08:30 Klein Gerwin: Verification of the seL4 microkernel
Abstract:
In this talk I will present an overview of the formal verification of
the seL4 microkernel in Isabelle/HOL. The verification encompasses a
proof of functional correctness from the C implementation of the kernel
up to an abstract Isabelle/HOL specification of its functionality. The
talk will cover the main points of the verification effort, such as the
C subset, the rapid prototyping methodology, and the refinement
and Hoarelogic calculi used in the verification, and will discuss
some of the challenges that we encountered.
Location: LMU Main Building  A U117
Links:
[+] 11.05.2011 16:00 Genet Thomas: Talk 1: Reachability Analysis of Rewriting using Tree
Abstract:
I will present Tree Automata Completion which is a verificationtechnique we
have been developping and implementing in the Timbuk tool,for some years at
IRISA. This technique aims at proving safety properties on programs represented
by Term Rewriting Systems. Tree automata are used to (finitely) represent the
(infinite) sets of reachable states of theprograms. In this setting, proving
safety properties on programs consists in showing that bad program states,
violating the property, are notrecognized by the tree automaton, i.e. are
unreachable.
To constructthis tree automaton, the completion technique we develop attempts
to combine some of the advantages of modelchecking, abstract interpretation and
interactive proof. Like modelchecking, it can automatically prove safety of
finite systems and of some classes of infinite systems having a regular
representation. Outside of those classes, and like with abstract interpretation,
tree automata completion permits to safely and finitely overapproximate the
behavior of infinite state systems. Approximations are defined using
abstraction equations that can either be generated or giv
Location: TUM Garching, Room 00.09.05
DateTimeTitle
[+] 18.01.2011 16:00 Flemming Nielson: Flow Logic for Process Calculi
Abstract: Plans for Flow Logic for Process Calculi at TUM (January 2011)\
Location: TUM Garching, Room 03.09.014
DateTimeTitle
02.07.2010 08:30 Brandt Felix: Social Choice
Abstract:
Location: LMU Main Building, A 001
Links:
[+] 30.04.2010 08:30 Simon Axel: Widening Polyhedra with Landmarks
Abstract:
The abstract domain of polyhedra is su?ciently expressive
to be deployed in veri?cation. One consequence of the richness of this
domainis that long, possibly in?nite, sequences of polyhedra can arise
in the analysis of loops. Widening and narrowing have been proposed to
infer asingle polyhedron that summarises such a sequence of polyhedra.
Motivated by precision losses encountered in veri?cation, we explain how
the classic widening/narrowing approach can be re?ned by an improved
extrapolation strategy. The insight is to record inequalities that are thus
far found to be unsatis?able in the analysis of a loop. These socalled
landmarkshint at the amount of widening necessary to reach stability.
This extrapolation strategy, which re?nes widening with thresholds, can
infer post?xpoints that are precise enough not to require narrowing. Un
like previous techniques, our approach interacts well with other domains,
is fully automatic, conceptually simple and precise on complex loops.
Location: LMU Main Building  A 011
Links:
DateTimeTitle
22.01.2010 10:05 Rybalchenko Andrey: Interpolation
Abstract:
Location: TUM Garching  02.07.014
Links:
15.01.2010 10:05 Rybalchenko Andrey: Termination
Abstract:
Location: TUM Garching  03.09.14
Links:
[+] 16.12.2009 14:00 Weidenbach Christoph: Automation of Logic
Abstract:
SAT, SMT, Resolution, Completion, Superposition
Superposition(Theorie), Superposition(Induction),
Applications (Automata, Transition Systems)SAT, SMT, Resolution, Completion, Superposition
Superposition(Theorie), Superposition(Induction),
Applications (Automata, Transition Systems)
Location: TUM Garching
Links:
DateTimeTitle
[+] 19.05.2009 16:00 Cousot Patrick:
Abstract: tba.
Location: LMU Main Building  A U117
Links: