CARI/ICTAC spring school
Stellenbosch, South Africa, 12-15 October 2018
Stellenbosch, South Africa, 12-15 October 2018
This is a spring school affiliated to both CARI and ICTAC 2018. The program consists of 7 half-day tutorials.
Tutorials
Interactive Theorem Proving and Program Development
Yves Bertot (Inria Sophia Antipolis - Méditerranée, FR) [DBLP]
Slides (pdf): part 1, part 2, part 3, part 4, part 5Coq code: sample1.v, sample2.v, sample3.v, sample4.v, sample5.v, sieve.v
Interactive theorem proving is a viable approach to reduce the number of bugs present in modern software, with applications in language design, operating systems, compilers, and a wide variety of mathematical algorithms. The aim of the course is to teach the basic methods relying on an interactive theorem proof assistant to describe formal models of systems, reason about their properties, specify algorithm requirements and solutions, and construct proofs of correctness. This course will be organized in five sub-modules:
- Describing algorithms in the functional setting
- Describing logical properties and performing basic proofs
- Reasoning about recursive functions
- Proofs of programs concerning numbers
- General data types and proofs of advanced programs and algorithms
Verification of Security Protocols:
From Confidentiality to Privacy
Vincent Cheval (Inria Nancy - Grand Est, FR) [DBLP]
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 verification tools. 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 techniques to automatically verify different kinds of security properties. The course will also contain practical sessions where students will be introduced to the use of a protocol verification tool.
Derivation beyond Regular Languages
Peter Thiemann (Universität Freiburg, DE) [DBLP]
Derivation is a well-known technique to transform regular expressions into finite automata and to obtain decision procedures for regular language equivalence and containment. We develop extensions of these techniques to context-free languages and use them to obtain decision procedures for containment in regular languages
Runtime Verification:
Some Basics and Some Latest Developments
Martin Leucker (Universität zu Lübeck, DE) [DBLP]
Slides -- main part (pdf), slides -- TeSSLa (pdf)
This tutorial gives an overview into the field of runtime verification. Starting with the basics on what RV is about, what monitors are, what the concepts of impartiality and anticipation mean, the synthesis of monitors from linear-time temporal logic specifications
In the second part of the tutorial, we present a novel platform for online monitoring of multicore system. A system-on-chip is observed using the tracing capabilities available on many modern multi-core processors. They provide highly compressed tracing information over a separate tracing port. From this information our system reconstructs the sequence of instructions executed by the processor, which can then be analyzed online by a reconfigurable monitoring unit. Analyses are described in a high-level temporal stream-based specification language, called TESSLA, that are compiled to configurations of the monitoring unit. To cope with the amount of tracing data generated by modern processors our system is implemented in hardware using an FPGA.
The work presented is carried out within the COEMS project and has received funding from the EU H2020 programme under grant agreement no. 732016.
An Introduction to Description Logics
Thomas Meyer (University of Cape Town, ZA) [DBLP]
Description Logics are a well-studied family of logic-based knowledge representation formalisms. They are frequently used to represent and reason with formal ontologies. They also provide the formal foundations for many semantic technologies in use today. In this tutorial I will introduce Description Logics by way of an introduction to the Description Logic ALC. More specifically, I will present the syntax and semantics of ALC, discuss an algorithm for reasoning with ALC, and briefly discuss the correctness of the algorithm. The focus will be on ALC because it is widely viewed as representative of many of the important aspects related to reasoning with Description Logics. We'll also have a look at other, more and less expressive, members of the Description Logic family of logics. Time permitting, I will illustrate reasoning with Description Logics using the Protégé ontology editor, a freely available tool for constructing logic-based ontologies, and reasoning over them.
Symbolic Execution for Java
Willem Visser (Stellenbosch University, ZA) [DBLP]
Symbolic execution has grown tremendously in popularity over the last decade, to the point now that commercial companies routinely use it for finding security flaws. This tutorial will be a hands-on look at (a) how to develop both a classic symbolic execution as well as a dynamic symbolic execution (DSE) engine and (b) how to use it to do some interesting analysis. In particular the popular Symbolic PathFinder (SPF, which is based on JPF) and the more recent DSE tool, DEEPSEA, will be used as representative examples. Participants will install and run the tools to get practical experience with using these symbolic execution tools.
In order to do the tutorial exercises, you can download the docker image here. So please install docker on your laptop, download the image by typing "docker pull willemvisser/willem-jpf-mutation" and, once downloaded, type "docker run -it willemvisser/willem-jpf-mutation". You will notice in the root directory there are a number of tutorial files that has the steps to execute.
The Correctness-by-Construction Approach to Programming
Ina Schaefer
(Technische Universität Braunschweig, DE)
[DBLP]
and
Loek Cleophas
(Technische Universiteit Eindhoven, NL)
[DBLP]
Slides (pdf): part 1, part 2, part 3
The purpose of the tutorial is to influence deeply the way the tutorial participants approach the task of developing algorithms, with a view to improving code quality. The tutorial features: a step-by-step explanation of how to derive provably correct algorithms using small and tractable refinements rules; a detailed illustration of the presented methodology through a set of carefully selected graded examples with prototypical tool support; a demonstration of how practical non-trivial algorithms have been derived. The focus is on bridging the gap between two extreme methods for developing software. On the one hand, some approaches are so formal that they scare off all, but the most dedicated theoretical computer scientists. On the other, there are some who believe that any measure of formality is a waste of time, resulting in software that is developed by following gut feelings and intuitions.
The “correctness-by-construction” approach to developing software relies on a formal theory of refinement, and requires the theory to be deployed in a systematic, but pragmatic way. We provide the key theoretical background (refinement laws) needed to apply the method. We then detail a series of graded examples to show how it can be applied to increasingly complex algorithmic problems. We show how the development process can be supported with an IDE and program verification tools. Finally, we present how correctness-by-construction lead to the development of large-scale algorithmic families and discuss practical relevance and industrial uptake.
Program
See in the ICTAC conference program.