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

• a one page CV
• an application letter explaining your interest in the school and your experience in the area
• a copy of your bachelor certificate (or equivalent or a more significant certificate)
• a short statement if you want to contribute to the student sessions

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

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

KLOSTER, JUGENDHERBERGE, FERIENWOHNUNGEN

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

• Viorica Sofronie-Stokkermans
• Bernard Boigelot
• Stephan Merz
• Jun Pang
• Christoph Weidenbach

Local Organization

• Beate Körner

Local Support

• Markus Bender
• Matthias Horbach
• Sabine Hülstrunk

Website

• Eugen Denerz

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

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

 

• Summer School 2015
• Application
• Registration
• Program
• Accommodation
• Arrival/Directions
• Organization und Contact
• Important Dates
• Poster
• History
  VTSA 14 VTSA 13 VTSA 12 VTSA 11 VTSA 10 VTSA 09 VTSA 08