The summer school on verification technology, systems & applications takes place at the Max Planck Institute for Informatics at Saarbrücken, Germany from July 31 - August 4, 2017. We believe that all three aspects verification technology, systems & applications strongly depend on each other and that progress in the area of formal analysis and verification can only be made if all three aspects are considered as a whole. Our five speakers Rajeev Alur, Christel Baier, Hoon Hong, Andrew Reynolds and Thomas Wies stand for this view in that they represent and will present a particular verification technology and its implementation in a system in order to successfully apply the approach to real world verification problems
The number of participants in the school is limited to 40. We expect participants to hold a bachelor (or higher) degree in computer science (or equivalent) and to have basic knowledge in propositional and first-order logic
The summer school is free of charge. It includes the lectures, daily coffee breaks and lunches and the special summer school dinner on Wednesday. Participants take travel, accommodation and daily living costs on their own. There is a limited number of free shared rooms on campus available for distribution by the selection committee. Please express your interest with your application. Recommendations on hotels can be found below.
The registration will be open to accepted applicants starting on June 19, 2017. Registration links have been send via eMail.
Lectures on Monday, Tuesday, Thursday and Friday will take place in room 029 (Building E1 5). Lectures on Wednesday will take place in room 002 (Building E1 5).
| July 31 Monday |
August 1 Tuesday |
August 2 Wednesday |
August 3 Thursday |
August 4 Friday |
|
|---|---|---|---|---|---|
| 8.00 | Registration | ||||
| 8.45 | Welcome | ||||
| 9.00-12.30 | Christel Baier | Christel Baier | Hoon Hong | Andrew Reynolds | Thomas Wies |
| 12.30-14.00 | Lunch break | ||||
| 14.00-17.30 | Rajeev Alur | Andrew Reynolds | Rajeev Alur | Thomas Wies | |
| 17.30-18.30 | Student session | Student session | Pre Dinner Welcome (17:45) | Student session | |
| Evening | Get-Together (19:30) | School dinner (19:00) | |||
Note: The Student sessions give all participants the opportunity to discuss their PhD/Master topics with the speakers, the organizers and further senior researchers. The topic can be introduced by a short talk (10-15 minutes) and/or a poster. We encourage the participants to contribute to the student sessions. They are a great opportunity to discuss interesting topics with world leading experts in a relaxed atmosphere.
Rajeev Alur
|
Syntax-Guided Synthesis
The classical synthesis problem is to find a program or a system that
meets a correctness specification given as a logical formula. Recent
work on synthesis and optimization illustrates many potential benefits
of allowing the user to supplement the logical specification with a
syntactic template that constrains the space of allowed implementations.
The formulation of the syntax-guided synthesis problem (SyGuS) is aimed
at standardizing the core computational problem common to these
proposals in a logical framework. The input to the SyGuS problem
consists of a background theory, a semantic correctness specification
for the desired program given by a logical formula, and a syntactic set
of candidate implementations given by a grammar. The computational
problem then is to find an implementation from the set of candidate
expressions so that it satisfies the specification in the given theory.
In these lectures, we first describe how a wide range of problems such
as automatic synthesis of loop invariants, program optimization, program
repair to defend against timing-based attacks, and learning programs
from examples can be formalized as SyGuS instances. We then describe the
counterexample-guided-inductive-synthesis (CEGIS) strategy for solving
the SyGuS problem. Finally we discuss our efforts over the past three
years on defining the standardized interchange format built on top of
SMT-LIB, repository of benchmarks from diverse applications,
organization of the annual competition, SyGuS-COMP, of solvers, and
experimental evaluation of solution strategies.
Quantitative Policies over Streaming Data
Decision making in cyber-physical systems often requires dynamic
monitoring of a data stream to compute performance-related quantitative
properties. We propose StreamQRE as a high-level declarative language
for modular specifications of such quantitative policies. This language
is rooted in the emerging theory of regular functions, and every policy
described in this language can be compiled into a space-efficient
streaming implementation. We describe a prototype system that is
integrated within an SDN controller and show how it can be used to
specify and enforce dynamic updates for traffic engineering as well as
in response to security threats. We conclude by outlining the rich
opportunities for both theoretical investigations and practical systems
for real-time decision making in IoT applications.
|
Christel Baier
|
Probabilistic Model Checking
Markov chains (MC) and Markov decision processes (MDP) are widely
used as operational models for the quantitative system analysis. They can be
understood as transition systems augmented with distributions for the states
(in MC) or state-action pairs (in MDPs) to specify the probabilities for the
successor states. Additionally one might add weight functions for modeling
accumulated costs or rewards earned along path fragments to represent e.g.
the energy consumption, the penality to be paid for missed deadlines, the
gain for completing tasks successfully or the degree of the achieved utility.
The tutorial will introduce the main features of discrete-time, finite-state
Markovian models (MC and MDP) and their quantitative analysis against
temporal logic specifications. The first part will present the basic principles
of the automata-based approach for linear temporal logic (LTL) and
probabilistic computation tree logic (PCTL), including a summary of techniques
that have been proposed to tackle the state-explosion problem. The
second part of the tutorial will present algorithms for dealing with fairness
assumptions as well as computing conditional probabilities and expectations
and quantiles. While the former is crucial to establish liveness properties
when MDPs are used as interleaving models. Conditional probabilities and
expectations are useful, for example, to zoom in to rare error scenarios and
to analyze the effect and cost of error-detection mechanisms, while computation
schemes for quantiles can, e.g., be useful to compute the minimal energy
budget that is required to guarantee a certain quality-of-service level with
sufficiently high probability.
|
Hoon Hong
|
Symbolic Computation (Quantifier Elimination)
Symbolic computation is a research area where one develops mathematical theories,
algorithms and software systems for solving problems symbolically, which means
(1) exactly in contrast to approximately and (2) parametrically in contrast to numerically.
Quantifier elimination is one of the core problems in symbolic computation.
It takes a quantified formula and produces an equivalent quantifier-free formula.
Satisfiability checking and theorem proving/verification can be viewed as special cases
where there are no free variables. The original motivation for quantifier elimination
research came from laying firm logical foundation of mathematics. However, recently,
it has been recognized that numerous important problems in science and engineering
can be reduced to that of quantifier elimination.
The lecture will consists of two parts: (1) a quick bird's eye view on the whole
symbolic computation area. (2) a tutorial/survey on various fundamental mathematical
theories and algorithms for quantifier elimination over complex algebra and real algebra, and
if time allows, differential algebra. The lecture will be down-to-earth, hands-on and self-contained.
This lecture will be followed by two closely related in-depth lectures.
(1) Davenport's lecture on crucial issues in the design and use of symbolic computation
algorithm and system. (2) Brown's lecture on cylindrical algebraic decomposition, one of
the most important quantifier elimination algorithms over real algebra.
Hoon Hong is a shared speaker with the SC2 Summer School 2017.
|
Andrew Reynolds
|
SMT Solvers for Verification and Synthesis
A growing number of approaches to software and hardware verification use Satisfiability Modulo Theories (SMT) solvers
as backend reasoning engines. SMT solvers are of interest due to their ability to efficiently reason in theories
such as arithmetic, arrays, inductive datatypes and unbounded character strings.
This talk will cover the basics of how SMT solvers work, and give examples of how they are used in practice. We will focus on recent approaches
in SMT solvers for handling quantified formulas, showing how these approaches can be used for discharging
verification conditions. Additionally, we will cover more advanced features in SMT solvers for function and invariant synthesis.
|
Thomas Wies
|
Introduction to Permission-Based Program Logics
Verifying programs with unbounded resources such as heap-allocated data
is notoriously difficult. Permission-based program logics (e.g.,
Separation Logic and Implicit Dynamic Frames) have greatly influenced
the design of formal methods tools that help to automate this difficult
task.
This course gives an introduction to permission-based program
logics. We will discuss how these logics are used to reason about
program correctness and how they can be automated. Specific topics
include semantics, framing, proof theory and symbolic execution,
decision procedures for entailment, and extensions for reasoning about
concurrent programs.
|
There is a limited number of free shared rooms on campus available for distribution by the selection committee. Please express your interest with your application.
Besides that, participants are responsible for their own accommodation arrangements. We have reserved rooms at a special rate in the following hotels. Please book the rooms yourself using the keyword "VTSA17".
The Summer School 2017 will take place at the Max Planck Institute for Informatics (MPI-INF), on the Saarland Informatics Campus of the Saarland University in Saarbrücken,. Please note that all lectures will take place in building E1 5 (Building of MPI-SWS). For more information on Saarbrücken, you can also check here.
General instructions to the MPI-INF
Use the Online Travel Information System. The nearest bus station on Campus is "Universität Mensa".
There are lots of cozy little pubs and cafés in Saarbrücken, especially near St. Johanner Markt. A few examples:
For comments or questions send an email to jmueller@mpi-inf.mpg.de
The summer school is organized by the Max Planck Institute for Informatics Saarbrücken, the University of Liège, the University of Luxembourg and INRIA Nancy - Grand Est.
| Application Deadline: | ||
|---|---|---|
| Notification until: | 2017/06/15 | |
| Summer School: | 2017/07/31 - 2017/08/04 |
click to enlarge
