Max-Planck-Institut für Informatik

Max-Planck-Institut für Informatik

Université de Liège

Université de Liège

Université du Luxembourg

Université du Luxembourg

Inria

Inria

Summer School 2017: Verification Technology, Systems & Applications

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.

Registration

The registration will be open to accepted applicants starting on June 19, 2017. Registration links have been send via eMail.

Program

Schedule

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.

Lecturer(s)

Rajeev Alur
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
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
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
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
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.

Accommodation

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".

Arrival / Directions

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.

Travelling to MPI-INF

General instructions to the MPI-INF

Public Transportation between the City and the MPI-INF

Use the Online Travel Information System. The nearest bus station on Campus is "Universität Mensa".


General Locations and Tips

There are lots of cozy little pubs and cafés in Saarbrücken, especially near St. Johanner Markt. A few examples:

  • Kulturcafé
    Sankt Johanner Markt 24
    66111 Saarbrücken
  • Vapiano
    Bahnhofstraße 22
    66111 Saarbrücken
  • Iguana
    Mainzer Strasse 2
    66111 Saarbrücken
  • Alex
    Saarstraße 15
    66111 Saarbrücken

Organization and Contact

General Organization

Local Organization

Website

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.

Important Dates

Application Deadline: 2017/06/01 2017/06/09 (extended!)
Notification until: 2017/06/15
Summer School: 2017/07/31 - 2017/08/04
(Format is YYYY/MM/DD)

Poster

Sponsored by

Max-Planck-Institut für Informatik

Université du Luxembourg

Interdisciplinary Centre for Security, Reliability and Trust

Inria

Université de Liège