ABSTRACT. Reasoning about the correctness of concurrent objects on weak memory models supported by modern multicore architectures is complicated. Traditional notions such as linearizability do not directly apply as the effect of an operation can become visible after the operation call has returned.

In this paper we develop a theory for correctness of concurrent objects under weak memory models. Central to our definitions is the concept of observations which determine when effects of operations become visible, and hence determine the semantics of objects, under a given memory model. The resulting notion of correctness, called object refinement, is generic as it is parameterised by the memory model under consideration. Our theory enforces the minimal constraints on the placing of observations and on the semantics of objects that underlie object refinement. Object refinement is suitable as a reference for correctness when proving new proof methods for objects under weak memory models to be sound and complete.

ABSTRACT. The purpose of this paper is to review some of the challenges of formally specifying components of concurrent programs in a manner suitable for refining them to an implementation. We present some approaches to devising specifications, in some cases investigating different forms of specification suitable for different contexts. Our focus is on shared variable concurrency rather than event-based process algebras.

ABSTRACT. To derive a program for a given specification R means to find an artifact P that satisfies two conditions: P is executable in some programming language; and P is correct with respect to R. Refinement-based program derivation achieves this goal in a stepwise manner by enhancing executability while preserving correctness until we achieve complete executability. In this paper, we argue that it is possible to invert these properties, and to derive a program by enhancing correctness while preserving executability (i.e. proceeding from one executable program to another) until we achieve absolute correctness. Of course, this latter process is possible only if we know what it means to enhance correctness.

ABSTRACT. Software is now ubiquitous and involved in complex interactions with the human users and the physical world in so-called cyber-physical systems (CPS) where the management of time is a major issue. Separation of concerns is a key asset in the development of these ever more complex systems. Two different kinds of separation exist : a first one corresponds to the different steps in a development leading from the abstract requirements to the system implementation and is qualified as vertical. It matches the commonly used notion of refinement. A second one corresponds to the various components in the system architecture at a given level of refinement and is called horizontal. Refinement has been studied thoroughly for the data, functional and concurrency concerns while our work focuses on the time modeling concern. This contribution aims at providing a formal construct for the verification of vertical separation in time models, through the definition of an order between strict partial orders used to relate the different instants in asynchronous systems. This work has been conducted using the proof assistant Agda and is connected to a previous work on the asynchronous language CCSL, which has also been modeled using the same tool.

ABSTRACT. Over the past decades we have developed formal frameworks to refine specifications into more detailed representations. These handle both deterministic and probabilistic specifications. We also have developed means for relaxing formality when the occasion demands it (retrenchment).  In this talk I will explore approaches to inferring programs from test data (derived from a specification), particularly involving  the use of genetic programming (GP). I will pay particular attention to quantum artifacts, e.g. discussing how GP can find Shor's Quantum Discrete Fourier Transform circuits.  Such approaches generally work by 'homing in' on an appropriate program, using deviation of results from specified results as guidance. This can produce programs that are either right or nearly right. I'll do a round trip with evolutionary computation and indicate the use of GP in unearthing formal specification fragments from test traces for traditional programs (using mutation approaches to get rid of uninteresting potential invariants inferred).

ABSTRACT. The Santa Claus Problem is an intricate exercise for concurrent programming. This paper outlines the refinement step to develop a highly efficient implementation with concurrent objects, starting from a very simple specification. The efficiency of the implementation is compared to three other languages.

ABSTRACT. We present a theory of lazy imperative timing.