TBA
19 November 2026 - 13h30
Barocq: A High-Level Programming Language for Efficient and Verifiable Embedded System Code.
by Clement Chavanon from IRISA - EPICURE Team
invited by David MONNIAUX
19 November 2026 - 13h30
Barocq: A High-Level Programming Language for Efficient and Verifiable Embedded System Code.
by Clement Chavanon from IRISA - EPICURE Team
invited by David MONNIAUX
Abstract: Critical embedded systems deserve the highest level of assurance to guarantee that their implementation satisfies their specification. Formally verifying system software is challenging because they are written in low-level languages, which require reasoning with pointers and fine-grained memory models. To reduce the verification effort, a standard approach is to reason on a higher level abstraction that models how the source code behaves. To ensure that the abstract model safely captures the semantics of the source code, one can define increasingly precise models, and connect them with refinement proofs, ensuring that they are valid implementations of the more abstract one. Nevertheless, these refinement steps are time consuming, and require manually maintaining the various models and refinement proofs in parallel, based on changes to the source code.
To tackle this problem, we propose to leverage verified compilation to automatically derive high-level functional models into equivalent low-level C programs. Because our target are embedded systems, we create a novel Domain Specific Language named Barocq, designed as a minimal and purely functional language, and compiled to human-readable and efficient C code. Efficiency is achieved by enforcing a strict alias-control programming discipline thanks to static analysis, allowing functional updates to be translated to in-place mutations. Thus, the compiled programs do not require a garbage collected runtime to execute. Additionally, Barocq programs can be embedded in the Rocq proof assistant for practical formal reasoning at the source level. We demonstrate that Barocq has adequate features to write an interesting class of critical embedded system code, by porting the S3K separation kernel to Barocq. We show that this new implementation can be used as drop-in replacement for the original C code, as it only introduces a fairly small performance overhead.
