Université de Liège

Université de Liège

Université du Luxembourg

Université du Luxembourg

University Koblenz-Landau

Universität Koblenz-Landau

Inria

Inria

Max-Planck-Institut für Informatik

Max-Planck-Institut für Informatik

Summer School 2016: Verification Technology, Systems & Applications

The summer school on verification technology, systems & applications takes place at the University of Liège in Liège from August 29 - September 2, 2016. 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 Hubert Comon, Thomas Eiter, Jean Krivine, Tobias Nipkow and Ruzica Piskac 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 vtsa16@montefiore.ulg.ac.be including

until July 29, 2016. Notifications on acceptance/rejection will be given by August 1, 2016.

Registration

The registration will be open to accepted applicants starting on July 15, 2016.

Program

All lectures will take place in room R3 of the building B28. Please find information on directions below.

Schedule

August 29
Monday
August 30
Tuesday
August 31
Wednesday
September 1
Thursday
September 2
Friday
8.00-8.50 Registration
8.50-9.00 Welcome
9.00-12.30 Tobias Nipkow
Jean Krivine
Thomas Eiter
Ruzica Piskac
Hubert Comon
12.30-14.00 Lunch break
14.00-17.20 Jean Krivine
Tobias Nipkow
Hubert Comon
Thomas Eiter
Ruzica Piskac
17.20-18.30 Student session Student session Student session
Evening Get-Together (19.00) School dinner (19.30)

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)

Hubert Comon
Hubert Comon

Communication security: Formal models and proofs

We will introduce the problem of verifying that a communication protocol satisfies a security property. This is a model-checking problem, however in a hostile environment. The focus of the lecture will be on modelling such a hostile environment (attacker). There are several possible choices, among which the classical Dolev-Yao attacker and probabilistic polynomial time communicating Turing machines. The goal will be to uniformly define these semantics and the some associated proof techniques
Thomas Eiter
Thomas Eiter

Answer Set Programming and Extensions

In the recent years, Answer Set Programming (ASP) has gained increasing attention and has become besides SAT, SMT and QBF a valuable tool of computational logic for declarative problem solving. Rooted in knowledge representation and nonmonotonic reasoning, ASP offers features beyond first-order expressibility, and motivated by applications, numerous extensions of ASP have been devised.
This lecture will give an introduction to ASP, and will contrast it with SAT and QBF. Furthermore, it will consider extensions of ASP that are geared towards interaction with other software, such as constraint solvers and description logic engines. Finally, it will briefly consider applications and ongoing developments.
Jean Krivine
Jean Krivine

Executable knowledge representation in Systems Biology: the rule-based approach

(Prior knownledge in biology is not needed (and not even useful) to follow this tutorial.)
As the quest for a cure for cancer is progressing through the era of high throughput experiments, the attention of biologists has turned to the study of a collection of signaling pathways that are suspected to be involved in the development of tumors. These pathways can be viewed as channels that propagate, via protein-protein interactions, the information received by the cell at its surface down to the nucleus in order to trigger the appropriate genetic response. This simplified view is challenged by the observation that most of this signaling cascades share components, such as kinases (that tend to propagate the signal) and phosphatases (that have the opposite effect). This implies that signaling cascades not only propagate information, but have also evolved to implement robust probabilistic "protocols" to trigger appropriate responses in the presence of various (possibly conflicting) inputs.
As cancer is now believed to be caused by a deregulation of such protocols, usually after some genes coding for the production of signaling components have mutated, systems biologists are accumulating immense collections of biological facts about proteins involved in cell signaling: for instance, more than 18,000 papers mentioning the protein EGFR, a major signaling protein, either in their title or abstract have been published since 2012. The hope of such data accumulation is to be able to identify possible targets for chemotherapy that would be specialized to a specific oncogenic mutation.
If biological data are being produced at an exponential rate, the production of comprehensive models of cell signaling is lagging. One of the reasons for the unequal race between data production and data integration is the difficulty to make large combinatorial models executable.
Site (or port) graph rewriting techniques, also called rule-based modeling [1], provide an efficient representation formalism to model protein-protein interactions in the context of cell-signaling. In these approaches, a cell state is abstracted as a graph, the nodes of which correspond to elementary molecular agents (typically proteins). Edges of site graphs connect nodes through named sites (sometimes called ports) which denote a physical contacts between agents. Biological mechanisms of action are interpreted as rewriting rules given as pairs of (site) graphs patterns. Importantly, rules are applied following a stochastic strategy, also known as SSA or Gillespie's algorithm for rule-based formalisms [2]. KaSim [3] is an efficient rule-based simulators that implements this algorithm for the Kappa language, a site-graph formalism adapted to biology.
In this tutorial, we will learn to abstract away and represent bio-molecular interactions in Kappa. Simulation and analysis of Kappa models will be studied and explained through interactive modeling exercises.
References
[1] Vincent Danos, Jérôme Feret, Walter Fontana, Russell Harmer, Jean Krivine: Rule-Based Modelling of Cellular Signalling. CONCUR 2007: 17-41 2006
[2] Vincent Danos, Jérôme Feret, Walter Fontana, Jean Krivine: Scalable Simulation of Cellular Signaling Networks. APLAS 2007: 139-157
[3] see dev.executableknowledge.org
Tobias Nipkow
Tobias Nipkow

Introduction to Interactive Proof with Isabelle/HOL

This course introduces interactive theorem proving with the Isabelle/HOL system [1,2]. It does so in 3 steps:
  • Verified functional programming: The logic HOL contains an ML-style functional programming language. It is shown how to verify functional programs in this language by induction and simplification.
  • Predicate logic: Formulas of predicate logic and set theory are introduced, together with inductively defined predicates.
  • Structured proofs: We introduce the proof language Isar and show how to write structured proofs that are readable by both the machine and the human.
The course assumes basic familiarity with some functional programming language of the ML or Haskell family, in particular with recursive data types and pattern matching. No specific background in logic is necessary beyond the ability to read predicate logic formulas. Students who want to obtain more than a superficial grasp of the subject are encouraged to bring their own laptops with the Isabelle system already downloaded (http://isabelle.in.tum.de). The lectures will be accompanied with exercises, and Tobias Nipkow will be happy to help.
[1] Tobias Nipkow. Programming and Proving in Isabelle/HOL. "isabelle.in.tum.de/doc/prog-prove.pdf
[2] Tobias Nipkow, Gerwin Klein. Concrete Semantics. Springer, 2014. www.concrete-semantics.org
Ruzica Piskac
Ruzica Piskac

SMT-based Verification of Heap-manipulating Programs

The goal of this course is to introduce the students to the theory and practice of program analysis and software verification. We will introduce the basic vocabulary of program verification; students will become familiar with assertions, pre- and post-conditions, and inductive invariants. They will learn how to derive mathematical formulas from the code and annotations (so called "verification conditions"). We will explore some state-of-the art tools used for program verification and we will provide more detailed insights into algorithms and paradigms on which those tools are based such as SMT solvers and decision procedures. Finally, we will discuss how to reason about programs that manipulate dynamically allocated data structures, such as lists or trees.

Accommodation

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

Arrival / Directions

The Summer School 2016 will take place on the Sart-Tilman campus of the University of Liège. All lectures will take place in room R3 of the Montefiore Institute, building B28, parking lot P32 (directions).

Organization and Contact

General Organization

Local Organization

Website

For comments or questions send an email to vtsa16@montefiore.ulg.ac.be

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

Important Dates

Application Deadline: 2016/07/29
Notification until: 2016/08/01
Summer School: 2016/08/29 - 2016/09/02
(Format is YYYY/MM/DD)

Poster

Photos

Break Discussion

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