Keynotes

Electronic voting aims at guaranteeing apparently conflicting properties: no one should know how I voted and yet, I should be able to check that my vote has been properly counted. Electronic voting belongs to the large family of security protocols, that aim at securing communications against powerful adversaries that may read, block, and modify messages. In this talk, we will see how to design secure electronic voting protocols and how to analyze them using formal methods, in order to detect attacks at an early stage, or prove security. This yielded several enhancements of ProVerif, a state-of-the-art tool for anaysing security protocols.

The VerCors verifier is a tool set for the verification of parallel and concurrent software. Its main characteristics are (i) that it can verify programs under different concurrency models, written in high-level programming languages, such as for example in Java, OpenCL and OpenMP; and (ii) that it can reason not only about race freedom and memory safety, but also about functional correctness. In this talk I will first give an overview of the VerCors verifier, and how it has been used for the verification of many different parallel and concurrent algorithms. In the second part of my talk I will zoom in on verification of GPU programs, as they are widely used in industry. To obtain the best performance, a typical development process involves the manual or semi-automatic application of optimizations prior to compiling the code. To avoid the introduction of errors, we can augment GPU programs with (pre- and postcondition-style) annotations to capture functional properties. However, keeping these annotations correct when optimizing GPU programs is labor-intensive and error-prone. In my talk I introduce Alpinist, an annotation-aware GPU program optimizer. It applies frequently-used GPU optimizations, but besides transforming code, it also transforms the annotations. We evaluate Alpinist, in combination with the VerCors program verifier, to automatically optimize a collection of verified programs and reverify them.

Simulation is a favoured technique adopted by roboticists to evaluate controller design and software. Often, state machines are drawn to convey overall ideas; they are used as a basis to program tool-specific simulations. The simulation code, written in general or proprietary programming languages, is, however, the only account of the robotic system. In this talk, we present a modern approach to design that supports the automatic generation of simulation code that is guaranteed to be correct, and complements the use of simulation with model checking and theorem proving. This approach, under development by the RoboStar group (https://www.cs.york.ac.uk/robostar/), uses two domain-specific languages: RoboChart and RoboSim. RoboChart includes a controlled subset of UML-like state machines, a customised component-model, and primitives to specify timed and probabilistic properties. RoboChart is an event-based notation for design; RoboSim is a matching cycle-based diagrammatic notation for simulation. RoboSim also includes block diagrams enriched to specify physical and dynamic behaviours of robotic platforms. Both RoboChart and RoboSim can be used to generate automatically mathematical models that can be used for verification. In the RoboStar approach, the mathematical models are hidden from practitioners, but can be used to prove properties of models, and consistency between designs and simulations. We have experience with FDR, PRISM, and Isabelle. RoboChart and RoboSim can complement approaches that cater for a global view of the system architecture by supporting modelling and verification of the functional component-behaviour, covering interaction, time, and probabilistic properties. It also complements work on deployment of verified code.

The development of computerized proofs has led to the development of a variety of set theories and types theories (such as the B set theory, the Calculus of constructions, Simple type theory, etc.) in which these proofs are expressed. After several decades of research on these theories, we understand better their relationship and how proofs can and cannot be translated from one theory to another. This permits to foresee a next step in the development of formal methods, where the same proof can be used in different theories.

Our talk will focus on how we get more people "onboard the FM ship", that is "Formal Methods Considered Normal". Altran has had much success with SPARK, an FM now accepted as normal part of business at Altran. We will elaborate on what has worked and why. We continue to have more challenges with using Z (and similar ABZ languages). We believe that specification structuring is a major discriminating factor for industrial scale-up. We will give examples of structuring idioms that have been especially important for the largest formal specification written by Altran. Our perspective is that of long-term users of FM in all parts of the development life cycle. A significant challenge for us is training and recruiting of specification producers and we see this as requiring a community effort involving industry and academia. We also touch on some of our on-going work on extracting further benefits from FM including automatic natural language generation for improved communication about specifications with all stake holders, and generation of monitors for improved V&V automation (lower cost).

When the field of formal methods began, it had broad and noble goals. But somehow, over time, these goals were eclipsed by a more reductionist view. Nowadays, quality is measured by defect counts, and eliminating bugs has become the central focus of our field. In this talk, I'll explain how I think this came about, why it's insidious, and what we can do about it. My key observation will be that bugs are not the causes of problems but are instead symptoms. To improve our software---to make it more secure, safe and usable---we need to move from symptoms to diagnosis, to determine the underlying causes of poor software and fix those. I will argue that design is essential to achieving this, and that we need to reinvigorate design as a central activity in formal methods research and practice. I will give examples of designs, good and bad, drawn from my ongoing work on conceptual design of software.

After more than 20 years since the publication of my book on B, and almost 10 years since the publication of my book on Event-B, the aim of this talk is to present some key points about these technologies. The talk will cover the basic principles on which B and Event-B have been developed and look at differences and similarities between B and Event-B. It will also outline where B and Event-B are spread around the world. Finally, the talk will explore challenges with the industrial application of these technologies.

A distributed system can be characterised by autonomously acting agents, where each agent executes its own program, uses shared resources and communicates with the others, but otherwise is totally oblivious to the behaviour of the other agents. In a distributed adaptive system agents may change their programs, enter or leave the collection at any time thereby changing the behaviour of the overall system. The talk will start with the motivation of a language-independent axiomatic definition of distributed adaptive systems and then present concurrent reflective Abstract State Machines (crASMs), an abstract machine model for their specification. It can be proven that any system stipulated by the definition can be step-by-step simulated by a crASM. Based on the simple observation that concurrent ASMs can be mimicked by non-deterministic parallel ASMs the complete one-step logic for non-deterministic ASMs can be exploited for the definition of a logic capturing concurrency. By making the extra-logical rules in the logic subject to being interpreted in a state the logic can be extended to capture also reflection.

Plotkin’s structural operational semantics provides a tried and tested method for defining the semantics of a programming language via sets of rules that define valid transitions between program configurations. Mosses’ modular structural operational semantics (MSOS) recasts the approach by making use of rules consisting of labelled transitions, allowing a more modular approach to defining language semantics. MSOS can be adapted by using "syntactic" labels that allow local variables and aliasing to be defined without augmenting the semantics with environments and locations. The syntactic labels allow both state-based constructs of imperative languages and event-based constructs of process algebras to the specified in an integrated manner. To illustrate the integrated approach we compare its rules with Plotkin’s original rules for both small-step and big-step operational semantics. One issue that arises is that defining concurrency requires the use of a small-step approach to handle interleaving, while defining a specification command requires a big-step approach. The integrated approach can be generalised to use a sequence of (small) steps as a label; we call this a multi-step operational semantics. This approach allows both concurrency and non-atomic specification commands to be defined.