Abstract
The ordering of events is a fundamental problem of distributed computing and has been extensively studied over several decades. From all the available orderings, total ordering is of particular interest as it provides a powerful abstraction for building reliable distributed applications. Unfortunately, deterministic total order algorithms scale poorly and are therefore unfit for modern large-scale applications. The main contribution of this paper is EPTO, a total order algorithm with probabilistic agreement that scales both in the number of processes and events. EPTO provides deterministic safety and probabilistic liveness: integrity, total order and validity are always preserved, while agreement is achieved with arbitrarily high probability. We show that EPTO is well-suited for large-scale dynamic distributed systems: it does not require a global clock nor synchronized processes, and it is highly robust even when the network suffers from large delays and significant churn and message loss.

Abstract

Abstract
Temporal logics targeting real-time systems are traditionally undecidable. Based on a restricted fragment of MTL-integral, we propose a new approach for the runtime verification of hard real-time systems. The novelty of our technique is that it is based on incremental evaluation, allowing us to effectively treat duration properties (which play a crucial role in real-time systems). We describe the two levels of operation of our approach: offline simplification by quantifier removal techniques; and online evaluation of a three-valued interpretation for formulas of our fragment. Our experiments show the applicability of this mechanism as well as the validity of the provided complexity results.

Abstract
Program verification tools use verification condition generators to produce logical formulas whose validity implies that the program is correct with respect to its specification. Different tools produce different conditions, and the underlying algorithms have not been properly exposed or explored so far. In this paper we consider a simple imperative programming language, extended with assume and assert statements, to present different ways of generating verification conditions. We study the approaches with experimental results originated by verification conditions generated from the intermediate representation of LLVM.

Abstract
Over the past decades several approaches for schedulability analysis have been proposed for both uni-processor and multi-processor real-time systems. Although different techniques are employed, very little has been put forward in using formal specifications, with the consequent possibility for misinterpretations or ambiguities in the problem statement. Using a logic based approach to schedulability analysis in the design of hard real-time systems eases the synthesis of correct-by-construction procedures for both static and dynamic verification processes. In this paper we propose a novel approach to schedulability analysis based on a timed temporal logic with time durations. Our approach subsumes classical methods for uni-processor scheduling analysis over compositional resource models by providing the developer with counter-examples, and by ruling out schedules that cause unsafe violations on the system. We also provide an example showing the effectiveness of our proposal.

Abstract
The availability of cheap wireless sensors boosted the emergence of unstructured networks using wireless technologies with decentralised administration. However, a simple task such as learning the temperature needs a discovery service to find a thermometer among all the sensors. In general, resource discovery relies on flooding mechanisms that waste energy and compromises system availability. Energy efficient strategies limit the exploration area, but with a significant impact on latency. The paper proposes ABC (Adaptive Broadcast Cancellation), a new algorithm that uses the knowledge acquired in previous discoveries to accelerate queries towards the resource. Knowledge is stored in a variation of Bloom filters, thus contributing for an efficient utilization of the sensors limited memory.