Formal verification of a realistic compiler

By Xavier Leroy. 2009

1,492 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

Citations in the corpus

Improving Robot Controller Transparency Through Autonomous Policy Explanation (2017, methodology): “Traditional methods for acquiring an understanding of control logic typically involve some form of source code inspection and documentation review [2, 13] or formal verification given proper specifications [36, 23].”
DeepMath - Deep Sequence Models for Premise Selection (2016, methodology): “ITP verification of the seL4 kernel [25] and CompCert compiler [27] show comparable progress in large scale software verification.”
Modelling High-Level Mathematical Reasoning in Mechanised Declarative Proofs (2020, background): “Over the last decade, nontrivial mathematical theorems [16, 18, 19], security protocols [14, 40], and industry-scale software systems [27, 32] have been mechanically checked, highlighting numerous issues and bugs.”
Using Crash Hoare logic for certifying the FSCQ file system (2015, methodology): “The CompCert compiler [45] is formally specified and verified in Coq.”
Finding and understanding bugs in C compilers (2011, background): “Wolfe [30], talk ing about independent software vendors (ISVs) says: An ISV with a complex code can work around correctness, turn off the optimizer in one or two .les, and usually they have to do that for any of the compilers they use (emphasis ours).”
Baldur: Whole-Proof Generation and Repair with Large Language Models (2023, methodology): “For example, the proof of the C compiler is more than three times as long as the compiler code itself [51].”
Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling (2019, background): “It has been a longstanding, active area of artificial intelligence research that has demonstrated utility in the design of operating systems [1, 2], distributed systems [3, 4], compilers [5, 6], microprocessor design [7], and in general mathematics [8].”
History of Interactive Theorem Proving (2014, methodology): “…carried out with interactive theorem proving in recent years are the correctness proofs of a ‘CompCert’ optimizing compiler from a significant subset of C using Coq [Leroy, 2009], and of a designed-forverification version of the commercial L4 microkernel using Isabelle/HOL [Klein et al., 2010].”
Learning Shape Analysis (2017, background): “CompCert [27], miTLS [6], seL4 [24], and IronFleet [19]).”
Verdi: a framework for implementing and formally verifying distributed systems (2015, methodology): “The CompCert C compiler [22] was verified in Coq and repeatedly shown to be more reliable than traditionally developed compilers [21, 41].”
Cosette: An Automated Prover for SQL (2017, methodology): “As such, they have been used recently to prove the correctness of many software systems [22, 19].”
Preliminary design of the SAFE platform (2011, methodology): “) We hope to formally verify the Tempest compiler, following the CompCert [11] verified C compiler; this will ease the burden of verifying the concreteware by allowing”
CakeML: a verified implementation of ML (2014, methodology): “The CompCert compiler [14] and projects based on it, including CompcertTSO [29] and the Princeton “verified software toolchain” [1], focus on a C-like source language in contrast to our ML-like language.”
Learning to Prove Theorems via Interacting with Proof Assistants (2019, methodology): “It has been used to develop certified software and hardware (Leroy, 2009; Paulin-Mohring, 1995), and to prove theorems in mathematics, including the Feit–Thompson theorem (Gonthier et al., 2013).”
Premise Selection for Theorem Proving by Deep Graph Embedding (2017, background): “It not only constitutes a key aspect of general intelligence, but also underpins a broad set of applications ranging from circuit design to compilers, where it is critical to verify the correctness of a computer system [2, 3, 4].”