Abstract Knowledge-based programs specify multi-agent protocols with epistemic guards that abstract from how agents learn and record facts or information about other agents and the environment. Their interpretation involves a non-monotone mutual dependency between the evaluation of epistemic guards over the reachable states and the derivation of the reachable states depending on the evaluation of epistemic guards. We apply the technique of a must/cannot analysis invented for synchronous programming languages to the interpretation problem of knowledge-based programs and demonstrate that the resulting constructive interpretation is monotone and has a least fixed point. We relate our approach with existing interpretation schemes for both synchronous and asynchronous programs. Finally, we describe an implementation of the constructive interpretation and illustrate the procedure by several examples and an application to the Java memory model.

In software-defined networks (SDN), a controller program is in charge of deploying diverse network functionality across a large number of switches, but this comes at a great risk: deploying buggy controller code could result in network and service disruption and security loopholes. The automatic detection of bugs or, even better, verification of their absence is thus most desirable, yet the size of the network and the complexity of the controller makes this a challenging undertaking. In this paper, we propose MOCS, a highly expressive, optimised SDN model that allows capturing subtle real-world bugs, in a reasonable amount of time. This is achieved by (1) analysing the model for possible partial order reductions, (2) statically pre-computing packet equivalence classes and (3) indexing packets and rules that exist in the model. We demonstrate its superiority compared to the state of the art in terms of expressivity, by providing examples of realistic bugs that a prototype implementation of MOCS in Uppaal caught, and performance/scalability, by running examples on various sizes of network topologies, highlighting the importance of our abstractions and optimisations.

Software-defined networking (SDN) enables advanced operation and management of network deployments through (virtually) centralised, programmable controllers, which deploy network functionality by installing rules in the flow tables of network switches.Although this is a powerful abstraction, buggy controller functionality could lead to severe service disruption and security loopholes, motivating the need for (semi-)automated tools to find, or even verify absence of, bugs.Model checking SDNs has been proposed in the literature, but none of the existing approaches can support dynamic network deployments, where flow entries expire due to timeouts.This is necessary for automatically refreshing (and eliminating stale) state in the network (termed as soft-state in the network protocol design nomenclature), which is important for scaling up applications or recovering from failures.In this paper, we extend our model (MoCS) to deal with timeouts of flow table entries, thus supporting soft state in the network.Optimisations are proposed that are tailored to this extension.We evaluate the performance of the proposed model in UPPAAL using a load balancer and firewall in network topologies of varying size.

Frame and anti-frame rules have been proposed as proof rules for modular reasoning about programs. Frame rules allow the hiding of irrelevant parts of the state during verification, whereas the anti-frame rule allows the hiding of local state from the context. We discuss the semantic foundations of frame and anti-frame rules, and present the first sound model for Charguéraud and Pottier's type and capability system including both of these rules. The model is a possible worlds model based on the operational semantics and step-indexed heap relations, and the worlds are given by a recursively defined metric space. We also extend the model to account for Pottier's generalised frame and anti-frame rules, where invariants are generalised tofamiliesof invariants indexed over preorders. This generalisation enables reasoning about some well-bracketed as well as (locally) monotone uses of local state.

Computational reflection allows a program to inspect and manipulate the structure or behaviour of itself at runtime. Often this means that it is possible to create more generic or adaptable programs in an elegant way. However, there is little support for specification and automatic verification of reflective programs. We address this problem by implementing, specifying, and verifying a reflective library using a Hoare-logic for a simple language with stored procedures. The latter is important since reflective metadata is modelled on the heap, thus method objects will be realised as stored procedures. We verify memory safety as well as functional correctness of an instance of the reflective visitor pattern, including the reflective library. The entire verification is carried out in our (semi-)automatic verification tool Crowfoot.

Over the last decade, there has been extensive research on modelling challenging features in programming languages and program logics, such as higher-order store and storable resource invariants. A recent line of work has identified a common solution to some of these challenges: Kripke models over worlds that are recursively defined in a category of metric spaces. In this paper, we broaden the scope of this technique from the original domain-theoretic setting to an elementary, operational one based on step indexing. The resulting method is widely applicable and leads to simple, succinct models of complicated language features, as we demonstrate in our semantics of Charguéraud and Pottier's type-and-capability system for an ML-like higher-order language. Moreover, the method provides a high-level understanding of the essence of recent approaches based on step indexing.

This special issue of Mathematical Structures in Computer Science contains six papers from the Workshop on Domains IX held at the University of Sussex (Brighton), on 22–24 September 2008. This was the ninth event in the long tradition of Domains workshops, which started in Darmstadt in 1994. Since then, workshops have been organised in Braunschweig (1996), Munich (1997), Siegen (1998), Darmstadt again (1999, 2004), Birmingham (2002) and Novosibirsk (2007).

The object-calculus is an imperative and object-based programming language in which every object comes equipped with its own method suite. Consequently, methods need to reside in the store (‘higher-order store’), which complicates the semantics. Abadi and Leino defined a program logic for this language enriching object types by method specifications. We present a new soundness proof for their logic using denotational semantics. It turns out that denotations of store specifications are predicates defined by mixed-variant recursion. A benefit of our approach is that derivability and validity can be kept distinct. Moreover, it reveals which of the limitations of Abadi and Leino's logic are incidental design decisions and which follow inherently from the use of a higher-order store. We discuss the implications for the development of other, more expressive, program logics.

The main contribution of this paper is a formal characterization of recursive object specifications based on a denotational untyped semantics of the object calculus and the discussion of existence of those (recursive) specifications. The semantics is then applied to prove soundness of a programming logic for the object calculus and to suggest possible extensions. For the purposes of this discussion we use an informal logic of predomains in order to avoid any commitment to a particular syntax of specification logic.

One of the goals of this paper is to demonstrate that denotational semantics is useful for operational issues like implementation of functional languages by abstract machines. This is exemplified in a tutorial way by studying the case of extensional untyped call-by-name λ-calculus with Felleisen's control operator [Cscr ]. We derive the transition rules for an abstract machine from a continuation semantics which appears as a generalization of the ¬¬-translation known from logic. The resulting abstract machine appears as an extension of Krivine's machine implementing head reduction. Though the result, namely Krivine's machine, is well known our method of deriving it from continuation semantics is new and applicable to other languages (as e.g. call-by-value variants). Further new results are that Scott's D ∞ -models are all instances of continuation models. Moreover, we extend our continuation semantics to Parigot's λμ-calculus from which we derive an extension of Krivine's machine for λμ-calculus. The relation between continuation semantics and the abstract machines is made precise by proving computational adequacy results employing an elegant method introduced by Pitts.