ABSTRACT. Sustaining the growing adoption of formal methods requires attention to not only the technical but also the human side. These range from paying more attention to the user interfaces of tools to creating rich environments for education. In this talk, I will discuss some of the challenges and opportunities for human factors in formal methods for the creation of a "formal methods mindset".

ABSTRACT. The problem of determining whether or not a point lies inside a given polygon occurs in many applications. In air traffic management concepts, a correct solution to the point-in-polygon problem is critical to geofencing systems for Unmanned Aerial Vehicles and in weather avoidance applications. Many mathematical methods can be used to solve the point-in-polygon problem. Unfortunately, a straightforward floating-point implementation of these methods can lead to incorrect results due to round-off errors. In particular, these errors may cause the control flow of the program to diverge with respect to the ideal real-number algorithm. This divergence potentially results in an incorrect point-in-polygon determination even when the point is far from the edges of the polygon. This paper presents a provably correct implementation of a point-in-polygon method that is based on the computation of the winding number. This implementation is mechanically generated from a source-to-source transformation of the ideal real-number specification of the algorithm. The transformation soundly approximates Boolean expressions in conditional statements. The correctness of this implementation is formally verified within the Frama-C analyzer, where the proof obligations are discharged using the Prototype Verification System (PVS).

ABSTRACT. When compared to idealized, real-valued arithmetic, finite precision arithmetic introduces unavoidable errors, for which numerous tools compute sound upper bounds. To ensure soundness, providing formal guarantees on these complex tools is highly valuable.

In this paper we extend one such formally verified tool, called FloVer~\cite{} to certify more sophisticated analysis. We extend FloVer with an SMT-based domain trusting results from an external SMT solver. Further, we implement interval subdivision on top of the existing analyses. Our evaluation shows that FloVer can verify more precise bounds while its runtime remains feasible.

ABSTRACT. Chord is a protocol providing a scalable distributed hash table over an underlying peer-to-peer network. It is very popular due to its simplicity, performance and claimed correctness. However, the original version of (the maintenance protocol of) Chord, presented with an informal proof of correctness, was since then shown to be in fact incorrect. It is actually tricky to come up with a provably-correct version as the protocol combines data structures, asynchronous communication, concurrency, and fault tolerance. Besides, the correctness property amounts to a form of stabilization, a particular kind of liveness property. Previous work only addressed automated proofs of safety; and pen-and-paper, or automated but much bounded, proofs of stabilization. In this article, we report on the first mechanized proof of the liveness property for Chord. Furthermore, our proof addresses the full parameterized version of the protocol, weakens previously-devised invariants and operating assumptions, and is essentially automated (requiring limited effort when manual assistance is needed).

ABSTRACT. In this paper, we provide a formal definition of symbolic execution in terms of a symbolic transition system and prove its correctness with respect to an operational semantics which models the execution on concrete values. We first introduce such a formal model for a basic programming language with a statically fixed number of programming variables. This model is extended to a programming language with recursive procedures which are called by a call-by-value parameter mechanism. Finally, we show how to extend this latter model of symbolic execution to arrays and object-oriented languages which feature dynamically allocated variables.

ABSTRACT. Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. GR(1) is an expressive assume-guarantee fragment of LTL that enables efficient synthesis and has been recently used in different contexts and application domains. A common form of providing system’s requirements is through use cases, which are existential in nature. However, GR(1), as a fragment of LTL, is limited to universal properties.

In this paper we introduce GR(1)*, which extends GR(1) with existential guarantees. We show that GR(1)* is strictly more expressive than GR(1) as it enables the expression of guarantees that are inexpressible in LTL. We solve the realizability problem for GR(1)* and present a symbolic strategy construction algorithm for GR(1)* specifications. Importantly, in comparison to GR(1), GR(1)* remains efficient, and induces only a minor additional cost in terms of time complexity, proportional to the extended length of the formula.

ABSTRACT. Probabilistic programs are key to deal with uncertainty in e.g. controller synthesis. They are typically small but intricate. Their development is complex and error prone requiring quantitative reasoning over a myriad of alternative designs. To mitigate this complexity, we adopt counterexample-guided inductive synthesis (CEGIS) to automatically synthesise finite-state probabilistic programs. Our approach leverages efficient model checking, modern SMT solving, and counterexample generation at program level. Experiments on practically relevant case studies show that design spaces with millions of candidate designs can be fully explored using a few thousand verification queries.

ABSTRACT. We present an optimization-based synthesis method for laying out railway signalling components on a given track infrastructure to fulfill capacity specifications. The specifications and the optimization method are aimed towards the scope of signalling construction projects and their associated interlocking systems.

The main synthesis algorithm starts from an initial heuristic over-approximation of required signalling components and iterates towards better designs using two main optimization techniques: (1) global simultaneous planning of all operational scenarios using incremental SAT-based optimization to eliminate redundant signalling components, and (2) a derivative-free numerical optimization method using as cost function timing results given by a discrete event simulation engine.

Synthesizing all of the signaling layout might not always be appropriate in practice, and partial synthesis from an already valid design can be an alternative. In consequence, we focus also on the usefulness of the individual optimization steps: SAT-based planning is used to suggest removal of redundant signaling components, whereas numerical optimization of timing results is used to suggest moving signaling components around on the layout, or adding new components. Such changes are suggested to railway engineers using an interactive tool where they can investigate the consequences of applying the various optimizations.

ABSTRACT. Continuous invariants are an important ingredient for deductive verification of hybrid and continuous systems. Just like discrete invariants are used to reason about correctness in discrete systems without unrolling their loops forever, continuous invariants are used to reason about differential equations without having to solve them. Automatic generation of continuous invariants remains one of the biggest practical challenges for automating formal proofs of safety for hybrid systems.There are at present many disparate methods available for generating continuous invariants; however, this wealth of diverse techniques presents a number of challenges, with different methods having different strengths and weaknesses. To address some of these challenges, we develop Pegasus: an automatic continuous invariant generator which allows for combinations of various methods, and integrate it with the KeYmaera X theorem prover. We describe some of the architectural aspects of this integration, comment on its methods and challenges, and present an experimental evaluation on a suite of benchmarks.

ABSTRACT. Reactive systems are composed of a well defined set of event handlers by which the system responds to environment stimulus. In concurrent environments, event handlers can interact with the execution of other handlers such as hardware interruptions in preemptive systems, or other instances of the reactive system in multicore architectures. The rely-guarantee technique is a suitable approach for the specification and verification of reactive systems. However, the languages in existing rely-guarantee implementations are designed only for ``pure programs'', simulating reactive systems makes the program and rely-guarantee conditions unnecessary complicated. In this paper, we decouple the system reactions and programs using a rely-guarantee interface, and develop PiCore, a parametric rely-guarantee framework for concurrent reactive systems. PiCore has a two-level inference system to reason on events and programs associated to events. The rely-guarantee interface between the two levels allows the reusability of existing languages and their rely-guarantee proof systems for programs. In this work we show how to integrate in PiCore two existing rely-guarantee proof systems. This work has been fully mechanized in Isabelle/HOL. As a case study, we have applied PiCore to the concurrent buddy memory allocation of a real-world OS, providing a verified low-level specification and revealing bugs in the C code.

ABSTRACT. Non-volatile memory (NVM), aka persistent memory, is a new paradigm for memory preserving its contents even after power loss. The expected ubiquity of NVM has stimulated interest in the design of persistent concurrent data structures, together with associated notions of correctness. In this paper, we present the first formal proof technique for durable linearizability, which is a correctness criterion that extends linearizability to handle crashes and recovery in the context of NVM. Our proofs are based on refinement of IO-automata representations of concurrent data structures. To this end, we develop a generic procedure for transforming any standard sequential data structure into a durable specification. Since the durable specification only exhibits durably linearizable behaviours, it serves as the abstract specification in our refinement proof. We exemplify our technique on a recently proposed persistent memory queue that builds on Michael and Scott’s lock-free queue.

ABSTRACT. Compositional verification is a promising technique for analyzing action-based temporal properties of concurrent systems. One approach to verify a property expressed as a modal mu-calculus formula on a system with several concurrent processes is to build the underlying state space compositionally (i.e., by minimizing and recomposing the state spaces of individual processes, keeping visible only the relevant actions occurring in the formula), and check the formula on the resulting state space. It was shown previously that, when checking the formulas of the L-mu-dsbr fragment of mu-calculus (consisting of weak modalities only), individual processes can be minimized modulo divergence-sensitive branching (divbranching) bisimulation. In this paper, we refine this approach to handle formulas containing both strong and weak modalities, so as to enable a combined use of strong or divbranching bisimulation minimization on concurrent processes depending whether they contain or not the actions occurring in the strong modalities of the formula. We extend the existing L-mu-dsbr fragment with strong modalities and show that the combined minimization approach preserves the truth value of formulas of the extended fragment. We implemented this approach on top of the CADP verification toolbox and demonstrated how it improves the capabilities of compositional verification on realistic examples of concurrent systems.

ABSTRACT. The last decade has seen a dramatic growth in the use of constraint solvers as a computational mechanism, not only for analysis of software, but also at runtime. Solvers are available for a variety of logics but are generally restricted to first-order formulas. Some tasks, however, most notably those involving synthesis, are inherently higher order; these are typically handled by embedding a first-order solver (such as a SAT or SMT solver) in a domain-specific algorithm. Using strategies similar to those used in such algorithms, we show how to extend a first-order solver (in this case Kodkod, a model finder for relational logic used as the engine of the Alloy Analyzer) so that it can handle quantifications over higher-order structures. The resulting solver is sufficiently general that it can be applied to a range of problems; it is higher order, so that it can be applied directly, without embedding in another algorithm; and it performs well enough to be competitive with specialized tools. Just as the identification of first-order solvers as reusable backends advanced the performance of specialized tools and simplified their architecture, factoring out higher-order solvers may bring similar benefits to a new class of tools.

ABSTRACT. Among several approaches aiming at the correctness of systems, model-checking is one technique to formally assess system models regarding their desired/undesired behavioural properties. We aim at model-checking the Circus notation that combines Z, CSP, and Morgan's refinement calculus, based on the Unifying Theories of Programming. In this paper, we experiment approaches for capturing Circus processes in CSP, and for each approach, we evaluate the impact of our decisions on the state-space explored as well as the time spent for such a checking using FDR. We also experimented the consequences of model-checking CSP models that capture both state invariants and preconditions of Circus models.

ABSTRACT. In this paper, we introduce Circus2CSP, a tool that automatically translates Circus into CSPm, with an implementation based on a published manual translation scheme. This scheme includes new and modified translation rules that emerged as a result of experimentation. We addressed issues with FDR state-space explosion, by optimising our models using the Circus Refinement Laws. We briefly describe the usage of Circus2CSP along with a discussion of some experiments comparing our tool with the literature.