FMOℤ 2017

Program

Abstracts

Peter Hoefner

Forwards and Backwards in Separation Algebra
(joint work with C. Bannister and G. Klein)

Separation algebra is a formal and abstract algebraic framework to describe separation logic. So far separation algebra was mainly used as an abstract base to reason about heaps. I will present an algebraic framework that allows backward reasoning using weakest preconditions, and forward reasoning using strongest postconditions for separation algebra; and hence also for separation logic. While the former is well understood, the later requires the introduction of a new operator. Since this is work in progress I will point at some surprising algebraic problems that need to be solved within the setting of forward reasoning.

Rajeev Gore

Modular Automated Proof Search in Separation Logics

I will present a labelled sequent calculus which can be tailored for separation logics. I will describe how we developed a method for proof-search using this sequent calculus and describe some experiments that compared it with other proof methods for separation logics. Our work nicely complements the work of Hoefner, Bannister and Klein on building a tool for analysing the correctness of programs based upon separation algebras.

Carroll Morgan

An experiment in data-refinement and atomisation
in rely-guarantee reasoning

Current work in Trustworthy Systems at Data 61 is exploring the extent to which rely/guarantee reasoning can be used for developing concurrent (even multi-core) operating-system code by refinement; and of particular interest is data-refinement and refinement of atomicity. Exploring those issues with a very simple algorithm (but famous: Peterson’s) has uncovered some interesting and unexpected issues, which I will explain.

Rob van Glabbeek

A classification of fairness assumptions

Fairness assumptions are crucial in the verification of liveness properties. In this talk I will present a classification of various fairness assumptions found in the literature, and present examples showing the difference between the various notions. (One point in the classification is our own notion of justness, about which I talked last year.)

Kai Engelhardt

A Better Composition Operator for Quantitative Information Flow Analyses

Given a description of the quantitative information flow (qif) for components, how can we determine the qif of a system composed from components? We explore this fundamental question mathematically and provide an answers based on a new composition operator. We investigate its properties and prove that it generalises existing composition operators. We illustrate the results with a fresh look on Chaum’s dining cryptographers. We show that the new operator enjoys various convenient algebraic properties and that it is well-behaved under composition refinement.

Dirk Pattinson

Schulze Voting as Evidence Carrying Computation

The correctness of vote counting in electronic election is one of the main pillars that engenders trust in electronic elections. However, the present state of the art in vote counting leaves much to be desired: while some jurisdictions publish the source code of vote counting code, others treat the code as commercial in confidence. None of the systems in use today applies any formal verification. In this paper, we formally specify the so-called Schulze method, a vote counting scheme that is gaining popularity on the open source community. The cornerstone of our formalisation is a (dependent, inductive) type that represents all correct executions of the vote counting scheme. Every inhabitant of this type not only gives a final result, but also all intermediate steps that lead to this result, and can so be externally verified. As a consequence, we do not even need trust the execution of the (verified) algorithm: the correctness of a particular run of the vote counting code can be verified on the basis of the evidence for correctness that is produced along with determination of election winners.

Mark Utting

Learning to Make Whiley Boogie!

In this talk, we explore the use of Boogie as an intermediate verification language for verifying programs in Whiley. This is noteworthy because the Whiley language has (amongst other things) a rich type system with considerable potential for an impedance mismatch. We report that, whilst a naive translation to Boogie is unsatisfactory, a more abstract encoding is surprisingly effective.

Sergiy Bogomolov

Towards Scalable Verification of Cyber-Physical Systems

Cyber-physical systems (CPS) are networks of physical and digital components and present a next generation of large-scale highly-interconnected networked embedded systems. On the one hand, CPS open enormous opportunities as they form the core of emerging smart devices and services which are going to revolutionize many traditional industries such as transportation and traffic management, power generation and delivery, as well as manufacturing. On the other hand, highly autonomous systems pose special engineering challenges as any unexpected behaviour might lead to large financial losses or even human deaths.

In this talk, we address this challenge and propose automatic techniques to analyze CPS. For this purpose, we use the concept of hybrid automata which has proven to be particularly useful to model CPS. We give an overview of techniques to ensure efficient analysis of hybrid automata. In particular, we present support-function based representation of region state space and discuss ways to refine it.

Jin Song Dong

Event Analytics

The process analysis toolkit (PAT) integrates the expressiveness of state, event, time, and probability-based languages with the power of model checking. PAT currently supports various modeling languages with many application domains and has attracted thousands of registered users from hundreds of organizations. In this talk, we will present the PAT approach to "Event Analytics" (EA) which is beyond "Data Analytics". The EA research is based on applying model checking to event planning, scheduling, prediction, strategy analysis and decision making. Various EA research directions will be discussed.