Warning: Invalid argument supplied for foreach() in /mnt/html/ppuma/html-data/mediawiki/extensions/calendar/modules/iCalReader.php on line 508

Warning: array_multisort(): Argument #1 is expected to be an array or a sort flag in /mnt/html/ppuma/html-data/mediawiki/extensions/calendar/modules/iCalReader.php on line 523

Warning: Invalid argument supplied for foreach() in /mnt/html/ppuma/html-data/mediawiki/extensions/calendar/modules/calendar.php on line 120
Calendar - PUMA Graduiertenkolleg
Personal tools

Calendar

From PUMA Graduiertenkolleg

Jump to: navigation, search

< September 2017 >

Monday

Tuesday

Wednesday

Thursday

Friday

Saturday

Sunday

18.09
19.09
20.09
21.09
22.09
23.09
24.09
25.09
26.09
27.09
28.09
29.09
30.09
01.10

Talks

Term: SS17:

DateTimeTitle

[+] 30.06.2017 08:30 Felix Klaedtke: Runtime Verification of Temporal Properties over Out-of-order 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 three-valued semantics for the real-time logic MTL. The three-valued 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).

[+] 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 free-choice workflow Petri nets, but with a built-in 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 PSPACE-hard in the general case.

In this paper we generalize and explain these results. We introduce a general static analysis frameworkfor negotiations, and define Mazurkiewicz-invariant static analysis problems, which encompass the questions above and new ones.

We show that Mazurkiewicz-invariant analysis problems can be solved in PTIME for sound deterministic negotiations iff they can be solved in PTIME for sequential flow-graphs---even though the flow-graph 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 semi-linear sets: the past, the present and the future

Abstract: Presburger arithmetic, the first-order 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 semi-linear sets, a generalisation of ultimately periodic sets to higher dimensions. The goal of this talk is togive a comprehensive overview about Presburger arithmetic and semi-linearsets, about their history and notable results. I will also discuss in more detail some recent work on the descriptive complexity of Boolean operations on semi-linear sets. This talk is partly based on joint work with Dmitry Chistikov.

[+] 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

Term: WS16/17:

DateTimeTitle

[+] 20.03.2017 15:00 David de Frutos: Understanding (Concurrent) Process Semantics [second talk]

Abstract: Once asynchronous parallellsm induces non-determinism, 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.

[+] 17.03.2017 10:00 David de Frutos: Understanding (Concurrent) Process Semantics [first talk]

Abstract: Once asynchronous parallellsm induces non-determinism, 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.

[+] 03.03.2017 10:00 Edon Kelmendi: Half-positional Two-player Stochastic Games

Abstract: We consider zero-sum 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 shift-invariant and submixing, then the game is half-positional, 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 non-deterministic automata do not fit, e.g., probabilistic model checking.

In this talk I will explain a polynomial time-bounded algorithm for probabilistic model checking of discrete-time Markov chains against unambiguous Büchi automata specifications and compare it withknown approaches for deterministic omega-automata, 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 Time-Varying Environments

Abstract: Trajectory planning for automated vehicles is a major problem in
robotics. This problem is in particular challenging for time-varying
environments and systems with constraint dynamics. Commonly used
sampling-based 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 two-dimensional motion with bounded speed and acceleration
in time-varying environments. The proposed method computes an
over-approximative 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.

[+] 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 general-purpose 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

[+] 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 on-the-fly 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 time-triggered, avoiding accumulated errorfrom geometric intersections. We enhance our static technique by combining time-triggered transitions with occasional space-triggered transitions,and demonstrate the benefits of the combined approach in what we call mixed-triggered 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 continuous-time 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 DNA-walkers.

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 context-free Chomsky grammars, namely context-free GTSs, aka hyper-edge 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.

[+] 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 well-known model of Discrete-Time 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

Term: SS16:

DateTimeTitle

[+] 13.09.2016 15:00 Julia Krämer: The Value of Attack-Defence Diagrams

Abstract: In an increasingly connected world, formal specification and verification of cost-intensive and mission-critical cyber-physical systemshave become a crucial element of design processes both in industry and research. Especially in the area of security-critical systems, such as powerplants and water supply works, the application of these techniques can save not only costs but also human lives.

Security-critical 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 security-critical 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 Attack-Defence Diagrams as an extension of attack trees, which can represent all of the aforementioned situational conditionsat the same time. Hence, Attack-Defence 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 cyber-security, the semantics enables an efficient what-if 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 model-checking 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 simply-typed lambda calculus

Abstract: Consider the simply-typed 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: Limit-Deterministic Büchi Automata for Linear TemporalLogic

Abstract: A Büchi automaton is said to be limit-deterministic 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 limit-deterministic Büchi automaton. Contrary to the indirect approach of constructing a non-deterministic automaton for the input formula and then applying a semi-determinisation 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 model-checking,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 black-box 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.

[+] 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 shared-memory programs. However, its highEXPSPACE-complete complexity poses a challenge when encountered in real-world 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 polynomial-time 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

[+] 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

[+] 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 Ford-Fulkerson algorithm using Isabelle/HOL

Abstract: The Ford-Fulkerson algorithm is a method for solving the Maximum-Flow-Problem 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 Ford-Fulkerson algorithm, and present the Ford-Fulkerson 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 cyber-physical 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 meta-argument 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.

[+] 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 proof-theoretic results on the relationship betweeninduction and tree grammars.

These results suggest an algorithm for pro

Term: WS15/16:

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 user-centric interactive theorem proving and machine-centric 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: Failure-aware Runtime Verification

Abstract: Prior runtime-verification 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 real-time logic MTL that efficiently handles out-of-order message deliveries andoperates in the presence of failures. It uses a three-valued 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.)

[+] 26.02.2016 10:00 Dmitry Chistikov: Navigating one-counter automata: Directions in the mountains

Abstract: One-counter automata (OCA) are finite-state automata with a counter that supports increments, decrements, and tests for zero. They correspond to an intermediate class between regular and context-free 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 many-valued 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 correct-by-construction 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 XML-documents 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 XML-documents. 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 zero-sum free, commutative strong bimonoid is recognizable.

[+] 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 language-theoretical 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.)

[+] 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 non-negative 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.

[+] 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 well-structured transition systems. Indeed, vector addition systems with configurations equipped with the classical point-wise ordering are well-structured transition systems. Based on this observation, problems like the coverability or the termination are shown to be decidable. However, the well-structured 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 quasi-order that satisfies an amalgamation property. This observation provides a unifying way for solving many problems for vector addition systems including the central reachability problem.

[+] 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 time-dependent 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.

[+] 27.11.2015 10:00 Stefan Wagner: Empirical Results on Cloning and Clone Detection

Abstract: Cloning means the use of copy-paste 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.

[+] 13.11.2015 10:00 Anca Muscholl: Word transducers: from 2-way to 1-way

Abstract: Two-way finite-state transducers on words are strictly more expressive than one-way transducers. It has been shown recently how to decideif a two-way functional transducer has an equivalent one-way transducer [Gauwin et al 2013], and the complexity of the algorithm is non-elementary. 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 one-way transducer of doubly exponential size. We also show that the bound on the size of the transducer is tight, and that the one-way definability problem is undecidable for non-functional transducers.

(joint work with F. Baschenis, O. Gauwin, G. Puppis, FSTTCS’15)

[+] 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
general-purpose programming constructs such as parallel and sequential
composition, conditional tests, and iteration, as well as
special-purpose 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 equationally-defined
properties of networks.

[+] 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

Term: SS15:

DateTimeTitle

[+] 31.07.2015 08:00 Zuzana Komarkova: Unified View on Multiple Mean-Payoff Objectives in Markov Decision Processes

Abstract: We investigate Markov decision processes (MDPs) with multiple long-run average (also called mean-payoff) objectives. There exist two diff

Location: tba

Links:

[+] 29.07.2015 09:00 Maximilian Claus: Model Checking With Higher-Order Automated Theorem Provers – A Logic Embedding Approach

Abstract: A model checker takes two inputs: a model description (here: afinite-state 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 hard-wired into the model checker to allow
for the use of a heavily optimised decision procedure. State-of-the-art examples include Spin [1] (for LTL), which
uses an automaton-based 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 Domain-Specific 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 Martin-Lö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 (proof-relevant 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 Cyber-Physical 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 Ann-Christin 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 first-order 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 computer-checked proofs developed using the proof assistant Isabelle. We perform anin-depth 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 partial-order 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.

[+] 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 set-valued dynamics and possibly non-deterministic 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 well-defined 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.

[+] 18.06.2015 16:00 Nathanaël Fijalkow: Trading Bounds for Memory in Games with Counters

Abstract: We study two-player games with counters played on graphs. We investigate a conjecture by Colcombet and Löding which states the existenceof a trade-off between the size of the memory and the bound achieved on the counters. They proved that this conjecture implies the decidability of cost monadic second-order logic over infinite trees, as well as the decidability of the Rabin-Mostowski 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 cyber-physical systems has been established in recent years. Examples are automated vehicles, surgicalrobots, smart grids, and collaborative human-robot 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

[+] 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 cyber-physical systems has been established in recent years. Examples are automated vehicles, surgicalrobots, smart grids, and collaborative human-robot 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

[+] 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 cyber-physical systems has been established in recent years. Examples are automated vehicles, surgicalrobots, smart grids, and collaborative human-robot 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 Tree-to-string Transducers is decidable

Abstract: We show that equivalence of deterministic top-down tree-to-string transducers is decidable, thus solving a long standing open problem informal language theory. We also present efficient algorithms for subclass

[+] 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 well-specified 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 well-specified, then it is said to compute thepredicate that assigns to each initial configuration its consensus value.

While the predicates computable by well-specified protocols have been e

Location: LMU D Z007

Links:

Term: WS14/15:

DateTimeTitle

[+] 13.03.2015 10:00 Alexander Weinert: Automatically Proving Memory Safety and Termination of C-Programs

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 real-world languages, such as C, which feature runtime memory-allocation and explicit pointer-arithmetic.

In this talk, we present a method for showing termination of C-programs.
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 C-programs.

Location: TUM MI 02.07.014

Links:

[+] 16.02.2015 10:15 Andrei Popescu: Consistency of the logic of Isabelle/HOL

Abstract: Gordon's Higher-Order Logic (HOL) extends Church's HOL with rank-1 polymorphism and a mechanism for non-empty 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: Client-side enforcement of web session integrity through secure multi-execution

Abstract: Sessions on the web are fragile. They have been attacked successfully in many ways, by network-level attacks, by direct attacks on session cookies (the main mechanism for implementing the session concept) andby application-level attacks where the integrity of sessions is violated by means of cross-site request forgery or malicious script inclusion.

Inthis talk, a variant of non-interference is introduced - that can be used to formally define the notion of client-side application - level web session integrity. The work also develops and proves correct an enforcement mechanism. Combined with state-of-the-art countermeasures for network-leveland cookie-level attacks, this enforcement mechanism gives very strong assurance about the client-side 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 run-time errors in the analyzed programs. Verasco enjoys a modular architecture that supports the extensible combination of multiple abstract domains, both relational and non-relational. Verasco integrates with the CompCert C formally-verified 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.

[+] 02.02.2015 11:00 Xavier Rival: Construction of modular abstract domains for heterogeneous properties

Abstract: In this talk, we study the construction of shape-numeric 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 shape-numeric 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.

[+] 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 Shared-Memory 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, bounded-value 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 finite-state machines, pushdown machines, and Turing machines.Our
proofs use combinatorial characterizations of
computations in the model, and in case of pushdown-systems, some novel
language-theoretic constructions of independent interest.

This is joint work with Pierre Ganty and Rupak Majumdar.

[+] 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 data-structures maintained by the program. Our aim in this talk to describe an efficient way of doing shape analysis for concurrent (or multi-threaded) programs. The main idea is to decompose the heap into regions that are accessed in a mutually-exclusive 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 joint-work (in-progress!)with Arnab De and Suvam Mukherjee.

Location: TUM MI 02.07.014

Links:

[+] 05.12.2014 10:00 Peter Habermehl: Logics and Automata for Multi-attributed Data Words

Abstract: We consider temporal logics on multi-attributed data words which are words over a finite alphabet where each position additionally carries multiple data values from an infinite domain. Multi-attributed data words can model naturally executions of object-oriented or parallel systems. Recently, BD-LTL 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 ND-LTL, an extension of BD-LTL by a restrictedform of tuple-navigation. 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.

[+] 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 multi-objective model checking to investigate trade-offs between several properties, and extensions to stochastic multi-player games.

[+] 10.10.2014 08:30 PUMA talk by Annette Bieniusa

Abstract: tba

Location: TUM MI 02.07.014

Links:

Term: SS14:

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 scale-free, in the sense that the equations remain thesame as the populations grow.

[+] 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 rendez-vous 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 omega-regular specifications. This is joint work with I. Walukiewicz.

[+] 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 Cyber-Physical 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 ad-hoc 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 correct-by-design 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 correct-by-design 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.-Scholl-Pl. 1 (E)

Links:

[+] 27.06.2014 08:30 An SMT-based 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
shared-memory or asynchronous message-passing 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ánLedesma-Garza, Rupak Majumdar
and Filip Niksi, to appear in CAV 2014.

Location: LMU room E 210, Geschw.-Scholl-Pl. 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 re-implementation 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.

[+] 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 well-chosen 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,1-game.

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 nicht-funktionale 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 SW-Schicht (RTE = Runtime Environment) gewährleistet alle
nicht-funktionalen 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 nicht-funktionale 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
operating-system 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 Hyper-Safety Properties

Term: WS13/14:

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 Event-B.

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 polynomial-time decidable. The
Weisfeiler-Lehman 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 Cai-Fuerer-Immerman 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 W-L 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

[+] 09.12.2013 16:00 Thiagarajan P.S.: Analysis of Continuous Dynamical Systems Via Statistical Model Checking

Abstract: Systems with real-valued variables that evolve continuously w.r.t. time arise
in many settings including cyber-physical 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 real-valued variables can be large and their dynamics can
be non-linear. 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 assumptions-induces 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.

[+] 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 i-th 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 omega-regular
language. However we show that this is not always the case. Consequently,
we develop the notionof an epsilon-approximation, based on the transient and long term behaviors of M . Briefly, a symbolic trajectory is an epsilon-approximation ofanother one iff (1) they agree during their transient phases;
and (2) both trajectories are within an epsilon-neighborhood 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 epsilon-approximations satisfies the given specification; (ii) for each infiniteword in L, all its epsilon-approximations satisfy the specification. These verification results are strong in that they apply to all finite stateMarkov chains.

[+] 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 finite-state 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 SMT-Solver 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.

[+] 15.11.2013 10:00 Althoff Matthias: Formal Verification of Cyber-Physical 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 human-robot systems, to name only a few.It
is obvious that most of those systems are either safety- or
operation-critical, demanding methods that automatically verify their
safety andcorrect operation.

In this talk, I present reachability analysis as amethod to formally
verify cyber-physical 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,
phase-locked loops, and smart grids. In the remainder of the talk,
futureresearch directions for compositional verification, model-based
design techniques, and fault-tolerant systems are suggested.

Term: SS13:

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 high-impact 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 real-world 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 higher-order 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 higher-order. 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
L-series L(s, chi), where s is a complex number and chi isa character modulo
k. One then sums certain expressions involving the L-series 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 higher-order model checking in practice.

Abstract: Higher-order recursion schemes (HORS) are a kind of grammar whose non-terminals
are simply typed. They provide a precise model of control-flow in programs featuring
higher-order recursive functions. The model-checking 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 equi-expressive 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 model-checking 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 saturation-like 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 thread-creation. In this talk, we present an
extension of DPNs that support join-operations 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 PSPACE-complete for a
constant number of locks and 3processes.
For dynamic thread creation without joining, the problem remains
PSPACE-complete, if we are only interested in reaching a configuration
where a constant-size 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 Mueller-Olm, 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 partial-order 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 hard-to-solve 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 Durand-Gasselin Antoine: From Monadic Second-Order Definable StringTransformations to Transducers

Abstract: Courcelle (1992) proposed the idea of using logic, in particular
Monadic second-order 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 two-way
finite state string-to-string transducers and showed that their
expressiveness matches MSO-definable transformations (MSOT).

Alur and ?erný (2011) presented streaming transducers â??one-way
transducers equipped with multiple registers that can store output
stringsâ?? as an equi-expressive model. Natural generalizations of
streaming transducers to string-to-tree (Alur and Dâ??Antoni, 2012) and
infinite-string-to-string (Alur, Filiot, and Trivedi, 2012) cases
preserve MSO-expressiveness.

While earlier reductions from MSOT to streaming transducersused two-way
transducers as the intermediate model, I will revisit theearlier
reductions in a more general, and previously unexplored settingof
infinite-string-to-tree 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 string-to-tree transducers yields
non-trivial decidabilityresults for instance the decidability of
functional equivalence for MSO-definable infinite-string-to-tree
transformations.
(joint work with Rajeev Alur and Ashutosh Trivedi, to appear in LICS 2013)

[+] 31.05.2013 10:00 Seidl Helmut: How to Combine Widening and Narrowing for Non-monotonic Systems of Equations.

Abstract: Non-trivial analysis problems require complete lattices
with infinite ascending and descending chains. In order
to compute reasonably precise post-fixpoints 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 non-monotonic, this is no longer the case for narrowing.
A narrowing iteration to improve a given post-fixpoint, additionally,
must assume that all right-hand sides are monotonic.

The latter assumption, though, is not met in presence of widening.
It is also not met by equation systems corresponding to context-sensitive
interprocedural analysis, possibly combining context-sensitive analysisof
local information with flow-insensitive 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 round-robin as well as of worklist iteration, local, and
side-effecting 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 shared-memory 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 EXPSPACE-complete, 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 cycle-length bound.Similarly, our undecidability proof
for linearizability suggests an incomplete detection algorithm which limits the
number of ``barriers'' bisecting non-overlapping operations. Our decidability
proof of bounded-barrier 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 variables---including e.g. integer and real arithmetic, bit-vectors and arrays---and 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 back-end. This is joint work with Andrey Rybalchenko.

[+] 03.05.2013 10:00 Cyriac Aiswarya: Model Checking Languages of Data Words

Abstract: We consider the model-checking 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 second-order (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 first-order 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.

[+] 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 Shared-Memory 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, bounded-value 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 finite-state machines, pushdown machines, andTuring machines. Our proofs use combinatorial characterizationsofcomputations in the model, and in case of pushdown-systems, some novellanguage-theoretic constructions of independent interest.

Term: WS12/13:

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 Linear-Constraint 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 single-path or
multipath loops, the complexity of the Linear Ranking problem has not
yet been determined. We show that it is coNP-complete. 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. Ben-Amram)

Location: Garching MI 02.07.014

[+] 13.03.2013 14:00 Terauchi Tachio: A Template-based Approach to Complete Predicate Refinement

Abstract: Predicate abstraction has proven successful for the verification of
software programs, especially when it is combined with a
counterexample-guided predicate refinement (i.e., predicate inference)
method. However, except for a few restricted first-order theories,
the current predicate refinement methods are incomplete in that
the counterexample-guided abstract-and-refine 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 underlyingfirst-order theory.

This talk presents a predicate refinement approachthat is
complete for the quantifier-free 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
template-based, inspired by thework on template-based (or,
``constraint-based'') program verification.To make the approach
scale, we make an important observation that the first-order
logic constraints that are solved to infer the predicates are
always repetitions of certain patterns (they are generated from a
set of``Horn-clause like'' rules), so as to limit the expensive
template-based inference to a small number predicate variables in
the constraints.

This is a joint work with Hiroshi Unno and Naoki Kobayashi.

[+] 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 interpolation-based 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
open-source C verification framework we built in theLLVM compiler
infrastructure. This is joint work with Arie Gurfinkel (SEI, CMU) and
Marsha Chechik (Univ. of Toronto).

[+] 08.02.2013 10:00 Terepeta Michal Tomasz: Recursive Advice for Coordination

Abstract: Aspect-oriented programming is a programming paradigm that is often praised for the ability to create modular software and separate cross-cutting 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.

     01.02.2013 10:00 Vogel-Heuser 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: Type-Based Enforcement of Secure Programming Guidelines Code Injection Prevention at SAP

Abstract: Code injection and cross-site 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 Java-like 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 context-sensitive inference for real Java programs.

Location: Garching MI 02.07.014

Links:

[+] 11.01.2013 10:00 Zimmerman Martin: Cost-Parity Games and Cost-Streett Games

Abstract: We consider two-player games played on finite graphs with costson edges
and introduce two wining conditions, cost-parity and cost-Streett, which
require bounds on the costs between requests and their responses.

For cost-parity games we show that the first player has positionalwinning
strategies and that determining the winner lies in NP intersection co-NP.
For cost-Street games we show that the first player has finite-state
winning strategies and that determining the winner is EXPTIME-complete.

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 finite-state graph whereeach transition is
labeled by a
vector of resource updates, where everyupdate is a non-positive 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: Fixed-delay Events in Generalized Semi-Markov ProcessesRevisited

Abstract: In the area of probabilistic verification and performance evaluation, the behavior of
real-life systems such as queues, assembly linesor communication protocols are
analyzed using formal mathematical models, such as Generalized Semi-Markov
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 long-run.
The instabilityis caused by properties of the model not found in real-life. 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 massive-scale stochastic models of computing systems

Abstract: Fluid (or mean-field) techniques, rooted in statistical mechanics and physical chemistry, provide accurate deterministic approximationsto massive-scale Markov chain models of interacting agents. The originaldiscrete-state 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 state-explosion problem of Markovian models of computing systems.

Then, I will introduce the concept of 'continuous-state 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 reaction-diffusion 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:

Term: SS12:

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 NP-complete for some restricted systems.
Nevertheless, we also introduced some techniques for overestimation of
worst-case 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 first-order 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 first-order logic and then using automated first-order
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 well-suited for
problems relying largely on linear algebra. General-purpose 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 fixed-point

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\odel-Kolmogorov-Art\\emovdefinition of intuitionistic logic as embedded into a classical modal logic of proofs, and of the Curry-Howard 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 multi-agent 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:

Term: WS11/12:

DateTimeTitle

[+] 24.02.2012 10:00 Traytel Dmitriy: Extending Hindley-Milner 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 type-correct according to
thestandard Hindley-Milner 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 self-organising wireless ad-hoc networks that can provide
broadbandcommunication without relying on a wired backhaul
infrastructure. This has the benefit of rapid and low-cost network
deployment. Traditionally,the main tools for evaluating and validating
network protocol are simulation and test-bed experiments. The key
limitations of these approaches are that they are very expensive, time
consuming and non-exhaustive. 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
``time-to-market'' 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 Model-Checking Higher-Order Recu

Abstract: Higher-order recursion schemes (HORS) can be viewed as simply typed terms in
the lambda-calculus with recursion and thereby provide a useful model for the
behaviour of higher-order functional programs. SinceOng's original proof
[LICS 2006] that the mu-calculus model-checking 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 HORS---namely `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-
calculusmodel-checking 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: Non-parametric 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
non-parametric. 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 step-indexedKripke logical
relation for a language with both non-parametric polymorphism (in the form
of type-safe cast) and dynamic type generation. Our logical relation enables
us to establish parametricity and representation independence results, even
in a non-parametric setting, by attaching arbitrary relational
interpretations to dynamically-generated 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 non-parametric
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
multi-site, multi-language, multi-vendor 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 large-scale 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 First-order 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 first-order 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 In-Memory 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 starts-with predicates
These predicates can be efficiently implemented using
a compressed self-index of the document's text data.

Location: TUM Garching - Room 02.07.014

Links:

[+] 20.01.2012 08:30 Katoen Joost-Pieter: Formal Verification and Performability Analysi

Abstract: The engineering process of on-board critical embedded systems involves a wide range of diverse approaches and techniques for system-levelaspects 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 on-board 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 general-purposemodeling 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 state-of-the-art 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: SAT-based 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 SAT-based 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 Ramsey-based 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
andtwo-letter 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 Christoph-Simon: 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 re-running 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 Almost-Full Adventures in constructive termination

Abstract: Disjunctive well-foundedness (used in Terminator), size-changetermination, and well-quasi-orders (used in supercompilation and term-rewrite 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 place-replication 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 Stacking-based 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 large-scale programs with object-oriented features by PDSs.
In this talk, I will introduce our efforts and preliminary results on designing
precise yet scalable stacking-based 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
points-to 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 Ledesma-Garza 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 higher-order
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:

Term: SS11:

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 thread-local
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 re-entrant 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 pre-defined. 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,
Tnf-alpha. 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 privacy-compliant data-handling 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 microkernel-based systems

Abstract: This talk presents our current work on the verification of security
and safety properties on the code-level 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 acase-study system, and the proof that seL4 enforces the
high-level 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 age-old 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 non-expert 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 data-structure such as a BDD. The algorithm combines model enumeration with the generation of shortest prime implicants so as to converge ontoa quantifier-free 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 PSPACE-complete. 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 single-threaded 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 side-effects. 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 fine-grained 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 error-prone 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 end-to-end 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 privacy-aware 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 zero-knowledge
proofs. We developed a compiler to automatically generate
cryptographic implementations (i.e.,
cryptographic library and source code) from high-level 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:

Term: WS10/11:

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 automata-based 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
omega-regular linear-time 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 worst-case
scenarios. Such bounds can be computed by a combination of
polynomially time-bounded graphalgorithm with methods for
solving linear programs. In the classical approach, the
worst-case 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 worst-case
probabilities are preserved. Related to this observation is also
the fact that the worst-case 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
partial-information schedulers yield more realistic worst-case
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 partial-information schedulers.

Location: TUM Garching, Room 03.09.014

Links:

[+] 04.02.2011 10:00 Beyer Dirk: Adjustable-Block Encoding: Towards a Unified Frameworkfor Software Verification

Abstract: Several successful software model checkers are based on a technique called
single-block encoding (SBE), which computes costly predicateabstractions after
every single program operation. Large-block 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 adjustable-block 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. Adjustable-block 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 plug-in new program analyses into this
framework.

Location: TUM Garching, Room 03.09.014

[+] 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: Automata-theoretic 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
data-dependent 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
automata-theoretic 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 I-6 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 Diot-Girard (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 One-Encryption Key Exchange

Abstract: We report on a case study of One-Encryption 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
Diffie-Hellman 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 ShortSelf-Contained 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
Kosaraju-Lambert-Mayr-Sacerdote-Tenney 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 non-reachability in
the Presburger arithmetic. In particular, there exists a simple
algorithm for deciding the general VAS reachability problem based on
two semi-algorithms. A first one that tries to prove the reachability
by enumerating finite sequences of actions and a second one that tries
toprove the non-reachability 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 widely-deployed systems that become
heterogeneous and federated. The set of routers incharge of the inter-domain
routing in the Internet is a prime example ofsuch a system. The unanticipated
interaction of nodes under seemingly valid configuration changes and local
fault-handling 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, real-world 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 state-spaces 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 real-world 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:

Term: SS10:

DateTimeTitle

[+] 17.09.2010 14:00 Manuel Fahndrich: Microsoft Research-Vortrag 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 Research-Vortrag an der Informatik-Fakultaet 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
graph-based program representations where instruction selection is NP-hard.

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 Real-Time Systems

Abstract: During the design of software for hard real-time systems, theworst-case 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 real-time system always terminates within given timing constraints.

However, the current state of the art in designing software for hard real-time systems is heavily unsafe. On the one hand, the actual industrial design practice relies on measurements or simulations so that no guarantees about the worst-case timing of a piece of software can be derived. On the other hand, current compilers usually optimize the average-case execution time (ACET) of a program, instead of the WCET. Again, there is no way to derive conclusions about a program's worst-case timing if the program is optimized w.r.t. the ACET.

This talk presents a WCET-aware compiler for hardreal-time 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 worst-case 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 polynomial-space polynomial-delay algorithm for enumerating all minimal feedback vertex sets. As corollary we derive the fastest exponential-time 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 general-purpose 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 multi-threaded programs

Abstract: I will present a proof rule for the verification of temporal safety and liveness properties of multi-threaded programs that facilitates modular reasoning when possible, and provides for non-modular 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
bit-blasting. This approach is entirely automatic, avoids complicated
elimination algorithms,and provides a systematic way of handling
wrap-arounds (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 case-driven development of component- and object based system using Refinement of Component- and Object-base 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 mixed-bag 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 Nelson-Oppen 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:

Term: WS09/10:

DateTimeTitle

[+] 26.03.2010 10:00 King Andy: Automatic Abstraction for Congruences

Abstract: One approach to verifying bit-twiddling 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 low-level 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 bit-level  
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 higher-order 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 MSC-graphs (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 well-structured 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 (non-linear) 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 Durand-Gasselin Antoine: Non-deterministic 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 non-deterministic 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:

Term: SS09:

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 so-called
interference graph that is constructed from the program to compile. Since
graphcoloring is NP-complete and each undirected graph can occur as an
interference graph, register allocation is NP-complete, too.

However, if we require the program to be in static single-assignment 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 non-SSA 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 Real-Valued 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
Parikh-disjoint or Parikh-equivalent. 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: Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads

Abstract: Context-bounded analysis has been shown to be both efficient and effective at finding bugs in concurrent programs. According to its original definition, context-bounded 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 context-bounded 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: Permission-based separation logic for message-passing 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 two-step 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, separation-based reasoning.

Location: Oettingenstrasse 67, Raum Z1.09

Links:

Term: WS08/09:

DateTimeTitle

[+] 26.02.2009 16:00 Friedmann Oliver: A Super-Polynomial 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 long-standing 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 Heap-Manipulating 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 heap-manipulating programs.

The first part of the talk gives a high-level 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), meta-ATP 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 higher-order logic will be introduced.

Location: Garching, room MI 01.11.018

Links:

Term: SS08:

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 Request-Reply-Mechanismus, 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 ASPfun-Kalkuel 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

Term: SS12:

DateTimeTitle

[+] 24.09.2012 09:00 PUMA Workshop 2012 - Goldegg

Abstract:

Location: Goldegg

Term: WS11/12:

DateTimeTitle

[+] 03.10.2011 00:00 PUMA Workshop 2011 - Traunkirchen

Abstract:

Location: Traunkirchen

Term: WS10/11:

DateTimeTitle

[+] 10.10.2010 00:00 PUMA Workshop 2010 - Szentendre

Abstract:

Location: Szentendre

Term: SS10:

DateTimeTitle

[+] 10.07.2010 11:00 TruSoft meets PUMA

Abstract: TrustSoft meets PUMA
----------------------------------

Beg

Location: TUM Garching, 02.07.014

Term: WS09/10:

DateTimeTitle

[+] 04.10.2009 00:00 PUMA Workshop 2009 - Venice

Abstract:

Location: Venice

Term: SS09:

DateTimeTitle

[+] 17.08.2009 00:00 PUMA Sponsored Talks at TPHOL

Abstract:

Location: http://www.novotel.com/gb/hotel-3280-novotel-muenchen-city/index.shtml

[+] 10.07.2009 00:00 PUMA Reading Group

Abstract:

Term: WS08/09:

DateTimeTitle

[+] 13.11.2008 08:00 DTUM workshop

Term: SS08:

DateTimeTitle

[+] 28.09.2008 00:00 PUMA Workshop 2008 - Spitzingsee

Abstract:

Location: Spitzingsee

[+] 08.09.2008 08:00 Workshop light-weight verification

Abstract:

Location: GI Jahrestagung 2008

Ringvorlesung

Term: WS11/12:

DateTimeTitle

[+] 08.02.2012 15:30 Hoder Krystof: Interpolants, Fixed-Points 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 pseudo-boolean
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 Datalog-like 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 first-order
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 linear-time logics, mainly LTL and PSL, and
automata on infinite strings. Branching-time 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 linear-time logics, mainly LTL and PSL, and
automata on infinite strings. Branching-time 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:

Term: SS11:

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 Hoare-logic 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 model-checking, abstract interpretation and
interactive proof. Like model-checking, 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 over-approximate 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

Term: WS10/11:

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

Term: SS10:

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 so-called
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:

Term: WS09/10:

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:

Term: SS09:

DateTimeTitle

[+] 19.05.2009 16:00 Cousot Patrick:

Abstract: tba.

Location: LMU Main Building - A U117

Links: