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.
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.
The registration will be open to accepted applicants starting on July 15, 2016.
All lectures will take place in room R3 of the building B28. Please find information on directions below.
| 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.
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
|
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
|
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
|
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:
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
|
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.
|
All participants are responsible for their own accommodation arrangements. The following list might help you to find an accommodation that fits your needs:
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).
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.
| Application Deadline: | 2016/07/29 | |
|---|---|---|
| Notification until: | 2016/08/01 | |
| Summer School: | 2016/08/29 - 2016/09/02 |
Break Discussion
