ABSTRACT. This research started with an algebra for reasoning about rely/guarantee concurrency for a shared memory model. The approach taken led to a more abstract algebra of atomic steps, in which atomic steps synchronise (rather than interleave) when composed in parallel. The algebra of rely/guarantee concurrency then becomes an interpretation of the more abstract algebra. Many of the core properties needed for rely/guarantee reasoning can be shown to hold in the abstract algebra where their proofs are simpler and hence allow a higher degree of automation. Moreover, the realisation that the synchronisation mechanisms of standard process algebras, such as CSP and CCS/SCCS, can be interpreted in our abstract algebra gives evidence of its unifying power. The algebra has been encoded in Isabelle/HOL to provide a basis for tool support.

ABSTRACT. Weak memory models determine the behavior of concurrent programs. While they are often understood in terms of reorderings that the hardware or the compiler may perform, their formal definitions are typically given in a very different style---either axiomatic or operational. In this paper, we investigate to what extent weak behaviors of existing memory models can be fully explained in terms of reorderings and other program transformations. We prove that TSO is equivalent to a set of two local transformations over sequential consistency, but that non-multi-copy-atomic models (such as C11, Power and ARM) cannot be explained in terms of local transformations over sequential consistency. We then show that transformations over a basic non-multi-copy-atomic model account for the relaxed behaviors of (a large fragment of) Power, but that ARM's relaxed behaviors cannot be explained in a similar way. Our positive results may be used to simplify correctness of compilation proofs from a high-level language to TSO or Power.

ABSTRACT. Error invariants are assertions that over-approximate the reachable program states at a given position in an error trace while only capturing states that will still lead to failure if execution of the trace is continued from that position. Such assertions reflect the effect of statements that are involved in the root cause of an error and its propagation, enabling slicing of statements that do not contribute to the error. Previous work on error invariants focused on sequential programs. We generalize error invariants to concurrent traces by augmenting them with additional information about hazards such as write-after-write events, which are often involved in race conditions and atomicity violations. By providing the option to include varying levels of details in error invariants---such as hazards and branching information---our approach allows the programmer to systematically analyze individual aspects of an error trace. We have implemented a hazard-sensitive slicing tool for concurrent traces based on error invariants and evaluated it on benchmarks covering a broad range of real-world concurrency bugs. Hazard-sensitive slicing significantly reduced the length of the considered traces and still maintained the root causes of the concurrency bugs.

ABSTRACT. Linearizability is a commonly accepted notion of correctness for libraries of concurrent algorithms, and recent years have seen a number of proposals of program logics for proving it. Although these logics differ in technical details, they embody similar reasoning principles. To explicate these principles, we propose a logic for proving linearizability that is generic: it can be instantiated with different means of compositional reasoning about concurrency, such as separation logic or rely-guarantee. To this end, we generalise the Views framework for reasoning about concurrency to handle relations between programs, required for proving linearizability. We present sample instantiations of our generic logic and show that it is powerful enough to handle concurrent algorithms with challenging features, such as helping.

ABSTRACT. A software specification is often the result of an iterative process that transforms an initial incomplete model through refinement decisions. A model is incomplete because the implementation of certain functionalities is postponed to a later development step or is delegated to third parties. An unspecified functionality may be later replaced by alternative solutions, which may be evaluated to analyze tradeoffs. Model checking has been proposed as a technique to verify that a model of the system under development is compliant with a formal specification of its requirements. However, most classical model checking approaches assume that a complete model of the system is given: they do not support incompleteness. A verification-driven design process would instead benefit from the ability to apply formal verification at any stage, hence also to incomplete models. After any change, it is desirable that only the portion affected by the change, called replacement, is analyzed. To achieve this goal, this paper extends the classical automata-based model checking procedure to deal with incompleteness. The proposed model checking approach is able not only to evaluate if a property definitely holds, possibly holds or does not hold in an incomplete model but, when the satisfaction of the specification depends on the incomplete parts, to compute the constraints that must be satisfied by their future replacements. Constraints are properties on the unspecified components that, if satisfied by the replacement, guarantee the satisfaction of the original specification in the refined model. Each constraint is verified in isolation on the correspondent replacement.

ABSTRACT. Bifurcation analysis is a central task of the analysis of parameterised high-dimensional dynamical systems that undergo transitions as parameters are changed. The classical numerical and analytical methods are typically limited to a small number of system parameters. In this paper we propose a novel approach to bifurcation analysis that is based on a suitable discrete abstraction of the system and employs model checking for discovering critical parameter values, referred to as bifurcation points, for which various kinds of behaviour (equilibrium, cycling) appear or disappear. To describe such behaviour patterns, called phase portraits, we use a hybrid version of a CTL logic augmented with direction formulae. We demonstrate the method on a case study taken from systems biology.

ABSTRACT. We address the problem of proving the equivalence of two recursive functions that have different base-cases and/or are not in lock-step. None of the existing software equivalence checkers (like Reve, RVT, Symdiff), or general unbounded software model-checkers (like Seahorn, HSF{C}, Automizer) can prove such equivalences. We show a proof rule for the case of different base cases, based on separating the proof into two parts---inputs which result in the base case in at least one of the two compared functions, and all the rest. We also show how unbalanced unrolling of the functions can solve the case in which the functions are not in lock-step. In itself this type of unrolling may again introduce the problem of the different base cases, and we show a new proof rule for solving it. We implemented these rules in our regression-verification tool RVT. We conclude by comparing our approach to that of Felsig et al.'s counterexample-based refinement, which was implemented lately in their equivalence checker Reve.

ABSTRACT. In earlier work, we were the first to investigate the potential of using graphics processing units (GPUs) to speed up explicit-state model checking. Back then, the conclusion was clearly that this potential exists, having measured speed-ups of around 10 times, compared to state-of-the-art single-core model checking. In this paper, we present a new version of our GPU model checker, GPUexplore. Since publication of our earlier work, we have identified and implemented several approaches to improve the performance of the model checker considerably. These include enhanced lock-less hashing of the states and improved thread synchronizations. We discuss experimental results that show the impact of both the progress in hardware in the last few years and our proposed optimisations. The new version of GPUexplore running on state-of-the-art hardware is on average 119 times faster than a sequential implementation and 6 times than the previous version of the tool running on the same hardware.

ABSTRACT. We address the problem of parameter synthesis for parametric timed systems (PTS). The problem is motivated by industrial parameter configuration problems for production lines. Our method consists in compositionally generating over-approximations for the individual components of the input systems, which are translated, together with global properties, to EFSMT problems. Our translations to EFSMT form the basis for optimised and robust parameter synthesis for slightly richer models than PTS.

ABSTRACT. This paper presents a linear programming (LP) relaxation based approach for generating polynomial barrier certificates for safety verification of semi-algebraic hybrid systems. The key idea is to introduce an LP relaxation to encode the set of nonnegativity constraints derived from the conditions of the associated barrier certificates and then resort to LP solvers to find the solutions. The most important benefit of the LP relaxation based approach is that it possesses a much lower computational complexity and hence can be solved very efficiently, which is demonstrated by the theoretical analysis on complexity as well as the experiment on a set of examples gathered from the literature. As far as we know, it is the first method that enables LP relaxation based polynomial barrier certificate generation.

ABSTRACT. Hybrid Communicating Sequential Processes (HCSP) is a powerful formal modeling language for hybrid systems, which is an extension of CSP by introducing differential equations for modeling continuous evolution and interrupts for modeling interaction between continuous and discrete dynamics. In this paper, we investigate the semantic foundation for HCSP from an operational point of view by proposing the notion of approximate bisimulation, which provides an appropriate criterion to characterize the equivalence between HCSP processes with continuous and discrete behaviour. We give an algorithm to determine whether two HCSP processes are approximately bisimilar. In addition, based on which, we propose an approach on how to discretize HCSP, i.e., given an HCSP process A, we construct another HCSP process B which does not contain any continuous dynamics such that A and B are approximately bisimilar with given precisions. This provides a rigorous way to transform a verified control model to a correct program model, which fills the gap in the design of embedded systems.

ABSTRACT. Hybrid systems exhibit both continuous and discrete behavior. Analyzing hybrid systems is known to be hard. Inspired by the idea of concolic testing (of programs), we investigate whether we can combine random sampling and symbolic execution in order to effectively verify hybrid systems. We identify a sufficient condition under which such a combination is more effective than random sampling. Furthermore, we analyze different strategies of combining random sampling and symbolic execution and propose an algorithm which allows us to dynamically switch between them so as to reduce the overall cost. Our method has been implemented as a web-based checker named HyChecker. HyChecker has been evaluated with benchmark hybrid systems and a water treatment system in order to test its effectiveness.

ABSTRACT. In this paper, we propose a novel symbolic approach to automatically synthesize a Hybrid Automaton (HA) from a switched electrical network. The input network consists of a set of physical components interconnected according to some reconfigurable network topology. The underlying model defines a local dynamics for each component in terms of a Differential-Algebraic Equation (DAE), and a set of network topologies by means of discrete switches. Each switch configuration induces a different topology, where the behavior of the system is a Hybrid Differential-Algebraic Equations.

Two relevant problems for these networks are validation and reformulation. The first consists of determining if the network admits an Ordinary Differential Equations (ODE) that describes its dynamics; the second consists of obtaining such ODE from the initial DAE. This step is a key enabler to use existing formal verification tools that can cope with ODEs but not with DAEs.

Since the number of network topologies is exponential in the number of switches, first, we propose a technique based on Satisfiability Modulo Theories (SMT) that can solve the validation problem symbolically, avoiding the explicit enumeration of the topologies. Then, we show an SMT-based algorithm that reformulates the network into a symbolic HA. The algorithm avoids to explicitly enumerate the topologies clustering them by equivalent continuous dynamics.

We implemented the approach with several optimizations and we compared it with the explicit enumeration of configurations. The results demonstrate the scalability of our technique.

ABSTRACT. The paper is motivated by non-deterministic synchronizations in MPI (Message Passing Interface), where some send operations and collective operations may or may not synchronize; a correctly written MPI program should count with both options. Here we focus on the deadlock detection in such systems and propose the following reduction of the explored state space. The system is first analyzed without forcing the respective synchronizations, by applying standard partial-order reduction methods. Then a suggested post-processing algorithm is used that searches for potentially missed deadlocks caused by synchronization. In practical examples this approach leads to major reductions of the explored state-space in comparison to encoding the synchronization options into the state-space search directly. The algorithm is presented as a stand-alone abstract framework that can be also applied to the future versions of MPI as well as to other related problem domains.

ABSTRACT. We combine a prior incomplete deadlock-freedom-checking approach with two new reachability tests to create a more precise deadlock-freedom-checking technique for concurrent systems. The reachability tests that we propose are based on the analysis of individual components of the system; we use static analysis to summarise the behaviour that might lead components to this system state, and we analyse this summary to assess whether components can cooperate to reach this system state. We implement this new framework on a tool called DeadlOx. This implementation encodes the proposed imprecise-deadlock search as a satisfiability problem that is later checker by a SAT solver. We demonstrate by a series of practical experiments that this tool is more accurate than (and as efficient as) similar incomplete techniques for deadlock-freedom analysis.

ABSTRACT. Static analysers search for overapproximating proofs of safety commonly known as safety invariants. Fundamentally, such analysers summarise traces into sets of states, thus trading the ability to distinguish traces for computational tractability. Conversely, static bug finders (e.g. Bounded Model Checking) give evidence for the failure of an assertion in the form of a counterexample, which can be inspected by the user. However, static bug finders fail to scale when analysing programs with bugs that require many iterations of a loop as the computational effort grows exponentially with the depth of the bug. We propose a novel approach for finding bugs, based on the concept of danger invariants - the dual to safety invariants. Danger invariants summarise sets of traces that are guaranteed to reach an error state. We present a second-order formulation of danger invariants and present an implementation of the solver to compute danger invariants for intricate programs taken from the Competition on Software Verification SV-COMP 2016.

ABSTRACT. We present a sequent-based deductive system for automatically proving entailments in separation logic with general inductive heap predicates by mathematical induction. Our induction technique, called mutual explicit induction proof, is an instance of Noetherian induction. Specifically, we propose a novel induction principle on a well-founded relation of separation logic model. We follow the explicit induction methods by implementing the proposed induction principle as inference rules, so that it can be easily integrated into a deductive system. We also support mutual induction, a natural feature of implicit induction, where the goal entailment and other entailments derived during proof search can be used as hypotheses to prove each other. We have implemented a prototype prover and evaluated it on benchmarks from a separation logic competition.

ABSTRACT. The need to get some confidence in binary programs without access to their source code has pushed efforts forward to analyze executable programs. However, low-level programs lack all handy structures compared to their source-level counterparts preventing the straightforward application of source-code analysis techniques. Especially, guarded jumps rely only on flag predicates, whereas they very often encode high-level "natural" conditions on program variables. Simple static analyzers are unable to learn more about high-level operands leading to embarrassing loss of precision. In this paper, we propose a new and sound approach to retrieve high-level predicates from their flag versions in a platform-independent and fully automatic way.This approach allows more precise analyses and helps to understand machine encoding of conditionals rather than relying on human error-prone interpretation.

ABSTRACT. This paper describes formal specification and verification of Lamport's Multi-Paxos algorithm for distributed consensus. The specification is written in TLA+, Lamport's Temporal Logic of Actions. The proof is written and checked using TLAPS, a proof system for TLA+. Building on Lamport, Merz, and Doligez's specification and proof for Basic Paxos, we aim to facilitate the understanding of Multi-Paxos and its proof by minimizing the difference from those for Basic Paxos, and to demonstrate a general way of proving other variants of Paxos and other sophisticated distributed algorithms. We also discuss our general strategies for proving properties about sets and tuples that helped the proof check succeed in significantly reduced time.