ABSTRACT. In this talk, we report on an on-going project, VOCaL, which aims at building formally-verified general-purpose OCaml libraries of data structures and algorithms. We present the various ingredients of this project. First, we introduce GOSPEL, a specification language for OCaml. It resembles existing behavioral specification languages (e.g. JML, ACSL, SPARK), yet departs from them on several points. Second, we describe techniques and tools to perform deductive verification of GOSPEL-specified OCaml code. Currently, this is built on top of three existing tools, namely Why3, CFML and Coq. Last, we report of the successful verification of the first OCaml modules of the VOCaL library. This includes general-purpose data structures such as resizable arrays, hash tables, priority queues, and union-find.

Jean-Christophe Filliâtre is a senior researcher at CNRS. He works at University Paris Sud in Orsay, France. He is chair of IFIP working group 1.9/ 2.15 “Verified Software”. His Ph.D. (1999) was related to the verification of imperative programs using interpretations in type theory, within the framework of the Coq proof assistant. It soon evolved into a tool of its own, known as Why3, where deductive program verification can be performed with the help of many off-the-shelf theorem provers. Jean-Christophe Filliâtre has been working on Why3 since 2001.

ABSTRACT. Software systems undergo several changes along their life-cycle and hence, their models may become outdated. To tackle this issue, we propose an efficient algorithm for adaptive learning, called partial-Dynamic L*M (∂L*M); that improves upon the state-of-the-art by exploring observation tables on-the-fly to discard redundant prefixes and deprecated suffixes. Using 18 versions of the OpenSSL toolkit, we compare our proposed algorithm along with three adaptive algorithms. For the existing algorithms in the literature, our experiments indicate a strong positive correlation between number of membership queries and temporal distance between versions and; for our algorithm, we found a weak positive correlation between membership queries and temporal distance and a significantly lower number of membership queries. These findings indicate that, compared to the state-of-the-art algorithms, our ∂L*M algorithm is less sensitive to software evolution and more efficient than the current approaches for adaptive learning.

ABSTRACT. In Cyber-Physical Systems, the software components are often distributed over several computing nodes, connected by a communication network. Depending on several factors, the behavior of these components may dynamically change during its execution. The existing data flow formalisms for the performance prediction of dynamic systems do not cover the real-time constraints of these systems, and suffer from complexity issues in the verification of mandatory model properties. To overcome these limitations, we propose a dynamic extension to Polygraph, a static data flow formalism covering the real-time behavior of the CPS components. We also propose a verification algorithm to determine if the transitions between different modes are well-defined for a given model. Initial experiments show that this algorithm can be efficiently applied in practice.

ABSTRACT. We propose a novel approach to parameter synthesis for parametrised Kripke structures and CTL specifications. In our method, we suppose the parameterisations form a semi-algebraic set and we utilise a symbolic representation using the so-called cylindrical algebraic decomposition of corresponding multivariate polynomials. Specifically, we propose a new data structure allowing to compute and efficiently manipulate such representations. The new method is significantly faster than our previous method based on SMT. We apply the method to a set of rational dynamical systems representing complex biological mechanisms with non-linear behaviour.

ABSTRACT. This paper is a short version of the authors’ journal article “Dynamic Structural Operational Semantics”, by Christian Johansen and Olaf Owe, in Journal of Logical and Algebraic Methods in Programming, vol 107, pages 79-107, June 2019.

The journal paper develops the theory of Dynamic Structural Operational Semantics (DSOS or Dynamic SOS) as a framework for describing semantics of programming languages that include dynamic software upgrades. DSOS is built on top of the Modular SOS since it allows a sharp separation of the program execution code from the additional structures needed at run-time. DSOS follows the same modularity and decoupling that MSOS advocates, partly motivated by the long term goal of having machine-checkable proofs for general results like type safety.

Dynamic SOS has been applied on two languages supporting dynamic software upgrades, namely the C-like Proteus, which supports updating of variables, functions, records, or types at specific program points, and Creol, which supports dynamic class upgrades in the setting of concurrent objects. Existing type analyses for software upgrades can be done on top of DSOS too, as we illustrate for Proteus.

ABSTRACT. In concurrent object models, objects encapsulate local state, schedule local processes, interact via asynchronous method calls, and methods of different objects are executed concurrently. In this paper, we introduce a compositional trace semantics for concurrent objects and provide an axiomatic characterization of the general properties of reachable traces, that is, traces that can be generated by a concurrent object program. The main result of this paper is a soundness and completeness proof of the axiomatic characterization.

ABSTRACT. Read and write dependences of program variables are essential to determine whether and how a loop or a whole program can be parallelized. State-of-the-art tools for parallelization use approaches that over- as well as under-approximate to compute dependences and they lack a formal foundation. In this paper, we give a formal semantics of read and write dependences and present a program logic that is able to reason about dependences soundly and with full precision. The approach has been implemented in the deductive verification tool KeY for the target language Java.

ABSTRACT. Multiparty Session Types (MPST) are a type formalism used to model communication protocols among components in distributed systems, by specifying type and direction of data transmitted. It is standard for multiparty session type systems to use access control based on linear or affine types. While useful in offering strong guarantees of communication safety and session fidelity, linearity (resp. affinity) run into the well-known problem of inflexible programming, excluding scenarios that make use of shared channels or need to store channels into shared data structures.

In this paper, we develop capability-based access control for multiparty session types. In this setting, channels are split into two entities, the channel itself and the capability of using it. This gives rise to a more flexible session type system, which allows channel references to be shared and stored in persistent data structures. We prove that the resulting language retains session fidelity and illustrate it through a producer-consumer example.

ABSTRACT. An important consequence of only having value types in an aliasing-free programming language is the significant reduction in annotation burden to verify programs using semi-automatic proof systems. However, values in such language are often copied implicitly which is detrimental to the execution speed and memory usage of practical systems. Moreover, embedded systems programmers need fine-grained control over the circumstances at which data is copied to be able to predict memory use and execution times.

This paper introduces a new approach to using uniqueness types to enable building efficient and verifiable embedded systems using an aliasing-free programming language. The idea is to use uniqueness types for enforcing at-most-once consumption of unique values. The proposed model of uniqueness of values enables compiler optimizations such as elimination of physical copies and in-place mutation. In addition, the proposed approach provides a lightweight notation for the programmer to control copying behavior.

We have implemented our method in Sim, a new language for the development of safety-critical software. Our validation cases suggest that our aliasing-free language allows one to verify the functional correctness of realistic embedded programs with only a small annotation overhead while keeping the run-time performance of the program up to par with hand-optimized code.

ABSTRACT. Many applications of formal methods require automated reasoning about system properties, such as system safety and security. To improve the performance of automated reasoning engines, such as SAT/SMT solvers and first-order theorem prover, it is necessary to understand both the successful and failing attempts of these engines towards producing formal certificates, such as logical proofs and/or models. Such an analysis is challenging due to the large number of logical formulas generated during proof/model search. In this paper we focus on saturation-based first-order theorem proving and introduce the SATVIS tool for interactively visualizing saturation-based proof attempts in first-order theorem proving. We build SATVIS on top of the world-leading theorem prover Vampire, by interactively visualizing the saturation attempts of Vampire in SATVIS. Our work combines the automatic layout and visualization of the derivation graph induced by the saturation attempt with interactive transformations and search functionality. As a result, we are able to analyze and debug (failed) proof attempts of Vampire. Thanks to its interactive visualisation, we believe SATVIS helps both experts and non-experts in theorem proving to understand first-order proofs and analyze/refine failing proof attempts of first-order provers.

ABSTRACT. We present SIGmA (SAT sImplification on GPU Architectures), a preprocessor to accelerate SAT solving that runs on NVIDIA GPUs. We discuss the tool, focussing on its full functionality and how it can be used in combination with state-of-the-art SAT solvers. SIGmA performs various types of simplification, such as variable elimination, subsumption elimination, blocked clause elimination and hidden redundancy elimination.

ABSTRACT. We consider a combinatorial optimisation problem in terms of execution of parallel directed graphs annotated with sets of resources, and show how to select a path across the graphs constrained by a notion of resource compatibility. This notion takes into account interactions between any finite number of resources; this makes it possible, in particular, to express non-monotonic interactions. Our formalisation also introduces a discrete temporal metric, so as to consider only simultaneous nodes in the optimisation process. We then express the formal problem as an SMT problem and provide a correctness proof of the SMT code by exploiting the interplay between SMT solvers and the proof assistant Isabelle/HOL. This shows how the infrastructure already in place in proof assistants to exploit SMT solvers for theorem proving, can also be used in the reverse direction to exploit proof assistants to prove correctness of SMT code. The problem we consider combines aspects of optimal graph execution and of optimal resource allocation, showing how an SMT solver can be an alternative to other approaches which are well-researched in the corresponding domains.

ABSTRACT. A Software Product Line (SPL) is a set of programs, called variants, which are generated from a common artifact base. Delta-Oriented Programming (DOP) is a flexible approach to implement SPLs. A foundation for rigorous development of delta-oriented product lines of statecharts is provided by defining: a core language for statecharts, DOP on top of it, an analysis ensuring that a product line is well-formed (i.e., all variants can be generated and are well-formed statecharts). An implementation of the analysis has been applied to an industrial case study.

ABSTRACT. In (ter Beek et al., 2018), we introduce QFLan, a framework for quantitative modeling and analysis of highly (re)configurable systems, like software product lines. We define a rich domain specific language (DSL) for systems with variability in terms of features, which can be dynamically installed, removed or replaced, capable of modeling probabilistic behavior, possibly subject to quantitative feature constraints. High-level DSL specifications are automatically encoded in a process algebra whose operational behavior interacts with a store of constraints, which allows to separate a system's configuration from its behavior. The resulting probabilistic configurations and behavior converge seamlessly in a semantics based on discrete-time Markov chains, thus enabling quantitative analysis. An accompanying Eclipse-based tool offers a modern integrated development environment to specify such systems and to perform analyses that range from the likelihood of specific behavior to the expected average cost, in terms of feature attributes, of specific system variants. Based on a seamless integration with the statistical model checker MultiVeStA, QFLan allows to scale to larger models with respect to precise probabilistic analysis techniques. We provide a number of case studies that have driven and validated the development of the QFLan framework. In particular, we show the versatility of the QFLan framework with an application to risk analysis of a safe lock system from the security domain. Apart from a short tool paper at FM'18, none of the results from (ter Beek et al., 2018) have been reported at classical formal methods venues before.

ABSTRACT. Modal transition systems (MTSs) and featured transition systems (FTSs) are widely recognised as fundamental behavioural models for software product lines. MTSs with variability constraints (MTSvs) are equally expressive as FTSs. This is proved by providing sound and complete transformations of the latter into the former, and of the former into the latter. First, our results contribute to the expressiveness hierarchy of such basic models studied in many papers. Second, it provides an automatic algorithm from FTSs to MTSvs that preserves the original (compact) branching structure, thus paving the way for using the model checking of FTSs with the variability model checker VMC.