Program
The program will be composed of 6 tutorials, each of 2:30h duration, and 5 technical talks, each of 1:30h duration.For Printing
pdf versionTutorials

Alessandro Cimatti and Thomas Noll: Safety, Dependability and Performance Analysis of Extended AADL Models
(abstract) (slides : part 1, part 2, part 3, part 4, part 5, part 6, archive) 
Javier Esparza: Unfoldings: A Partial order Approach to Model Checking
(abstract) (slides) 
Hugo Gimbert: Games for Verification and Synthesis
(abstract) (slides : part 1, part 2 : mac) 
Marta Kwiatkowska: Probabilistic model checking
(abstract) (slides : part 1, part 2) 
Kim G. Larsen: Timed automata and their quantitative extensions
(abstract) 
Moshe Y. Vardi: Logic and Verification
(abstract) (slides)
Technical talks

Gilles Barthe: ComputerAided Cryptographic Proofs and Designs
(abstract) (slides) 
Ahmed Bouajjani: Verification of concurrent systems
(abstract) (slides) 
Martin Leucker: Runtime Verification
(abstract) (slides) 
Antoine Miné: Static analysis by abstract interpretation of runtime errors in synchronous and multithreaded embedded C programs
(abstract) (slides) 
Ruzica Piskac: Software Synthesis
(abstract) (slides)
Student session abstracts
 Florent Avellaneda, Checking Two Structural Properties of Vector Addition Systems with States (slides)
 Stanislav Böhm, Kaira: HPC and Petri nets
 Mathieu Caralp, Visibly Pushdown Automata with Multiplicities: Finiteness and KBoundedness (slides)
 Sylvain Cotard, Runtime Verification for RealTime Automotive Embedded Software (slides)
 Aiswarya Cyriac, Model Checking Dynamic Distributed Systems
 Amit Kumar Dhar, Model Checking Flat Counter Systems (slides)
 Maxime Folschette, Inferring Biological Regulatory Networks from Process Hitting models (slides)
 Paulin Fournier, Parameterized verification of networks with many identical probabilistic processes (slides)
 Aleksandra Jovanovic, Implementation of RealTime Systems: Theory and Practice (slides)
 Ahmet Kara, Model Checking Concurrent Systems with Unboundedly Many Processes Using Data Logics (slides)
 Artem Khyzha, Compositional reasoning about concurrent libraries on the axiomatic TSO memory model (slides)
 José António Lopes, Hybrid type systems (slides)
 Laure Millet, Formal Verification of Mobile Robot Protocols (slides)
 Benjamin Monmege, A Probabilistic Kleene Theorem (slides)
 Durica Nikolic, Constraintbased Static Analyses for Java Bytecode Programs (slides)
 Benedikt Nordhoff, TreeRegular Analysis of Parallel Programs with Dynamic Thread Creation and Locks (slides)
 Shashank Pathak, Formal Verification of Agents Learning by Reinforcement (slides)
 Giuseppe Perelli, Recent Results and Future Directions in Strategy Logic (slides)
 Srinivas Pinisetty, Runtime Enforcement of Timed Properties (slides)
 Cesar Rodriguez, Construction and Verification of Unfoldings for Petri Nets with Read Arcs (slides)
 JanThierry Wegener, On Minimality and Equivalence of Petri Nets (slides)
Abstracts
Safety, Dependability and Performance Analysis of Extended AADL Models
Alessandro Cimatti (IRST, Italy) and Thomas Noll (RWTH Aachen University, Germany)
This tutorial presents a componentbased modeling approach to systemsoftware coengineering of realtime embedded systems,
in particular aerospace systems. Our method is centered around the standardized Architecture Analysis and Design Language
(AADL) modeling framework. Taking the core features of AADL and its recent Error Model Annex, we have set up a modeling
framework that supports a variety of system analysis and verification methods. Its major distinguishing aspects are the
possibility to describe hardware and software components and its nominal operations, hybrid (and timing) aspects, as well
as probabilistic faults and their propagation and recovery. Moreover, it supports dynamic (i.e., onthefly) reconfiguration
of components and intercomponent connections. The operational semantics gives a precise interpretation of specifications by
providing a mapping onto networks of eventdata automata. These networks are then subject to different kinds of formal analysis
such as model checking, safety and dependability analysis, and performance evaluation. We demonstrate tool support realizing
these analyses and report on industrial case studies that have been carried out in the context of aerospace systems. The tool
is publicly available.
Unfoldings: A Partial order Approach to Model Checking
Javier Esparza (TU München, Germany)
State space methods are the most popular approach
to the automatic verification of concurrent systems. In their
basic form, these methods explore the transition system associated to the
concurrent system. Loosely speaking, the transition system is a graph having the
reachable states of the system as nodes, and an edge from a state s to another state
s' whenever the system can make a move from s to s'. In the worst case, state
space methods need to explore all nodes and transitions of the transition system.The main problem of transition systems as a basis for state space methods is the wellknown stateexplosion problem. Imagine a concurrent system consisting of n sequential subsystems, communicating in some way, and assume further that each of these subsystems can be in one out of m possible states. The global state of the concurrent system is given by the local states of its components, and so the system may have up to m^n reachable states; in fact, this bound is already reached by the rather uninteresting system in whose components run independently of each other, without communicating at all. So very small concurrent systems may generate very large transition systems. As a consequence, naive state space methods may have huge time and space requirements even for very small and simple systems.
The unfolding method is a technique for alleviating the stateexplosion problem. It uses results of the theory of true concurrency to replace transition systems by special partially ordered graphs. While these graphs contain full information about the reachable states of the system, their nodes are not reachable states themselves. In particular, the number of nodes of the graph does not grow linearly in the number of reachable states.
The goal of the course is to provide a gentle introduction to the basics of the unfolding method, and in particular to introduce an unfoldingbased algorithm for model checking concurrent systems against properties specified as formulas of Linear Temporal Logic (LTL).
The course is based on the book
Javier Esparza and Keijo Heljanko. Unfoldings. A PartialOrder Approach to Model Checking. EATCS Monographs on Theoretical Computer Science. Springer, 2008.
The book is available online (for free) at
http://www7.in.tum.de/~esparza/bookunf.html
It is recommended to download the book and have it available during the course. Some familiarity with Petri nets will be of advantage.
Games for Verification and Synthesis
Hugo Gimbert (LaBRI & CNRS, France)
Game playing is a powerful metaphor that fits many situations in which
interaction between autonomous agents plays a central role. Numerous tasks in
computer science and AI such as design, synthesis, verification, testing, query
evaluation, planning, etc. can be formulated in gametheoretic terms. Viewing them
abstractly as games reveals the underlying algorithmic questions, and helps to clarify the
relationships between problem domains.This talk will illustrate how games can be used in several ways in this context: as algorithmically tractable models of controllable open systems (e.g. games on graphs and stochastic games) as algorithmic tools (e.g. for mucalculus modelchecking) as well as proof tools (e.g. to prove stability under complementation of recognizable set of trees).
Probabilistic model checking
Marta Kwiatkowska (University of Oxford, UK)
Probabilistic model checking is a formal verication technique for
the analysis of systems that exhibit stochastic behaviour. Such behaviour occurs,
for example, due to component failure or randomisation, commonly used as a symmetry
breaker in distributed coordination and communication protocols. The techniques have
been implemented in tools such as PRISM (www.prismmodelchecker.org) and enable a
range of quantitative analyses of probabilistic models against specifications such
as the worstcase probability of failure within 10 seconds or the minimum expected
power consumption over all possible schedulings. This course will give an overview
of probabilistic model checking discretetime Markov chains and Markov decision
processes, explaining the underlying theory and model checking algorithms for temporal
logics such as PCTL and LTL. The material will be illustrated with several case studies
that have been modelled and analysed in PRISM.
Timed Automata and Their Quantitative Extensions
Kim G. Larsen (Aalborg University, Denmark)
Timed automata is by now a wellestablished formalism for modeling and analyzing realtime systems, including realtime controllers, communication protocols. Over the years a number of symbolic techniques have been developed for the efficient analysis of timed automata and with implementation in the tool suite UPPAAL (www.uppaal.{com,org}). The UPPAAL modeling formalism allows for the efficient analysis of safety and (timebounded) liveness properties of networks of interacting timed automata extended with discrete variables, structured and userdefined types as well as userdefined functions. The course will give an overview of the modeling formalism of timed automata and the basic symbolic model checking algorithms. More recently the formalism of timed automata has been extended with continuous observer variables allowing for issues related to e.g energy consumption in embedded systems. The course reviews a number of results for the resulting notion of priced timed automata, including recent results on energybounded infinite runs in the case when energy may both be consumed as well as harvested. Most recently a stochastic semantics of (priced) timed automata has been put forward enabling the expression of performance properties such as the probability of violating a deadline or the expected energy consumption. A range of socalled highly scalable statistical modelchecking techniques have been implemented in UPPAAL, allowing estimation and testing of such performance metrics to be obtained through simulation, where the simulation effort increases with the desired level of confidence. The lecture will contain demonstration of the UPPAAL tool, the new statistical model checking engine as well as several case studies that have been dealt with by the tool.
Logic and Verification
Moshe Y. Vardi (Rice University, USA)
Mathematical logic developed as an attempt to provide formal foundations
for mathematics. The success of that project can be questioned, as the
logical foundations of mathematics proved to be incomplete, possibly
inconsistent, and undecidable. Logic, on the other hand, proved to
be highly successful in providing formal foundations for reasoning about
computing systems, where it is deployed today in industrial tools.
This tutorial will focus on one application of logic to verification,
which is the temporal analysis of systems.
ComputerAided Cryptographic Proofs and Designs
Gilles Barthe (University of Manchester, UK)
EasyCrypt is a tool for constructing and verifying cryptographic
proofs. EasyCrypt can be used as a standalone application, or as
a verifying backend for cryptographic compilers. SyntheCrypt is
a new tool that synthesizes publickey encryption schemes and
generates proofs of security in EasyCrypt.The presentation will outline the languagebased methods that underlie the design of both tools and illustrate some of their applications.
Verification of concurrent systems
Ahmed Bouajjani (LIAFA, Univ. Paris Diderot (Paris 7), France)
The verification of concurrent programs is a challenging problem. This is due to the huge number of orderings in which actions of different threads
can be executed, and to the intricacy of the interactions between these threads (especially in presence of dynamic thread creation, recursion, etc).
Basic problems such as the state reachability problem, that is relevant in checking safety properties, are undecidable in general, even when the
manipulated data are in a finite domain. Therefore, restrictions either on the considered class of program models or on the class of explored
behaviors during the analysis, must be considered in order to obtain decidable and/or tractable analysis problems.In this talk, we will present program models capturing relevant classes of programs (including for instance asynchronous programs) and study the decidability and complexity of their state reachability problem. Moreover, we will present bounded analysis techniques (such as contextbounding) that are used for efficient bug detection in concurrent programs.
Runtime Verification
Martin Leucker (Technische Universität München, Germany)
Starting from a definition of runtime
verification, we develop a taxonomy that explains the different aspects
of runtime verification. We explain the core idea of runtime
verification by showing how monitors can be attached to existing
programs, be used to verify certain aspects of the underlying program as
well as be used to guide the program execution. The main part of the
presentation deals with synthesis techniques that, starting from a high
level correctness specifications, derive suitable monitors
automatically. We start with properties expressed in linear temporal
logic (LTL), first with a semantics on finite traces and then extended
to a semantics over infinite traces.
Static analysis by abstract interpretation of runtime errors in synchronous and multithreaded embedded C programs
Antoine Miné (CNRS, ENS, France)
In the realm of embedded critical systems, it is crucial to guarantee the
correctness of programs before they are deployed.
We present semanticbased two static analyzers developed in our research group
to help addressing this need: Astrée focuses on synchronous controlcommand
software in C; its extension AstréeA analyzes multithreaded embedded C
software. These analyzers detect statically (at compile time) all the
arithmetic and memory runtime errors in the program. They are based on
abstract interpretation, a general theory of the approximation of program
semantics that ensures soundness: the analyzers cannot miss any threat. They
may however output false alarms. We show how specializing Astrée with novel
abstractions allowed us to reach the zero false alarm goal (that is, a proof
of absence of runtime error) on some industrial avionic applications.
Software Synthesis
Ruzica Piskac (Max Planck Institute for Software Systems, Germany)
Software synthesis is a technique for automatically generating code given a specification. The goal of software synthesis is to make coding easier while increasing both the productivity of the programmer and the correctness of the produced code.In this talk we describe an approach to synthesis that relies on the use of automated reasoning and decision procedures. The complex specifications are handled by employing efficient algorithms for reasoning about the domain of the specification. We show how to generalize some decision procedures into predictable and complete synthesis procedures. Here completeness means that the procedure is guaranteed to find code that satisfies the given specification. Moreover, code produced this way is correct by construction. The synthesis procedure also outputs preconditions on input values that guarantee the existence of the output values.
In addition, we also outline a synthesis procedure for specifications given in the form of type constraints. The procedure takes into account polymorphic type constraints as well as code behavior and derives code snippets that use given library functions. The constraints can have multiple solutions and hence more than one code snippet can be a good candidate. We use an additional weight function to rank the derived snippets.
The tools implementing these synthesis algorithms are publicly available.