Data Intensive Systems Formalization (DataCert)

The Datacert thematic is highly interested in the certification of data intensive systems with the Coq proof assistant. As data, in all forms, is increasingly large in volume, as a result of computers capturing more and more of the companies activity, the scientists' work and also as a result of better and more powerful automatic data gathering tools (e.g. space telescopes, focused crawlers, archived experimental data mandatory in some types of government-funded research programs). The availability and reliability of such large data volumes is a gold mine for companies, scientists and simply citizens. It is then of crucial importance to protect data integrity and reliability by means of robust methods and tools.

The aim of this research track is to certify data intensive systems such as relational database systems, XQuery and semi structured engines using formal tools such as SMT provers (e.g., Alt-ergo) embedded in the Why(3) platform as well as interactive theorem provers (e.g., Coq).

Formal semantics of UML/OCL

The Unified Modeling Language (UML) is one of the few modeling languages that is widely used in industry. While UML is mostly known as diagrammatic modeling language (e.g., visualizing class models), it is complemented by a textual language, called Object Constraint Language (OCL). OCL is based on a four-valued logic that turns UML into a formal language. Unfortunately the semantics of this specification language, captured in the "Annex A" of the OCL standard, leads to different interpretations of corner cases. We formalize the core of OCL: denotational definitions, a logical calculus and operational rules that allow for the execution of OCL expressions by a mixture of term rewriting and code compilation. Our formalization reveals several inconsistencies and contradictions in the current version of the OCL standard 2.5. Overall, we provided a theory in Isabelle/HOL and a generated document which is intended to provide the basis for a machine-checked text "Annex A" of the OCL standard targeting at tool implementors.

Formal semantics of process-oriented specification languages.

The Circus specification language combines elements for complex data and behavior specifications, using an integration of Z and CSP with a refinement calculus. Its semantics is based on Hoare and He’s unifying theories of programming (UTP). We develop a machine-checked, formal semantics based on a “shallow embedding” of Circus in Isabelle/UTP (our semantic theory of UTP based on Isabelle/HOL). We derive proof rules from this semantics and implement tactic support that finally allows for proofs of refinement for Circus processes (involving both data and behavioral aspects).

In parallel, we developed a formalization in Isabelle/HOL of the work of Hoare and Roscoe on the denotational semantics of the Failure/Divergence Model of CSP. It follows essentially the presentation of CSP in Roscoe's Book "Theory and Practice of Concurrency" @{cite "roscoe:csp:1998" } and the semantic details in a joint Paper of Roscoe and Brooks "An improved failures model for communicating processes" originated by Brookes and Roscoe in 1985. This model is still the "Gold-Standard" of CSP semantics.

Formalization of heterogenous timed choreography languages.

We study the semantics of specification languages for the coordination of concurrent systems, which provides time, duration and causality constraints. The language TESL (developed by Boulanger et al in the LRI-ModHel group) is defined for the coordination of concurrent systems, and provides concepts for time, duration and causality constraints. The language is defined in terms of a denotational semantics. In order to be applicable in verification techniques, we also define a symbolic operational semantics that constructs the possible timelines. We present a novel way to link these two semantics by taking advantage of an unfolding principle of these timelines. Moreover, we apply our study to a tool for runtime-testing heterogeneous systems. We also define a dilation relation between timelines, which characterizes the addition of stuttering instants, and we prove that specifications in the language are invariant by stuttering. We give a formalization of these semantic models in the Isabelle/HOL proof assistant, together with formal proofs for soundness, completeness and progress, as well as local termination and invariance by stuttering.

Formal semantics of JavaScript

The JsCert project has provided a formalization of an almost-complete subset of the semantics of JavaScript, following the ECMAScript Language Specification, version 5. This semantics is expressed in Coq, using a pretty-big step semantics. In addition to the inductive evaluation rules, a reference interpreter has been proved correct. This interpreter may be used to run actual JavaScript program following the rules of the formal semantics. It has been used in particular to validate the formal semantics against official JavaScript test suites. This formalization of JavaScript can serve as a basis for developing formalization of secure subsets of JavaScript, for developing verified static analyses for JavaScript code, and for mechanically-verified translations from high-level languages into JavaScript. These applications are the fpcus of the ANR AJACS project.

Floating-point arithmetic

A high-level of guarantee on floating-point computations is obtained by formal proofs in Coq. We maintain and develop large Coq libraries (such as Flocq and PFF) for floating-point arithmetic: core definitions, axiomatic and computational rounding operations, high-level properties. They provide a framework for developers to formally certify numerical applications. More details can be found on the verified computer arithmetic page.

Real analysis

We have worked on easing proofs of differentiability and integrability in Coq. The use case was the existence of a solution to the wave equation thanks to D'Alembert's formula; the goal was to automate the process as much as possible. Our approach is based on the pervasive use of total functions. We aim at creating a modern formalization of the real numbers in Coq, with a focus on practicality. This is sorely needed to ease the verification of numerical applications, especially those involving advanced mathematics.

Weak memory model of Multicore OCaml

Multicore OCaml is an experimental variant of the OCaml programming language which features shared-memory multicore parallelism. It is planned to be merged in the main OCaml sources. At Vals, we explore the weak memory model which Multicore OCaml uses by formally verifying concurrent programs in this memory model and by experimenting the design of lock-free concurrent algorithms in Multicore OCaml.