We investigate the algorithmic feasibility of checking whether concurrent

implementations of shared-memory objects adhere to their given sequential
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

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
detectable by considering very few conflict edges or barriers.

(Joint work with Constantin Enea, Michael Emmi, and Jad Hamza. Published in ESOP'13.)

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 examples and 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.

We consider the model-checking problem for data multi- pushdown automata (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 is a joint work with Benedikt Bollig, Paul Gastin and K. Narayan Kumar.

http://www.lsv.ens-cachan.fr/~cyriac/

We introduce negotiations, a model of concurrency close to Petri nets, with multiparty negotiation as primitive. We study two problems: soundness of negotiations (close to deadlock freedom), and the problem of, given a negotiation with possibly many steps,
computing a summary, i.e., an equivalent one-step negotiation.

We provide a complete set of reduction rules for acyclic, weakly deterministic negotiations and show that, in the case of deterministic negotiations, the rules compute the summary in polynomial time.

We characterize the complexity of the safety verification problem forparameterized systems consisting of a leader process and arbitrarily manyanonymous 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 verification problem whenprocesses are modeled by finite-state machines, pushdown machines, andTuring machines. Our proofs use combinatorial characterizations ofcomputations in the model, and in case of pushdown-systems, some novellanguage-theoretic constructions of independent interest.

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 memory model 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 concept is that of cube extrapolation: it successfully avoids exponential state explosion when abstracting PM . We implemented our approach for the x86 TSO and PSO memory models and showed that predicates discovered via extrapolation are powerful enough to verify several challenging concurrent programs. We show that our cube extrapolation method is enabling verification of additional programs. This is the first time some of these programs have been verified for a model as relaxed as PSO.

Joint work with Yuri Meshman, Martin Vechev and Eran Yahav.

Bio: Andrei Dan is a PhD student at ETH Zurich where his adviser is Prof. Martin Vechev. Previously he obtained a M.Sc. degree from EPFL. His interests are in program analysis, verification and concurrency.

We study the complexity of the Linear Ranking problem: given a loop,

described by linear constraints over a finite set of integer
variables, is there a linear ranking function for this loop? While
existence of such a function implies termination, this problem is not
equivalent to 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 special cases of importance of PTIME complexity. We
also present complete algorithms for synthesizing linear ranking

(joint work with Amir M. Ben-Amram)

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

This talk presents a predicate refinement approach that is
complete for the quantifier-free theory of linear real arithmetic
with uninterpreted functions and arrays, extending the previous
state of the art on complete predicate refinement which was only
complete for more limited theories. Our approach is
template-based, inspired by the work 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.

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 that Craig interpolants mined from unsatisfiability proofs can
be used as "guesses" for inductive invariants (correctness proofs). In
this talk, I will describe 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 the UFO framework, an
open-source C verification framework we built in the LLVM compiler
infrastructure. This is joint work with Arie Gurfinkel (SEI, CMU) and

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 be analyzed by aspects — as well as being simultaneously applicable in concurrent threads. Therefore the problem of reachability of various states of a system becomes much more challenging. This is important since ensuring that a system does not contain errors is often equivalent to proving that some 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 primarily used for analysis of recursive programs, we are able to adapt them to fit this new context.

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- lating programming guidelines or “best practices”.

In this paper, we study the concrete example of a guideline used at SAP for the handling of untrusted, potentially executable strings that are embedded in the output of a Java 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.

We consider two-player games played on finite graphs with costs on edges

and introduce two wining conditions, cost-parity and cost-Streett, which

For cost-parity games we show that the first player has positional winning
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.

Deciding equivalence of probabilistic automata is a key problem for

establishing various behavioural and anonymity properties of probabilistic
systems. In particular, it is at the heart of the tool APEX, an analyser
for probabilistic programs. APEX is based on game semantics and analyses a
broad range of anonymity and termination properties of randomised

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 on costs, 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.

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 where each transition is
labeled by a
vector of resource updates, where every update is a non-positive number or
omega. The omega updates model the reloading of a given resource. Each
vertex
belongs either to player Box or player 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 are computationally hard in general, they are solvable in
polynomial
time for every fixed number of resource types (i.e., the dimension of
the update

This is a joint work with Krishnendu Chatterjee, Antonin Kucera and
Petr Novotny.

In the area of probabilistic verification and performance evaluation, the behavior of

real-life systems such as queues, assembly lines or 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 fixed delay. Disproving several previous results, we
show that such GSMP can exhibit a surprisingly unstable behavior in the long-run.
The instability is 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

Fluid (or mean-field) techniques, rooted in statistical mechanics and physical chemistry, provide accurate deterministic approximations to massive-scale Markov chain models of interacting agents. The original discrete-state model is properly scaled in such a way that it converges to the 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 informatics within the context of a stochastic process algebra, as a means to dealing with 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 composite processes 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 of composite 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 discuss ongoing work which is pushing the limits of differential aggregations. I will 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.

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"
with restricted 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 in general 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 used to improve existing techniques such as partial
order reduction.

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 to reason about these. In this way, we have built a contract
checker for Haskell programs, an automated induction tool for Haskell
programs, and an automated counter example finder for Haskell
programs. I will discuss successes and challenges; all this is ongoing

This is joint work with the automated reasoning group at Chalmers:
Nick Smallbone, Moa Johansson, Dan Rosen, and myself; and the Haskell
group at Microsoft Research: Dimitrios Vytiniotis and Simon
Peyton-Jones.

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

equations by means of the heuristic of strategy (or: policy) iteration
is studied specifically for games related to verification problems
like simple stochastic games, mean-payoff games, or parity games.

Solving these games means solving a system of equations. Often

solving this system directly is not possible. Strategy iteraiton
reduces the problem of solving the original system to that of a
sequence of simpler equation systems. Here "simpler" means that these
systems can be considered to be linear w.r.t. a suitable algebraic
structure thereby becoming amenable for GPU computing.

In this talk, I will discuss my progress at implementing a GPU based

solver for parity games including the difficulties encountered so

I will be presenting our work on a Isabelle/HOL library with a generic type class implementation of separation algebra based on the formulation by Calcagno et al. Our library features the basic separation logic concepts developed on top of the separation algebra, and contains automated tactic support that can be used directly for any instantiation of the library.

We propose a logic of interactive proofs as the first and main step towards an intuitionistic foundation for interactive computation to be obtained via an interactive analog of the G\"odel-Kolmogorov-Art\"emov definition of intuitionistic logic as embedded into a classical modal logic of proofs, and of the Curry-Howard isomorphism between intuitionistic proofs and typed programs. Our interactive proofs effectuate a persistent epistemic impact in their intended communities of peer reviewers that consists in the induction of the (propositional) knowledge of their proof goal by means of the (individual) knowledge of the proof with the interpreting reviewer. 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 other words, 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.

Coercions allow to convert between different types, and their automatic

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
the standard 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

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
broadband communication 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 a result, protocol errors and
limitations are still found many years after the 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. The overall goal is to reduce the
``time-to-market'' for better (new or modified) WMN protocols, and to

In this talk I describe the importance of WMNs and present one of the
leading protocols: the Ad-hoc on Demand Distance Vector (AODV) routing
protocol.
Moreover, I give an overview over formal methods used so far to model,
analyse and verify AODV.
This includes a formal model using process algebra, fully automation by
a matrix model and the use of model checkers.
In an outlook I present some problems we are faced and discuss ongoing
and future work. The latter includes a formal
model of process algebra in Isabelle/HOL/.

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. Since Ong'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

Another way of looking at the problem 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 can define a natural class of automata recognising sets of CPDA
configurations that provide a way to represent a solution to the global mu-
calculus model-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 be able to inform each other.

Type abstraction and intensional type analysis are features seemingly at

odds -- type abstraction is intended to guarantee parametricity and
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 may safely be used as a dynamic representative of the abstract type for

But does dynamic type generation provide us with the same kinds of
abstraction guarantees that we get from parametric polymorphism? To give an
answer to that question, we definene a step-indexed Kripke 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, and vice 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.

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
recursion of degree d, such that for rewrite systems in this class we
obtain that the runtime complexity lies in O(n^d). We show that
predicative recursive rewrite systems of degree d define functions
computable on a register machine in time O(n^d). This result emphasises
the fact that (innermost) runtime complexity of a rewrite system is an

In the past decade, static validation of software systems has made 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

Andreas Zeller is a full professor for Software Engineering at Saarland
University in Saarbrücken, Germany. His research concerns the analysis of large
software systems and their development process; his students are funded by
companies like Google, 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.

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
transaction of 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 for checking 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

Joint work with David Basin, Matus Harvan, Samuel Mueller, and
Eugen Zalinescu.

A large fraction of an XML document typically

consists of text data. 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. Most
queries, however, are hybrid: they contain parts which query
the text of the document, and contain other parts which query
the tree structure of the document. It is therefore a challenge
to appropriately choose a query evaluation order which optimally
leverages the execution speeds of the text and tree indexes.
Here the SXSI system is introduced. It stores the tree
structure of an XML document using a bit array of opening
and closing brackets plus a sequence of labels, and stores
the text nodes of the document using a global compressed
self-index. On top of these indexes sits an XPath query en-
gine that is based on tree automata. The engine uses fast
counting queries on the text index in order to determine
whether to evaluate top-down or bottom-up with respect to
the tree structure. The resulting system has several advantages
over existing systems: (1) on pure tree queries (without
text search) such as the XPathMark queries, the SXSI
system performs on par or better than the fastest known systems
MonetDB and Qizx, and (2) on queries that use text
search, SXSI outperforms the existing systems by 1-3 orders
ders of magnitude (depending on the size of the result set),
and (3) for all tested data and queries, SXSI's memory consumption

The engineering process of on-board critical embedded systems involves a wide range of diverse approaches and techniques for system-level aspects 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-purpose modeling and specification formalism based on AADL, enriched with a
rich palette of formal analysis techniques for all properties and measures of interest. It is supported by an advanced toolset which is centered around state-of-the-art symbolic and stochastic model checking. We present our AADL 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 funded by the European Space Agency.)

Büchi Automata are an automaton model for describing infinite languages.

Despite its similarities to finite automata determinisation is not
always possible in this model and no canonical minimization algorithm

This work describes SAT-based minimization procedure for nondeterministic Büchi 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 sense that 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 for given 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
and two-letter alphabet as well as some instances of Michel's NBA
which were introduced to establish an n!
lower bound on complementation of NBA.

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 algorithms that the proofs of these theorems yield. For one of
Glivenko's classes of such sequents, we can give an algorithm of
quadratic runtime, provided it is in long normal form and given in a
slightly weaker version of classical logic. This is of interest for

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 to automatically identify
code as free from vulnerabilities and to address the 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
and then 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

Disjunctive well-foundedness (used in Terminator), size-change termination, 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. At the 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 to highlight 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 present some Ramsey-like arguments: Though similar proofs are typically classical, we offer an entirely constructive development standing on the shoulders of Veldman and Bezem, and Richman and Stolzenberg.

by Dimitrios Vytiniotis, MSR Cambridge

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 of a 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

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 the expressiveness 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

As time goes by, it becomes more and more apparent that the puzzles of life involve more and more molecular pieces that fit together in increasingly complex ways. Biology is not an exact science. It is messy and noisy, and most often vague and ambiguous. We cannot assign clear rules to 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. At the same time, this 'new wave of the future' forces computer science to stretch far and beyond, and in ways never considered before, in order to deal with the enormous complexity observed in biology. In this talk, I will summarize some of the success stories in using formal verification to reason about mechanistic models in biology. In particular, I will focus on models of cell fate decisions during development and cancer, and their analysis using model checking.

A primary feature of a computer program is its quantitative

performance characteristics: the amount of resources such as time,
memory, and power the program needs to perform its task. Concrete
resource bounds for specific hardware have many important applications
in software development but their manual determination is tedious and

This dissertation studies the problem of automatically determining
concrete worst-case bounds on the quantitative resource consumption of
functional programs.

Traditionally, automatic resource analyses are based on recurrence
relations. The difficulty of both extracting and solving recurrence
relations has led to the development of type-based resource analyses
that are compositional, modular, and formally verifiable. However,
existing automatic analyses based on amortization or sized types can
only compute bounds that are linear in the sizes of the arguments of a
function.

This work presents a novel type system that derives polynomial resource
bounds from first-order functional programs. As pioneered by Hofmann
and Jost for linear bounds, it relies on the potential method of
amortized analysis. Types are annotated with multivariate resource
polynomials, a rich class of functions that generalize non-negative
linear combinations of binomial coefficients. The main theorem states
that type derivations establish resource bounds that are sound with
respect to the resource-consumption of programs which is formalized by a
big-step operational semantics.

Simple local type rules allow for an efficient inference algorithm for
the type annotations which relies on linear constraint solving only.
This gives rise to an analysis system that is fully automatic if a
maximal degree of the bounding polynomials is given. The analysis is
generic in the resource of interest and can derive bounds on time and
space usage. The bounds are naturally closed under composition and
eventually summarized in closed, easily understood formulas.

The practicability of this automatic amortized analysis is verified with
a publicly available implementation and a reproducible experimental
evaluation. The experiments with a wide range of examples from
functional programming show that the inference of the bounds only takes
a couple of seconds in most cases. The derived heap-space and
evaluation-step bounds are compared with the measured worst-case
behavior of the programs. Most bounds are asymptotically tight, and the
constant factors are close or even identical to the optimal ones.

For the first time we are able to automatically and precisely analyze
the resource consumption of involved programs such as quick sort for
lists of lists, longest common subsequence via dynamic programming, and
multiplication of a list of matrices with different, fitting dimensions.

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. The efficient 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 we present 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 that preserves

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, and abstracting the behavioural effect into a

Symbolic systems biology (SSB) is an approach to computational modeling of biological

systems that builds on logical representations and uses 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

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, and find and compare pathways satisfying different constraints.

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 vocabulary and semantics of service
behaviours abstract. A privacy-compliant data-handling protocol for a network

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 a case-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

In recent work we have found new approaches to the old problem of 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.

tba.

I shall present an algorithm for existential quantifier elimination using incremental SAT solving. This approach contrasts with existing techniques 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 onto a quantifier-free formula presented in CNF.

This is joint work with Joerg Brauer and Jael Kriener.

joint work with Ahmed Bouajjani (LIAFA) and Eike Möhlmann (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.

VeriFast is a verifier for single-threaded and multithreaded C and Java programs annotated with preconditions and postconditions written in 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 terminate and 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 kernel modules, and JavaCard programs.

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

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 techniques do not provide end-to-end security
guarantees, since they focus on the logic of the protocol and tend to

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
granted only to authorized users; on the other hand, these users would
like to share as little personal information as possible with third
parties.

I will 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.

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 results in 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 software.

• For more information, please see:
  

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 graph algorithm 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

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 specific for 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. Such classes 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.

Several successful software model checkers are based on a technique called

single-block encoding (SBE), which computes costly predicate abstractions 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 the fundamental properties of the analysis, and makes the
differences of the variants more explicit. Adjustable-block encoding (ABE) is
implemented as 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

With the subprime crisis of 2007 it became clear that financial institutions have to steer their risks with sophisticated methods on the basis 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 to face the challenges of modern banking.

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
applications tend 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 our recent 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
relevant to 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 its expressiveness and analysis

This talk is based on joint work with PS Thiagarajan from the National
University of Singapore, and Linh T.X. Phan and Insup Lee from the
University of Pennsylvania.

Bio:
Samarjit Chakraborty is a Professor of Electrical Engineering at the
Technical University of Munich, where he heads the Institute for
Real-Time Computer Systems. He obtained his Ph.D. in Electrical and
Computer Engineering from ETH Zurich in 2003. Prior to joining TU
Munich, from 2003 -- 2008 he was an Assistant Professor of Computer
Science at the National University of Singapore. His research
interests are primarily in system-level power/performance analysis of
real-time and embedded systems.

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)

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.

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 by Bresson et al
(CCS'03), with the help of the automatic, computationally sound prover
CryptoVerif, which provides additional confidence that the proof 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 that rely on Shoup's lemma. They also
include additional game transformations that insert case distinctions manually
or merge cases that no longer need to be distinguished. Eventually, the
computation of the probability bounds for attacks has also been improved,

(joint work with David Pointcheval)

The reachability problem for Vector Addition Systems (VASs) is a

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 from an initial one if and only
if there exists a Presburger inductive invariant that contains the
initial configuration but not the final one. Since we can decide if a
Preburger formula denotes an inductive invariant, we deduce 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
to prove 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 of production relations inspired from Hauschildt that

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 checking: first, to
underapproximate the reachable state space of multithreaded procedural programs
and second, to underapproximate the reachable state space of counter machines.
In particular, we show that verification with bounded languages generalizes
context-bounded reachability for multithreaded programs.

We also show a new and constructive proof of the following language-theoretic
result: for every context-free language L, there is a bounded context-free
language L' which is a subset of L and has the same Parikh image as L.

(Joint work with Pierre Ganty and Benjamin Monmege

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 in charge of the inter-domain
routing in the Internet is a prime example of such 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 emergent behavior resulting from a local session
reset.

We argue that the key step 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 Jovanovic, Gautam Kumar, Boris Spasojevic,
and Olivier Crameri

Bio:

Dejan Kosti? obtained his Ph.D. in Computer Science at the Duke University,
under Amin Vahdat. He spent the last two years of his studies and a brief stay
as a postdoctoral scholar at the University of California, San Diego. He
received his Master of Science degree in Computer Science from the University
of Texas at Dallas, and his Bachelor of Science degree in Computer Engineering
and Information Technology from the University of Belgrade (ETF), Serbia. In
January 2006, he started as a tenure-track assistant professor at the School of
Computer and Communications Sciences at EPFL (Ecole Polytechnique Fédérale de
Lausanne), Switzerland. In 2010, he received a European Research Council (ERC)
Starting Investigator Award. His interests include Distributed Systems,
Computer Networks, Operating Systems, and Mobile Computing.

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 will give a high-level presentation of Holfoot (http://holfoot.heap-of-problems.org).

Smallfoot (http://www.dcs.qmul.ac.uk/research/logic/theory/projects/smallfoot) is an automated separation logic tool. It is able to reason about the partial correctness of programs written in a simple, low-level imperative language, which is designed to resemble C. This language contains pointers, local and global variables, dynamic memory allocation/deallocation, conditional execution, while-loops and recursive procedures with call-by-value and call-by-reference arguments. Moreover, concurrency is supported by conditional critical regions and a parallel composition operator. Smallfoot-specifications are concerned with the shape of datastructures in memory. Their content is not considered.

Holfoot can verify most Smallfoot examples completely automatically. However, it extends Smallfoot to reason about the content of datastructures. Moreover, there is support for arrays and pointer arithmetic. Considering the data-content allows Holfoot to reason about fully-functional specifications. Simple fully-functional specifications like reversal of a single linked list can be verified automatically. For more complicated examples like a fully-functional specification of mergesort or insertion into a red-black-tree, Holfoot can be used interactively inside HOL4. This allows using all the libraries and tools of HOL4.

This talk will be a high-level presentation of Holfoot. I don't expect the audience to be familiar with separation logic or HOL4. The talk will briefly sketch the semantic foundations, i.e. Abstract Separation Logic. Then, an end-user view on Holfoot will be presented. Holfoot's web-interface (http://holfoot.heap-of-problems.org/web-interface.php) will be used to run Holfoot on concrete examples. I will also briefly demonstrate, how to use Holfoot interactively inside the HOL4 theorem prover to tackle more complicated specifications.

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 applied to 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, we also analysed authentication routines in the Secure Remote Password suite and of a Internet Message Support Protocol implementation. Our technique shows when there is unacceptable leakage; the same technique is also used to verify, for the first time, that the applied software patches indeed plug the information leaks. This is the first demonstration of quantitative information flow addressing security concerns of real-world industrial programs.

Im Zuge immer komplexerer und umfangreicherer Softwareentwicklungsprojekte wird es zunehmend wichtiger, entwickelte Software von Anfang an umfangreich und effektiv zu testen, um ein qualitativ hochwertiges Produkt herzustellen. Kunden erwarten Software mit einem großen Funktionsumfang und Komponenten, die optimal aufeinander abgestimmt sind und die dabei noch ein Höchstmaß an Sicherheit bietet.
Die Förderinitiative 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 Software Contracts. 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 können. Der Research-Vortrag an der Informatik-Fakultät der Technischen Universität München, Boltzmannstraße 3, Hörsaal 2, 14:00 Uhr steht für alle Interessierten offen. Auf Grund einer begrenzten Anzahl an Sitzplätzen werden Teilnehmer gebeten, sich online auf http://de.amiando.com/mspclousout.html anzumelden.

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, rely on

In this talk we present a formulation of instruction selection by PBQP and
show how the resulting instances occurring in practice can be solved efficiently.

During the design of software for hard real-time systems, the worst-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 hard real-time systems. By tightly coupling the compiler with a tool for static WCET analysis, it is possible for the very first time to integrate a formal WCET timing model into a compiler. This WCET timing model provides the compiler with valuable data about the worst-case behavior of a program to be 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 focus in particular on the memory hierarchy of embedded processors: register allocation and scratchpad memory allocation.

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 work with Serge Gaspers, Universidad de Chile)

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 a classical nondeterministic automaton
in which each transition carries a weight 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;

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 automata model
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).

1) L4.verified: An Overview

The L4.verified project, demonstrating the functional correctness of the
seL4 microkernel, was recently completed by NICTA. This makes seL4 the
world's first verified general-purpose operating system kernel, and
marks a significant step forward in the application of formal methods to
system software. In this talk I will give an overview of the project,
including an introduction to the various specifications of seL4's
behaviour used in the project and an outline the methodology used in
proving refinement between them. I will conclude by 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 proof
effort: that of demonstrating that monadic models of the system respect
certain invariants. While both invariant proofs and the Hoare Logic we
use have been well studied, a number of original challenges arise in our
specific environment. These include handling of large databases of Hoare
rules, addressing recursive functions, and managing the boundary between
user-driven and interactive proof within the Isabelle/HOL proof
environment. I will conclude with some thoughts about how proof
automation might better serve such large projects in the future.

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

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.

Traditionally, transfer functions have been manually designed for each

operation in a program. Recently, however, there has been growing
interest in computing transfer functions, motivated by the desire to

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 overflows and underflows) which arise in
machine arithmetic.

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 procedure for a fragment of a theory of asymptotic "big O" equations. Next, I will discuss Nelson-Oppen combination methods in the context of theories of the real 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).

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, and it generate verifiable code from design models.
We also report on a recent project of integrating Runtime Verification into the software engineering process.

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 the large 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 decoupled into two parts: (1) a SAT-
based abstraction (compilation) step which can be automated, and (2)  
an interpretation step that requires no SAT-solving. We exploit  
triangular matrix forms to derive transfer functions efficiently,  
even in the presence of large numbers of bits. Finally we propose  

We investigate the following question. Given a higher-order SML function

                    F : (int->int) -> int

how can we rigorously specify that F is pure, ie produces no side-effects
other than those arising from calling its functional argument.
(If you don't like higher-order SML functions think of F as a method that
may invoke a library function. It should produce no side-effects other
than those that might arise from calls to the library function.)

We show that existing methods based on preservation of invariants and
relational parametricity are insufficient for this purpose and thus define
a new notion that captures purity in the sense that for any functional F
that is pure in this sense there exists a corresponding question-answer
strategy, ie an element of the datatype

type tree = Answer of int | Question of int * (int -> tree)

This work is motivated by the ongoing effort to verify a new fixpoint
algorithm by Helmut Seidl which takes such a functional as input (or
rather a functional of type ((Variables->Domain)->(Variables->Domain)) and
whose correctness is contingent on this functional to be pure.

Message Sequence Charts (MSCs) provide an intuitive notation of communication 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 and reliability, 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.

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 is because 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 static constraint generation with information obtained
from static abstract interpretation and dynamic execution of the
program. The strengthening comes in 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.

The use of automata to decide Presburger Arithmetic (PA) has been

introduced by Büchi in 1960. Henceforth we represent PA's formula by the
(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

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 states of the minimal
deterministic finite automaton and of the canonical RSFA, for some
simple fragments of PA.

tba.

tba.

Register allocation is one of the most important optimizations in a modern

compiler. It maps the variables of a program to the processor's registers in

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
graph coloring 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 deficiencies of traditional
register allocators.

Logical formulas involving special functions such as ln, exp and sin can

be proved automatically by MetiTarski: a resolution theorem prover
modified to call a decision procedure for the theory of real closed
fields. (This theory in particular includes the real numbers with
addition, subtraction and multiplication.) Special functions are
approximated by upper and lower bounds, which are typically ratios of
polynomials. The decision procedure simplifies clauses by deleting
literals that are inconsistent with other algebraic facts; the net
effect is to split the problem into numerous cases, each covered by a
different approximation, and to prove them individually. MetiTarski
simplifies arithmetic expressions by conversion to a recursive
representation, followed by flattening of nested quotients. It can solve
many difficult problems found in mathematics reference works, and it can

One of the fundamental connections between logic and automata was

established by Buechi in the 60's: Monadic Second-Order (MSO) logic over
strings has precisely the same expressiveness as finite-state automata.
Thus, we can use the theory of finite automata to give new decidability
results for MSO logic!
This result was later generalized to trees: MSO logic over two
successors (i.e., over trees) has the same expressiveness as
finite-state tree automata.
In the early 90's, Courcelle and others found a way to use MSO logic
for the specification of translations, rather than for sets of objects
(string, trees, or graphs). The key idea is to use formulas with
one and two free variables in order to define the nodes and edges
of the output object, respectively. The interpretation of these formulas
on a given input object (graph) generates a translated output
graph. If the input and output graphs are trees, then the resulting
formalism specifies a tree translation.
The question arose whether there exists an appropriate generalization
of Buechi's result to tree translations: is there a class of
finite-state tree transducers that has precisely the same
expressivness as the MSO definable tree translations?
In this talk we discuss the answer to this question, and show
that particular tree transducers, called macro tree transducers,
when restricted to linear size increase, precisely characterize
the MSO definable tree translations.
We also show important properties of MSO definable tree translations
and how they can be proved very shortly and elegantly. Through the
above equivalence to finite-state tree transducers, such properties
have helped to identify important new properties of tree transducers
(which were too difficult to reason about without the connection
to MSO logic); thus, we point out the usefulness of MSO logic over

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

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 for programs with dynamic thread creation. The idea is to bound the number of context 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 analysis induced by them.

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
concurrent processes are first analysed for confluent behaviour using
a type and effect system which provides a foundation for establishing

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 the algorithm requires exponentially many strategy iterations, answering in the 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.

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 recent contributions: separation logic yields concise specifications and can be used for interactive functional verification, while decidable fragments apply to the automatic verification of safety properties. Burstall's split heap approach, on the other hand, supports record-based data structures and enables the application of existing automated reasoning techniques.

The second part sketches the speaker's approach, lightweight separation. It supports reasoning about memory layouts by specialized tactics, but uses classical HOL for assertions, such that reasoning about them can rely on the automation already available in Isabelle.

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 Derivation Viewer (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 through the SystemOnTPTP web service, and applications in various domains. Current work extending the TPTP to higher-order logic will be introduced.

Im Zeitalter des Internet muss sich das verteilte Rechnen mit asynchronen parallelen Aktivitäten, Codeverteilung und komplexen Aufrufstrukturen auseinandersetzen. Wir stellen in diesem Vortrag den Kalkül ASPfun für funktionale, aktive Objekte vor. ASPfun erweitert die Theorie der Objekte um eine Kommunikation mit einem Request-Reply-Mechanismus, basierend auf sogenannten Futures. Futures repraesentieren erwartete Antworten von 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.

Im Vortrag wird der aktuelle Algorithmus zur Lösung schwerer

Rucksackinstanzen von Howgrave-Graham und Joux aus dem Jahr 2009
vorgestellt. Dies geschieht unter Zuhilfenahme der
Vorgängeralgorithmen von Schroeppel und Shamir (1981) beziehungsweise
Horowitz und Sahni (1974). Der aktuelle Algorithmus ist, im Gegensatz
zu den beiden Vorgängern, randomisiert und verwendet eine Heuristik.
Der Fokus soll nicht auf der Korrektheit der Heuristik liegen, sondern
auf der Kernidee hinter dem neuen Ansatz, der sogenannten
Repräsentationstechnik. Außerdem liefert dieser Algorithmus einen
Tradeoff zwischen Speicher und Zeit. Im Vortrag wird gezeigt, wie

TrustSoft meets PUMA
----------------------------------

Begin: 11:00

*** 2 talks before lunch:

1. Sven Linker:
"Diagrammatic Specification of Mobile Real-Time Systems"

2. Nils Müllner:
"Unmasking Fault Tolerance:
Masking vs. Non-masking Fault-tolerant Systems"

----------------------------------

Lunch: 12:30 - 13:30

----------------------------------

*** 2 talks after lunch

3. Mani Swaminathan:
"Layered Design of Data-Enriched Real-Time Systems"

4. Tino Teige:
"Stochastic Satisfiability-Based Analysis of
Probabilistic Hybrid Systems"

---------------------------------

Coffee break: 15:30 - 16:00

---------------------------------

***  talks after coffee break by TUM:

Javier Esparza:
"Complexity of Pattern-based Verification of Concurrent Programs"

Tobias Nipkow:
"Sledgehammer: Judgement Day"

One more talk on verification: TBA

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

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

The purpose of this tutorial is to introduce temporal logics as formal languages

for the specification and verification of programs. We will 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 a broad
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 will be covered in the second part

The purpose of this tutorial is to introduce temporal logics as formal languages

for the specification and verification of programs. We will 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 a broad
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 will be covered in the second part

When compiling users queries into imperative execution plans, query optimizers

use a wide range of optimization techniques to speed up the resulting plan.
Join queries are a particular interesting class of queries, as they are

When compiling users queries into imperative execution plans, query optimizers

use a wide range of optimization techniques to speed up the resulting plan.
Join queries are a particular interesting class of queries, as they are

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

I will present Tree Automata Completion which is a verification technique 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 the programs. In this setting, proving
safety properties on programs consists in showing that "bad" program states,
violating the property, are not recognized by the tree automaton, i.e. are

To construct this 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 given by hand.

In the first talk, entitled:

Reachability Analysis of Rewriting using Tree Automata Completion

I will briefly recall the notions of term rewriting systems, tree automata, and
define the reachability analysis problem for term rewriting systems. I will
recall some of the classes of term rewriting systems for which this problem is
known to be decidable. Then, I will define the tree automata completion
algorithm and bound the set of decidable classes that it covers. Finally, I
will briefly recall the equational abstraction framework and show how it can be
adapted to tree automata completion. This talk is likely to contain (short)
demos.

In the second talk, entitled:

Tree Automata Completion, for real

I will restart from the end of the previous talk and give more details about the
completion algorithm that is actually used in the Timbuk tool. First, I will
relate tree automata completion with the rewriting modulo framework in order to
justify the evolution of the algorithm. Then, using the two applications we
experimented with (verification of cryptographic protocols and Java bytecode
program analysis), I will comment on the choices we made w.r.t. non left-linear
rewriting systems and on the future developments.

Plans for Flow Logic for Process Calculi at TUM (January 2011)

By HYPERLINK "http://www.imm.dtu.dk/~nielson" Flemming Nielson.

Motivation:

Flow Logic is an approach to statically determining the behaviour of programs and processes. It borrows methods and techniques from Abstract Interpretation, Data Flow Analysis and Constraint Based Analysis while presenting the analysis in a style more reminiscent of Type Systems. Traditionally developed for programming languages, this course provides a tutorial development of the approach of Flow Logic for process calculi based on a decade of research.

We develop a simple analysis for the pi-calculus; this consists of the specification, semantic soundness (in the form of subject reduction and adequacy results), and a Moore Family result showing that a least solution always exists, as well as providing insights on how to implement the analysis.

We next show how to strengthen the analysis technology by introducing reachability components, interaction points, localised environments and, finally, we extend it to a relational analysis.

Finally we clarify that Flow Logic is a program logic -- in the same sense that a Hoare's logic is.

Lectures:

January 18: [FL-paper] Section 1, 2: The Basics of Flow Logic.

January 19: [FL-paper] Section 3: Extending the Analysis Technology.

January 20: [FL-paper] Section 4, 5: Flow Logic as a Program Logic.

Lecture Materials:

[FL-paper] Hanne Riis Nielson, Flemming Nielson, Henrik Pilegaard: Flow Logic for Process Calculi. Accepted for ACM Computing Surveys.

[FL-slides] Hanne Riis Nielson, Flemming Nielson, Henrik Pilegaard: Flow Logic for Process Calculi. Slides.

19.01.2010 - 16:00

09.07.2010 - 08:30

The abstract domain of polyhedra is su?ciently expressive

to be deployed in veri?cation. One consequence of the richness of this
domain is that long, possibly in?nite, sequences of polyhedra can arise
in the analysis of loops. Widening and narrowing have been proposed to
infer a single 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
landmarks hint 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,

SAT, SMT, Resolution, Completion, Superposition

Superposition(Theorie), Superposition(Induction),

SAT, SMT, Resolution, Completion, Superposition

Superposition(Theorie), Superposition(Induction),

16.12.2010 - 16:00 17.12.2010 - 09:00 17.12.2010 - 10:30 18.12.2010 - 14:30

tba.