University Koblenz-Landau

Universität Koblenz-Landau

Université de Liège

Université de Liège

Université du Luxembourg

Université du Luxembourg

Inria

Inria

Max-Planck-Institut für Informatik

Max-Planck-Institut für Informatik

Summer School 2015: Verification Technology, Systems & Applications

The summer school on verification technology, systems & applications takes place at the University of Koblenz-Landau in Koblenz from August 24–28, 2015. 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 Bernhard Beckert, Stephanie Delaune, Alberto Griggio, Tobias Schubert and Mihaela Sighireanu 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. Recommendations on hotels can be found below.

Application

Please apply electronically by sending an email to Eugen Denerz (please note: You can encrypt the email and your documents using [Open]PGP or S/MIME to protect your data.) including

until Friday, July 17, 2015. Notifications on acceptance/rejection will be given by Friday, July 24, 2015.

Registration

The registration will be open to accepted applicants starting on Friday, July 24, 2015.

Program

All lectures will take place in room 239 of the building D. Please find the campus map below.

The programme can be downloaded as a PDF file here.

Schedule

August 24
Monday
August 25
Tuesday
August 26
Wednesday
August 27
Thursday
August 28
Friday
8.00-8.50 Registration
8.50-9.00 Welcome
9.00-12.30 Tobias Schubert
Stephanie Delaune
Alberto Griggio
Bernhard Beckert
Mihaela Sighireanu
12.30-14.00 Lunch break
14.00-17.20 Alberto Griggio
Tobias Schubert
Stephanie Delaune
Mihaela Sighireanu
Bernhard Beckert
17.20-18.30 Student session (each 15 min)
  • Haniel Barbosa: Congruence Closure with Free Variables
  • Martin Riener: Current Challenges for the TLA Proof System
  • Marco Voigt: Decidability of First-Order Logic with Real Constraints
Student session (each 15 min)
  • Paulius Stankaitis: Event - B and Cloud Provers
  • Pekka Aho: Automated Extraction of Graphical User Interface Models
Student session (each 15 min)
  • Michał Wypych: Alvis Formal Modeling Language
  • Oleksandra Kulankhina: Integrated Environment for Verifying and Running Distributed Components
  • Ahmed Irfan: Word-Level Formal Verification of Verilog Designs
Evening Get-Together (19.00) School dinner (18.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)

Bernhard Beckert
Bernhard Beckert

Deductive Verification of Object-Oriented Software

In this lecture we show how Java programs can be formally specified using the Java Modeling Language (JML), and how they can be analysed using techniques such as deductive verification and symbolic execution.
The KeY System will be used for demonstration purposes. KeY is a software verification tool that aims to integrate implementation, formal specification, and formal verification of object-oriented software as seamlessly as possible. At the core of the system is a theorem prover for first-order Dynamic Logic for Java with a user-friendly graphical interface.
The lecture covers the following topics:
  • Formal specification of object-oriented programs.
  • Deductive verification of (Java) implementations w.r.t. their specification based on a sequent calculus for Dynamic Logic.
  • Using verification technology as a basis for other purposes such as, for example, information-flow analysis.
  • Case studies and critical assessment.
Though we concentrate in this lecture on particular languages (Java and the Java Modeling Language), the presented ideas, problems, and solutions apply to other object-oriented design and implementation languages as well.
Stephanie Delaune
Stephanie Delaune

Verification of Security Protocols: from Confidentiality to Privacy

Security protocols are widely used today to secure transactions that take place through public channels like the Internet. Typical functionalities are the transfer of a credit card number or the authentication of a user on a system. Because of their increasing ubiquity in many important applications (e.g. electronic commerce, smartphone, government-issued ID . . . ), a very important research challenge consists in developing methods and verification tools to increase our trust on security protocols, and so on the applications that rely on them.
Formal methods offer symbolic models to carefully analyse security protocols, together with a set of proof techniques and efficient tools such as ProVerif. These methods build on techniques from model-checking, automated reasoning and concurrency theory. We will explain how security protocols as well as the security properties they are supposed to achieve are formalised in symbolic models. Then, we will describe and discuss decision techniques to automatically verify different kinds of security properties.
Alberto Griggio
Alberto Griggio

Exploiting SMT for Verification of Infinite-State Systems

Satisfiability modulo theories has become increasingly popular in the last decade. One of the main applications of SMT is formal verification. In this lecture, we will discuss how to exploit efficient SMT techniques for verifying properties of infinite-state systems. We will start from the basic building blocks of modern SMT solvers, and then describe extended functionalities that are of fundamental importance in verification (such as computation of interpolants). Finally, we will discuss how to put together the various bits in order to obtain effective verification algorithms for various kinds of systems and properties.
Tobias Schubert
Tobias Schubert

SAT-based Approaches for Test and Verification of Integrated Circuits

The Boolean Satisfiability Problem (SAT) is one of the most well-known problems in computer science. It is not only of theoretical interest, but also finds many applications, for example in the area of Computer Aided Design. In particular with respect to test and formal verification of integrated cicruits, SAT solving now has become the state-of-the-art solving technique. Todays SAT solvers are able to efficiently handle industrially-sized problems even if the corresponding SAT formula contains millions of clauses. Due to this success story SAT-related approaches (also reffered to as generalizations of SAT) like MAX-SAT, #SAT, QBF, and SMT have become more and more popular in the last few years, because on the one hand in some cases SAT does not allow for a compact and efficient representation of the question to be answered, while on the other hand these approaches in most cases also benefit from the SAT optimization techniques developed in recent years.
The first part of the lecture will highlight the main components of modern SAT solvers followed by an overview of generalizations of SAT like MAX-SAT, #SAT, QBF, and SMT. In the second part of the lecture we will show how the different SAT-based approaches can be used to solve real-world problems, in particular in the area of test and formal verification of integrated circuits.
Mihaela Sighireanu
Mihaela Sighireanu

Modelling, Specification and Formal Analysis of Complex Software Systems

To face the complexity that arises in reasoning about modern software systems, automatic program verification methods must rely on powerful decision procedures for rich theories on data structures, as well as on efficient symbolic model-checking algorithms, combined with static analysis techniques. For both static analysis and model checking techniques, a crucial point is the definition of suitable logic-based specification formalisms and efficient symbolic representations allowing to reason about the infinite sets of program states (i.e. configurations of its memory) at different abstraction levels.
This talk presents through two examples, i.e., programs with an unbounded number of threads and procedure calls and programs manipulating dynamic data structures, several choices for such a logic-based formalisms, based on First-Order Logic resp. Separation Logic. These formalisms are investigated from the point of view of expressiveness, decidability and complexity. We show that by choosing a fragment with a good trade-off between these qualities, it is possible to obtain not only the automatic verification of program properties but also the automatic inference of program invariants.

Accommodation

All participants are responsible for their own accommodation arrangements. The following list might help you to find an accommodation that fits your needs:

Please note: You can receive special prices for the hotels.

Hotels

Cityhotel Kurfürst Balduin ***
Hohenfelder Str. 12
56068 Koblenz
Tel: 0261-133250
Fax: 13222100
Special Price (when booking mention keyword VTSA)
Single room: 55,50 € including breakfast
Double room: 81,00 € including breakfast
www.cityhotel-koblenz.de
Hotel Weinhaus Kreuter ***
Stauseestr. 31
56072 Koblenz-Güls
Tel: 0261-94147-0
Fax: 0261-94147-60
Special Price (when booking mention keyword VTSA)
Single room: 60,00 € including breakfast
Double room: 90,00 € including breakfast
www.hotel-kreuter.de
Contel Hotel ****
Pastor-Klein-Str. 19
56073 Koblenz
Tel: 0261 40 65-154 (or -159)
Fax: 0261 40 65 - 188
Special Price (when booking mention keyword VTSA)
Single room: 85,00 € incl. breakfast
Double room: 95,00 € incl. breakfast
www.contel-koblenz.de

KLOSTER, JUGENDHERBERGE, FERIENWOHNUNGEN

Kloster: Schönstätter Marienschwestern Haus Providentia
Trierer Straße 388
56070 Koblenz
Tel: 0261-27010
EZ 25,00 € (+ FR 7,00)
E-mail: info@haus-providentia.de
www.haus-providentia.de
Jugendherberge Koblenz
Festung Ehrenbreitstein
56077 Koblenz
Tel: 0261-972870
EZ 28,00 € inkl. FR / DZ 45,00 € inkl. FR / (alle Zimmer mit Dusche und WC).
Es gibt auch Mehrbettzimmer.
www.diejugendherbergen.de/
Ferienwohnung in KO-Metternich, Bachweg 1a (Uni-Nähe)
www.ferienwohnung-uni-koblenz.de/Uni-3.html
Preis verhandelbar z.B. bei 4 Personen 25,00 € p.P./p.Tag
Ferienwohnung in Güls, Palmstück 45
www.fewo-sodin.de/html/home.html
Ideal zur Unterbringung von bis zu 5 Personen.
Bei 3 Personen 45,00 €/Tag

Arrival / Directions

The Summer School 2015 will take place on the campus Koblenz-Metternich of the University of Koblenz-Landau in Koblenz (Germany). Please find more information on arrival here.

All lectures will take place in room 239 of the building D:

Organization and Contact

General Organization

Local Organization

Local Support

Website

For comments or questions send an email to Viorica Sofronie-Stokkermans

The summer school is organized by the University of Koblenz-Landau, Montefiore Institute, University of Luxembourg, INRIA Nancy, and the Max Planck Institute for Informatics Saarbrücken.

Important Dates

Application Deadline: 2015/07/17
Notification until: 2015/07/24
Summer School: 2015/08/24 - 2015/08/28
(Format is YYYY/MM/DD)

Poster

Sponsored by

Universität Koblenz-Landau

Université du Luxembourg

Interdisciplinary Centre for Security, Reliability and Trust

Inria

Max-Planck-Institut für Informatik

Université de Liège

Fonds National de la Recherche Scientifique