Formal Proofs

Theme Presentation

Scientific Context

Contemporary software and system design methods use very complex tools relying on complex and often unstated mathematical properties. For instance, a key element in the software production workflow is the compiler which translates human-readable source code into efficient machine-executable code, using advanced optimisation techniques. While the theory behind compilers has been well understood for quite some time, providing a fully formalized, machine-checked proof of correctness for a compiler for a mainstream programming language has been an elusive task until the landmark achievement of X. Leroy et al : in 2009, they released the CompCert formalized C compiler, written and proven correct using the formal language of the Coq interactive proof assistant. This work shows how far one can go with the versatile framework for interactive formal proof development that is Coq, and how its built-in program extraction mechanism can be useful for industrial applications.

Scientific Goal

The goal of the Formal Proofs theme is to coordinate all research efforts made at Verimag Lab about using formal proofs to model systems and software and certify their properties with a very high confidence level. This allows to consider using these tools, libraries and methods for the design and development of critical systems.

The main formal proof software that we use is the Coq proof assistant, both for scientific and historical reasons. Scientific reasons because Coq is a very general tool that allows to use various formalization techniques that can be fitted to our proving needs. Historical reasons because many proof development efforts involve extending the CompCert C compiler, and because Coq is the proof assistant in which Verimag members are the most proficient.

Scientific Activities

Among the group activities, we can distinguish several research directions:

• Extensions and applications of certified compilers : new source languages, new target architectures, combining certified compilation with static analysis.
• Advancing confidence in distributed software and systems: fault-tolerant distributed algorithms, robot swarms
• Enhancing proof techniques and tactics for the Coq Proof Assistant : making the formal proof process more accessible and less tedious through small-scale proof automation.

Theme activities

Certified compilation and static analysis

• Certified polyhedra for static analysis. The VPL (Verimag/Verified Polyhedron Library) provides an abstract domain of convex polyhedra, formally verified in Coq for formally verified static analyzers, such as Verasco.

• Certified C compiler backends for the CompCert certified compiler
  • Instruction scheduling for pipelined processors and in particular for Kalray VLIW core (with explicit instruction parallelism at the assembly level). See the KVX CompCert Compiler.
  • Cryptographically Hardened RiscV architecture (IntrinSec/NanoTrust)
  • Embedded ARM/RiscV Architectures with custom instruction set extensions

• Certified compilers for synchronous languages
  • A verified compiler for the Lustre Synchronous Language, translating Lustre code into CompCert’s Clight code, which is then compiled using CompCert
  • A verified compiler for Pure Kernel Esterel (a subset of Esterel featuring only control flow constructs, no datatypes) to digital circuits

Certified distributed software and systems

• Certification of Realtime Systems and scheduling policies
• Formalization of distributed self-stabilizing systems. Development of the PADEC framework. The goal of the PADEC framework is to build certified proofs of self-stabilizing algorithms using the Coq proof assistant. The framework includes the definition of the computational model, lemmas for common proof patterns and case studies (correctness of self-stabilizing algorithm, time complexity).
• Formalization of mobile robot fleets behavior and algorithms, with formally precise models allowing correctness proofs of protocols, impossibility proofs, and comparison between models, all backed by the Coq proof assistant, within the Pactole library.

Enhancing proof techniques and tactics for the Coq Proof Assistant

• Automation for proofs using equivalence relations and setoids. Design and study of a decision procedure adapted to a context with multiple (partial) equivalence relations, using appropriate extensions of congruence-closure and E-matching.
• Design patterns for formally verified and efficient software, with embeddings of untrusted imperative computations through Coq extraction (toward OCaml). See the Impure Library.
• Proof techniques based on reflection and external certificates. For example, see the VPL tactic (for simplifying linear arithmetic within Coq goals, with oracles from the VPL library).