Formal verification is the mathematical proof of the correctness of algorithms, protocols and computer systems. In the last decades proof assistants like Isabelle have verified a general-purpose operating system microkernel in the order of 10000 lines of C-code as well as a 300-pages textbook on programming language semantics. Journals like Archive of Formal Proofs have numerous verified articles covering both mathematics and computer science topics and many other verification projects have been successfully completed. The development and use of proof assistants and related tools, including model checking and advanced solvers, can be found in several sections at DTU Compute, for example in analysis of embedded systems, software specification and verification, security protocols, algorithms and meta-logic. The aim of the project is to strengthen the cross-sectional cooperation in formal verification research and teaching.
Supported by DTU Compute's Strategic Foundation
Portal for research and teaching in higher-order logic, in particular using the proof assistant Isabelle for formalization and verification: https://hol.compute.dtu.dk
Makarius Wenzel's slides are available here: https://sketis.net/2017/future-prospects-of-isabelle-technology
Program:
Tuesday 5 December 2017 - DTU room 303B/034 (entrance from the glass corridor) 9:30-10:30 Arne Borälv (Chief Strategy Officer, Prover Technology, Sweden): The Prover Trident process for Interlocking Design Automation 10:40-11:15 Julien Ouy (Life-Critical Software Developer, ClearSy, France): Co-Simulation of a Safety Critical Railway Application 11:15-11:20 Henrik Sylvan (Head of Center Railtech DTU): Working with Railways across Disciplines 11:20-11:50 Anne Haxthausen (DTU Compute): Model Checking Geographically Distributed Railway Interlocking Systems using UMC 13:30-14:10 Signe Geisler & Anne Haxthausen (DTU Compute): Modelling and Verification of a Distributed Railway Interlocking System using RAISE 14:10-14:30 Alessandro Fantechi (University of Florence, Italy): Railway Interlocking as a Distributed Mutual Exclusion Problem 14:30-15:00 Wrap Up - Discussions
Abstract for the talk by Arne Borälv: Prover iLock is a desktop tool suite for formal development of application software for railway interlocking systems, ready for compilation and installation on the target platform. An overview of the process of using Prover iLock and a demonstration will be provided, including (1) Configuration of a new interlocking, (2) Interactive and scripted simulation of the resulting signaling system, (3) Automatic generation of code for the interlocking, and (4) Formal verification of the generated code. The presentation will in addition include (1) Industrial applications of Prover iLock, and (2) The sign-off verification flow based on Prover Certifier, producing complete safety evidence for CENELEC EN50128 SIL 4 certification based on formal verification (with access to the cloud I aim to demonstrate this too).
Abstract for the talk by Julien Ouy: INTO-CPS is a H2020 R&D project that is developing a tool-chain and methods supporting continuous and discrete models. We present an application to railway where a light rail line is modeled (equipment and train) in this context. It is first equipped with a central interlocking then with a distributed interlocking for which we have obtained a Hardware in the Loop co-simulation, the source code being automatically generated from the models.
Abstract for the talk by Alessandro Fantechi: In this talk the problem of railway interlocking is generalized to a particular class of distributed mutual exclusion problems, addressing simultaneous locking of a pool of distributed objects. A family of distributed algorithms solving this problem is envisioned, with variants related to where the data defining the pool's topology reside, and how such data rules the communication between nodes. Some proposed distributed interlocking algorithms are shown to be instances of such variants.
Program:
Wednesday 29 November 2017 - DTU room 322/123 15:00-16:00 Jüri Vain (Tallinn University of Technology, Estonia): Multi-Fragment Markov Model Guided Online Model-Based Testing for MPSoC
Model-based online monitoring and testing are commonly accepted quality assurance measures for mission critical systems (MCS). We propose an integrated approach where the Multi-Fragment Markov Models (MFMM) are used for specifying the system reliability and quality of service related behavior on highlevel of abstraction, and the more concrete state and timing constraints related with MFMM are specified explicitly using Uppaal Probabilistic Timed Automata (UPTA). To interrelate these two model classes we demonstrate how the MFMM is mapped to UPTA. The second contribution is the test case selection mechanism for online identification of MCS execution modes by model-based conformance testing where the test cases are prioritized by their durations and probabilities of execution modes. The hypotheses on which mode the system switches next are provided by MFMM and the hypotheses are tested using UPTA for online conformance. The approach is illustrated with the Bonfire Multi-Processor System-on- Chip (MPSoC).
Program:
Monday 27 November 2017 - DTU room 101/S12 14:00-15:00 Luca Vigano (Kings College, London, UK): Access-Controlled Temporal Networks
We define Access-Controlled Temporal Networks (ACTNs) as an extension of well-known temporal networks such as simple temporal networks (STNs), conditional STNs, STNs with uncertainty, and conditional STNs with uncertainty (the latter have been used to represent the temporal constraints of workflows underlying business processes). ACTNs are capable of handling important characteristics such as contingent durations and conditional paths, as well as authorization constraints in order to model “who can do what, when”. Controllability of ACTNs (i.e., the existence of a set of strategies for executing the network no matter how the uncontrollable parts behave) generalizes the answer to the temporal workflow satisfiability problem ensuring the existence of a set of strategies covering all possible valid assignments of tasks to users. To check if an ACTN is controllable, we extend a recent mapping from temporal networks to Timed Game Automata and use sound and complete algorithms of the UPPAAL-TIGA software.
Program:
Thursday 23 November 2017 - DTU room 101/S14 13:00-14:00 Markus "Makarius" Wenzel (Sketis, Augsburg, Germany): Future Prospects of Isabelle Technology 14:30-15:30 Johannes Åman Pohjola (Chalmers University of Technology, Gothenburg, Sweden): End-to-End Verification with CakeML
Abstract for the talk by Markus "Makarius" Wenzel: In the past 3 decades, Isabelle has made a long way from a modest LCF-style proof assistant (with copy-paste of proof scripts written in ML) to the current Isabelle/PIDE editor-environment (with its timeless and stateless processing of proof documents). In this presentation I will try to extrapolate this into the future: How far can we scale proof documents and libraries, e.g. via moving Isabelle into the "cloud"? How can we reduce system resource requirements on the client side? How can we upgrade interactive edits produced by a single author, towards versioned changesets by multiple or distributed authors? What are suitable frameworks for the next generation of Isabelle document preparation? What can we make out of Isabelle/ML as ultra-clean environment for functional programming? Etc. etc.
Abstract for the talk by Johannes Åman Pohjola: Software verification tools that build machine-checked proofs of functional correctness usually focus on the algorithmic content of the code. Their proofs are not grounded in a formal semantic model of the hardware and operating system that will ultimately run the program. As a result, several layers of translation and wrapper code must be trusted. In contrast, the CakeML project focuses on end-to-end verification to replace this trusted code with verified code in a cost-effective manner. We show how to prove functional correctness at the binary level for real executables that do I/O and file handling, with only a little more effort than an algorithmic-level proof.
Program:
Monday 13 November 2017 - DTU room 101/S10 13:00-14:00 Stefan Berghofer (secunet Security Networks AG, Dresden, Germany): Development of Security-Critical Software with SPARK/Ada at secunet 14:30-15:30 Christian Sternagel (University of Innsbruck, Austria): IsaFoR/CeTA - An Isabelle/HOL Formalization of Rewriting for Certified Tool Assertions
Abstract for the talk by Stefan Berghofer: In this talk, we describe how the SPARK/Ada language and toolset is used for the development of component-based high-security systems at secunet Security Networks AG. To make the complexity of assessing the security of these systems manageable, the components are running on top of a separation kernel, which ensures that they can only communicate with each other via designated channels. We give an overview of our methodology for verifying trusted components using a combination of the SPARK tools and the interactive proof assistant Isabelle, which is used for solving proof obligations that are beyond reach of automatic provers. We illustrate the methodology using selected correctness properties of a cryptographic library.
Abstract for the talk by Christian Sternagel: I will give a general overview of the ongoing IsaFoR/CeTA project and its two main components: (1) the IsaFoR proof library for Isabelle/HOL, focusing on term rewriting related properties (like termination, confluence, and completion) and (2) the accompanying, formally verified certifier CeTA, obtained by code generation.
Program:
Thursday 9 November 2017 - DTU room 101/S16 13:30-14:00 Jørgen Villadsen (DTU Compute, joint work with Anders Schlichtkrull and Andreas Halkjær From): A Certified Simple Prover for First-Order Logic 14:00-15:00 Freek Wiedijk (Radboud University, Nijmegen, The Netherlands): Trust 15:00-15:30 Anders Schlichtkrull (DTU Compute): IsaFoL - Isabelle Formalization of Logic - A Brief Overview
Abstract for the talk by Freek Wiedijk: I will discuss how trustworthy a formal proof (checked with an interactive theorem prover like Coq, Isabelle or one of the HOLs) can be, both in theory and in practice. I will illustrate this by explaining the current state of the art and by discussing possible new technologies.
Program:
Thursday 12 October 2017 - DTU room 101/S04 13:00-14:00 Andreas Halkjær From (DTU Compute): FIT - From's Isabelle Tutorial - Verification of Quicksort 14:30-15:30 Uwe Waldmann (Max-Planck-Institut für Informatik - Saarbrücken): Saturation Theorem Proving - Basic Ideas, History, and Recent Developments
Abstract for the talk by Uwe Waldmann: With the development of "Hammers", automated theorem provers have become increasingly important for improving the degree of automation of interactive proof systems. Saturation provers, such as E, SPASS, or Vampire, are one of the two categories of automated provers used in this context. These provers are based on variants of the superposition calculus for first-order logic with equality. In this talk, we give an overview of the history of saturation calculi from the 1960's (resolution, completion) to recent developments; we explain how these calculi work, why they work, and what makes them successful in practice.
Program:
Thursday 7 September 2017 - DTU room 101/S10
9:30-9:45 Jørgen Villadsen & Sebastian Alexander Mödersheim (DTU Compute): Welcome & Introduction
10:00-10:45 Andreas Lochbihler (ETH Zurich): CryptHOL - Game-Based Cryptographic Proofs in Higher-Order Logic
11:00-11:30 Sebastian Alexander Mödersheim (DTU Compute, joint work with Achim Brucker, Alessandro Bruni and Andreas Hess): PSPSP - Proper Security Proofs of Stateful Protocols
11:30-12:00 Michael Reichhardt Hansen (DTU Compute, based on joint work with Patrick Kasting and Steen Vester): On Local, On-the-Fly, Game-Based Methods for Synthesizing Control Programs for Railway Networks
13:00-13:45 Luís Cruz-Filipe (University of Southern Denmark, Odense): Formal Verification of Very Large Proofs in Coq
14:30-15:15 Nicolas Peltier (Laboratoire d’Informatique de Grenoble): A Formalization of the Superposition Calculus in Isabelle
15:30-16:00 Anders Schlichtkrull (DTU Compute, joint work with Jasmin Christian Blanchette, Dmitriy Traytel and Uwe Waldmann): Formalization of an Ordered Resolution Prover in Isabelle/HOL
16:00-16:30 Jasmin Christian Blanchette (VU Amsterdam, joint work with Mathias Fleury and Christoph Weidenbach): A Verified SAT Solver with Two Watched Literals in Isabelle/HOL
Program:
Tuesday 28 February 2017 - DTU room 101/S16 10:15-10:30 John Bruntse Larsen & Jørgen Villadsen: An Approach for Hospital Planning with Multi-Agent Organizations 10:30-11:30 Virginia Dignum (TU Delft, The Netherlands): Interactions as Social Practices - Towards a Formalization
Abstract for the talk by Virginia Dignum: Multi-agent modelling and simulation are a suitable starting point to model complex social interactions. However, as the complexity of the systems increase, we argue that novel modelling approaches are needed that can deal with inter-dependencies at different levels of society, where many heterogeneous parties are interacting and reacting to each other. We argue that for many intelligent and autonomous systems the BDI (Belief-Desire-Intention) architecture is a solid basis, but does not give enough support to model the autonomous decision processes required for these systems. In this talk, we sketch a fundamentally social formal framework for the agents in these simulations in order to get a grip on the underlying mechanisms at work. We show some scenarios where we applied some of the ideas and sketch the sociological foundation of the agents and an agent architecture that can be used for building agent based simulations for societal challenges.
Program:
Wednesday 30 November 2016 - DTU room 325/H009 9:30-10:15 Achim Brucker: Security of Browser Extensions - Towards a Formal Model 10:45-11:30 Christoph Sprenger: Refining Authenticated Key Agreement with Strong Adversaries 13:00-13:45 Andrei Popescu (joint work with Ondrej Kuncar): A Consistent Foundation for Isabelle/HOL 14:15-15:00 Heinrich Ody: Discounted Duration Calculus 15:30-16:15 Markus Roggenbach: On the 'Algebra' of Railway Interlockings 16:15-17:00 Hugo Daniel dos Santos Macedo: Compositional Verification of Multi-Station Interlocking Systems
Abstracts:
Achim Brucker (University of Sheffield, UK): Security of Browser Extensions - Towards a Formal Model
On the one hand, browser extensions, e.g., for Chrome, are very useful, as they extend web browsers with additional functionality (e.g., blocking advertisements). On the other hand, they are the most dangerous code that runs in your browsers: extension can modify both the content displayed in the browser as well as the communication with any web-site or web-service. Moreover, the current security model for browser extensions seems to be inadequate for expressing the security and privacy needs of browser users. Consequently, browser extensions are a "juice target" for attackers targeting web users. In this talk, we first present our results of analyzing the current security model of browser extensions. Second, we present first steps towards formally modeling the parts of a web browser that are necessary to analyze and propose a future security model for browser extensions. The long-term goal of our work is to provide a formally verified security model for web browser extensions that focuses on the need of browser users.
Christoph Sprenger (ETH Zurich, Switzerland): Refining Authenticated Key Agreement with Strong Adversaries
This talk presents the development of a family of key agreement protocols that are correct-by-construction. Our development method is based on stepwise refinement. We use our previously proposed refinement strategy, which transforms abstract security goals into protocols that are secure when operating over an insecure channel controlled by a Dolev-Yao-style adversary. As intermediate levels of abstraction, we employ message-less guard protocols and channel protocols communicating over channels with security properties. The present work substantially extends this framework. First, we strengthen the adversary by allowing him to compromise different resources of protocol participants, such as their long-term keys or their session keys. This enables the systematic development of protocols that ensure strong properties such as perfect-forward secrecy. Second, we broaden the class of protocols supported to include those with non-atomic keys and equationally defined cryptographic operators. Third, we implement channels in a parametric way, under a set of assumptions that any concrete implementation must satisfy. This approach sheds light on the conditions that are needed for such implementations to be secure and makes security proofs more modular. These extensions required a major redesign of our previous framework. We have implemented our method in Isabelle/HOL and used it to develop key agreement protocols including signed Diffie-Hellman and the core of IKEv1 and SKEME.
Andrei Popescu (Middlesex University London, UK): A Consistent Foundation for Isabelle/HOL (joint work with Ondrej Kuncar)
The interactive theorem prover Isabelle/HOL is based on the well understood Higher-Order Logic (HOL), which is widely believed to be consistent (and provably consistent in set theory by a standard semantic argument). However, Isabelle/HOL brings its own personal touch to HOL: overloaded constant definitions, used to achieve Haskell-like type classes in the user space. These features are a delight for the users, but unfortunately are not easy to get right as an extension of HOL—they have a history of inconsistent behavior. It has been an open question under which criteria overloaded constant definitions and type definitions can be combined together while still guaranteeing consistency. This paper presents a solution to this problem: non-overlapping definitions and termination of the definition-dependency relation (tracked not only through constants but also through types) ensures relative consistency of Isabelle/HOL.
Heinrich Ody (Carl von Ossietzky Universität Oldenburg, Germany): Discounted Duration Calculus
To formally reason about the temporal quality of systems discounting was introduced to CTL and LTL. However, these logic are discrete and they cannot express duration properties. In this work we introduce discounting for a variant of Duration Calculus. We prove decidability of model checking for a useful fragment of discounted Duration Calculus formulas on timed automata under mild assumptions. Further, we provide an extensive example to show the usefulness of the fragment.
Markus Roggenbach (Swansea University, UK): On the 'Algebra' of Railway Interlockings
Formal verification of railway control software has been identified as one of the "grand challenges" of Computer Science. This challenge comes in two parts. The first addresses the question of whether proposed mathematical models faithfully represent the railway domain; verifications must translate to guarantees in the real world. The second addresses the question of how to employ available technologies effectively; analyses must be doable in practice and not just in theory. Our talk will focus on the second, while briefly touching on the first of these challenges. In addressing the second part of the grand challenge we face the wider challenge for formal methods of overcoming state space explosion. Having rendered a real-world problem into a modelling language, it remains a mystery in general as to how to decompose a verification problem into tractable pieces whose solutions can be composed together to provide a solution to the initial problem. Our approach is to carry out abstractions at the domain level, thus avoiding the lack of general compositional techniques in modelling languages. We have developed three abstraction techniques which provide - to a certain extent - the 'algebraic' laws of railway interlockings. These techniques have proven successful in practice, both in isolation and taken together: 1. Finitisation reduces the number of trains that need to be considered in order to prove safety for an unbounded number of trains; 2. Covering decomposes the network into a set of sub-networks in a compositional fashion: proving correctness results for the sub-networks suffices to infer the correctness of the whole network; and 3. Topological abstraction reduces the number of tracks in the topology of the network, so as to minimise the size and complexity of the network prior to its analysis. The second abstraction technique is a particular strength of our approach. In her 2003 paper, Winter theorized on the possibility of such compositional proof strategies for the railway domain, but to our knowledge there has since been no practical solution. Putting things into the wider context of a "grand challenge" again, our work in the railway domain might serve as witness for our belief: careful analysis on the domain level will lead to the abstractions and decompositions which are key to the successful application of Formal Methods on industrial size challenges.
Hugo Daniel dos Santos Macedo (DTU Compute): Compositional Verification of Multi-Station Interlocking Systems
The railway controlling interlocking systems are safety-critical components and their automated safety verification is an active research topic involving several groups that typically employ verification techniques to produce important cost and time savings in their certification. Such systems pose a big challenge to general verification tools due to the inherent computational resource demands. In this talk we report on how we improve an existing tool to verify models of the new Danish interlocking systems by exploring the locality principles related to the topological layout of the controlled system.
Program:
Wednesday 20 April 2016 - DTU room 101/S09 9:15-9:30 Jørgen Villadsen & Sebastian Alexander Mödersheim: Welcome / The PART Project 9:30-10:00 Burkhart Wolff (Université Paris-Sud, France): Experiences of a Formal Certification Project EURO-MILS - Why is it so hard to get proofs accepted in Common Criteria Projects 10:00-10:30 Burkhart Wolff: Parallel Computing in an Interactive Theorem Prover - Experiences from the Paral-ITP Project 11:00-12:00 Tom Ridge (University of Leicester, UK): Netsem, Ott, Lem, SibylFS and Verified Parsing: Specification and Validation at Scale 13:00-13:45 Carsten Schürmann (ITU): Specifying Security Protocols in Celf 14:00-14:30 Jørgen Villadsen & Anders Schlichtkrull: Computer-Checked Logical Inference Systems 14:30-15:00 Sebastian Alexander Mödersheim & Andreas Viktor Hess: Proving Protocol Security in Isabelle: Towards State and Composition
Abstract for the talk by Tom Ridge: I have worked on several large specification and validation projects (those mentioned in the title), and tools to support these projects. Most recently, the SibylFS project (sibylfs.io) gave a formal semantics to POSIX and real-world file systems. The semantics was extensively validated, which uncovered numerous bugs and strange behaviours in real-world file systems and the POSIX specification itself. Interestingly, we also found errors (at least one of which was serious) in a *formally verified file system*. In this talk I want to discuss these projects, particularly focusing on how they form a coherent body of work. I also want to explicitly state and analyse the assumptions that lie behind this work. Finally, I would like to discuss how I plan to extend this work in the future.
Program:
Friday 18 December 2015 - DTU room 321/033 11:00-12:00 Dmitriy Traytel (Information Security Group, ETH Zurich, Switzerland): Soundness and Completeness Proofs by Coinductive Methods
Abstract: Coinductive methods can produce compact, high-level proofs of key results in logic: the soundness and completeness of proof systems for variations of first-order logic. The results are formalized in the proof assistant Isabelle using the recently introduced support for codatatypes and corecursion. In the talk I will focus on the abstract core of a classical completeness result: a property of possibly infinite derivation trees. The abstract proof can be instantiated for a wide range of Gentzen and tableau systems as well as various flavors of first-order logic. All of this is joint work with Jasmin Blanchette and Andrei Popescu.
Invited speakers:
Program:
Wednesday 23 September 2015 - DTU room 101/S09 09:00-09:15 Jørgen Villadsen: Welcome / The PART Project 09:15-10:15 Alessandro Fantechi: How Formal Modeling Can Address Advanced Issues in Railway Signalling 10:30-11:15 Anne Elisabeth Haxthausen: Combining Domain-specific Methods and Bounded Model Checking in the Railway Domain 11:15-11:45 Michael Reichhardt Hansen: Towards a Realizable Interpretation of a Logic for Traffic Analysis 12:30-13:30 Jasmin C. Blanchette: Towards Formalizing Superposition 13:30-14:00 Anders Schlichtkrull: Formalization of Resolution Calculus in Isabelle 14:00-14:30 Mathias Fleury: Formalization of Ground Inference Systems in Isabelle Thursday 24 September 2015 - DTU room 101/S09 09:00-10:00 Martin Fränzle: Multi-Objective Parameter Synthesis in Probabilistic Hybrid Systems 10:15-10:45 Jørgen Villadsen: Using the Isabelle Proof Assistant for Teaching Logic 10:45-11:15 Steen Vester: Winning Cores in Parity Games 11:15-11:45 Mathias Nygaard Justesen: A Verification Framework Using Parity Games 12:30-13:30 Achim D. Brucker: Isabelle: Not Only a Proof Assistant 13:30-14:00 Sebastian Alexander Mödersheim: Automated Security Proofs in Isabelle 14:00-14:30 Alessandro Bruni: Proving Stateful Injective Agreement with Refinement Types
Program:
Wednesday 25 February 2015 - DTU room 101/S10
12:00-12:05 Opening session
12:15-12:45 Jørgen Villadsen (DTU Compute): Computer-Checked Meta-Logic
Abstract:
Over the past decades there have been several impressive results in computer-checked meta-logic, including the correctness of proof systems for first-order and higher-order logic as well as the first-ever formalization of Gödel's Incompleteness Theorems, recently published by Larry Paulson as a 250+ pages document for the Isabelle proof assistant. I give a brief overview of the research area and discuss the prospects for verified and self-verified systems.
13:00-13:30 Jesper Bengtson (ITU): Software Verification Using Proof Assistants
Abstract:
Proving full functional correctness of software has long been a holy grail for computer scientists. To be able to ease up on testing and also verify that a program follows its specifications to the letter, that no corner case has been overlooked and that no stone has been left unturned, is an exhilarating concept. To realise this goal three things are required. First of all, we must have a specification language that is rich enough to express all properties of programs that we are interested in. Secondly, since proofs of program correctness are typically very large we need a tool that automates as much of the process as possible, provides interactive support when it is not, and ensures that all proofs are valid and that no mistakes have been made. Finally, the verification process needs to find its way into the standard IDEs that are part of the system developers work flow. In this talk I will focus on my work to tackle these three goals by (1) using higher-order separation logic to write specifications for imperative object-oriented programming languages, (2) mechanising these logics in the interactive proof assistant Coq, and (3) developing a verification environment as a plugin for the Java development environment of Eclipse. The talk will be at a high level of abstraction and no expertise in either of these areas is required.
14:00-14:30 Sebastian Alexander Mödersheim (DTU Compute): Integrating Automated and Interactive Protocol Verification (joint work with Achim Brucker, SAP Research)
Abstract:
Several automated protocol verification tools are based on an over-approximation of the set of possible traces. The underlying protocol models are shaped by the needs of automated verification and have subtle assumptions. Also, a complex verification tool may suffer from implementation bugs. Thus, in the worst case a tool could accept some incorrect protocols as being correct. The same risks are also present, but considerably smaller, when using an LCF-style theorem prover like Isabelle. The interactive security proof, however, requires a lot of expertise and time. We look at two approaches that combine the advantages of both worlds, by using automatic tools to generate a "proof idea" for an interactive theorem prover. In the worst case (e.g., a bug) this proof idea will simply not check out in the theorem prover. However, when it succeeds, the correctness only relies on the basic model and the correctness of the "core" of the theorem prover.
14:45-15:15 Ximeng Li (DTU Compute): Coq for Programming Language Proofs - A Personal Experience
Abstract:
This talk is centered around a personal experience on using Coq to develop proofs for a draft paper on information flow security. Instrumented semantics is used to capture the flows arising from computation, and a type system then guarantees that only secure flows are admitted. The Coq development consists of the formulation of the syntax of a simple concurrent language, its instrumented semantics, the security type system, and a soundness result. The development uses mostly elementary to intermediate features of the Coq language and some excerpts of it will be displayed and discussed.
15:30-16:00 Closing session