Formal certification of a compiler back-end or: programming a compiler with a proof assistant

No abstract is available for this paper.

• Publication year

  2006

• Venue

  ACM-SIGACT Symposium on Principles of Programming Languages

• Publication date

  2006-01-11

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1145/1111037.1111042
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• A machine-checked model for a Java-like language, virtual machine, and compiler

  2006cited by this paper
• Towards the Formal Verification of a C0 Compiler: Code Generation and Implementation Correctnes

  2005cited by this paper
• Formal Verification of a Memory Model for C-Like Imperative Languages

  2005cited by this paper
• Interprétation abstraite en logique intuitionniste : extraction d'analyseurs Java certifiés

  2005cited by this paper
• Optimizing Code Generation from SSA Form: A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL

  2005cited by this paper
• Automated soundness proofs for dataflow analyses and transformations via local rules

  2005cited by this paper
• Coq à la conquête des moulins

  2005cited by this paper
• Symbolic transfer function-based approaches to certified compilation

  2004cited by this paper
• A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis

  2004cited by this paper
• A Uniform and Certified Approach for Two Static Analyses

  2004cited by this paper
• Interactive Theorem Proving and Program Development

  2004cited by this paper
• Register allocation and spilling via graph coloring

  2004cited by this paper
• Compiler verification: a bibliography

  2003cited by this paper
• Compilation de termes de preuves : un (nouveau) mariage entre coq et OCaml

  2003cited by this paper
• A New Extraction for Coq

  2002cited by this paper
• Tool-Assisted Specification and Verification of the JavaCard Platform

  2002cited by this paper
• VOC: A Translation Validator for Optimizing Compilers

  2002cited by this paper
• Formal Verification of a Java Compiler in Isabelle

  2002cited by this paper
• Java and the Java Virtual Machine

  2001cited by this paper
• Oracle-based checking of untrusted software

  2001cited by this paper
• A Mechanically Verified Compiling Specification for a Lisp Compiler

  2001cited by this paper
• Translation validation for an optimizing compiler

  2000cited by this paper
• Correct System Design, Recent Insight and Advances, (to Hans Langmaack on the occasion of his retirement from his professorship at the University of Kiel)

  1999cited by this paper
• Credible Compilation with Pointers

  1999cited by this paper
• From system F to typed assembly language

  1999cited by this paper
• Verification of Compilers

  1999cited by this paper
• C--: A Portable Assembly Language that Supports Garbage Collection

  1999cited by this paper
• The calculational design of a generic abstract interpreter

  1999cited by this paper
• Translation Validation

  1998cited by this paper
• Basic-Block Graphs: Living Dinosaurs?

  1998cited by this paper
• Piton: A Mechanically Verified Assembly-Level Language

  1996cited by this paper
• Iterated register coalescing

  1996cited by this paper
• Towards a Formal Forth

  1993cited by this paper
• A mechanically verified language implementation

  1989cited by this paper

• A Formally Verified Procedure for Width Inference in FIRRTL

  2026cites this paper
• Miri: Practical Undefined Behavior Detection for Rust

  2026cites this paper
• Foundational Multi-Modal Program Verifiers

  2026cites this paper
• Automatically Engineering Trusted Software: A Research Roadmap

  2026cites this paper
• Synthesizing Instruction Selection Back-Ends from ISA Specifications Made Practical

  2026cites this paper
• Non-interference Preserving Optimising Compilation

  2025cites this paper
• Parameterized Hardware Verification Through A Term-level Generalized Symbolic Trajectory Evaluation And Its Linkage With Concrete Hardware Verification At Netlist Level

  2025cites this paper
• Compiler Optimization Testing Based on Optimization-Guided Equivalence Transformations

  2025cites this paper
• A Verified Foreign Function Interface between Coq and C

  2025cites this paper
• Verifying Asynchronous Hyperproperties in Reactive Systems

  2025cites this paper
• CCR 2.0: High-level Reasoning for Conditional Refinements

  2025cites this paper
• On the Impact of Formal Verification on Software Development

  2025cites this paper
• Formal Verification of Just-in-Time Compilation

  2025cites this paper
• IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL (Extended Version)

  2025cites this paper
• Formal Semantics and Program Logics for a Fragment of OCaml

  2025cites this paper
• Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting

  2025cites this paper
• Preservation of Speculative Constant-Time by Compilation

  2025cites this paper
• Symbolic Parallel Composition for Multi-language Protocol Verification

  2025cites this paper
• Preserving provability over GPU program optimizations with annotation-aware transformations

  2025cites this paper
• HITrees: Higher-Order Interaction Trees

  2025cites this paper
• Are Users More Willing to Use Formally Verified Password Managers?

  2025cites this paper
• Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment

  2025cites this paper
• Emerging Compiler Testing Based on Test Case Reuse

  2025cites this paper
• Towards Formal Verification of LLM-Generated Code from Natural Language Prompts

  2025cites this paper
• Icarus: Trustworthy Just-In-Time Compilers with Symbolic Meta-Execution

  2024cites this paper
• StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator

  2024cites this paper
• Modeling Dynamic (De)Allocations of Local Memory for Translation Validation

  2024cites this paper
• AC4: Algebraic Computation Checker for Circuit Constraints in Zero-Knowledge Proofs

  2024cites this paper
• QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning

  2024cites this paper
• Some Remarks About Dependent Type Theory

  2024cites this paper
• Correct-by-Construction Design of Custom Accelerator Microarchitectures

  2024cites this paper
• Verified Extraction from Coq to OCaml

  2024cites this paper
• Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification

  2024cites this paper
• Active Objects Based on Algebraic Effects

  2024cites this paper
• Refinement Composition Logic

  2024cites this paper
• Formal Verification of Code Conversion: A Comprehensive Survey

  2024cites this paper
• Correct and Complete Type Checking and Certified Erasure for Coq, in Coq

  2024influential citation
• Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification

  2024cites this paper
• Correctly Compiling Proofs About Programs Without Proving Compilers Correct

  2024cites this paper
• Charon: An Analysis Framework for Rust

  2024cites this paper
• Refinement Proofs in Rust Using Ghost Locks

  2023cites this paper
• SimplMM: A simplified and abstract multicore hardware model for large scale system software formal verification

  2023cites this paper
• Correct Compilation of Proofs About Embedded 1 Programs 2

  2023cites this paper
• TorchProbe: Fuzzing Dynamic Deep Learning Compilers

  2023cites this paper
• Expressive Authorization Policies using Computation Principals

  2023cites this paper
• Mostly Automated Proof Repair for Verified Libraries

  2023cites this paper
• 2022 ACTIVITY REPORT Project-Team GALLINETTE

  2023cites this paper
• On Normative Arrows and Comparing Tax Automation Systems

  2023cites this paper
• FuzzyFlow: Leveraging Dataflow To Find and Squash Program Optimization Bugs

  2023cites this paper
• Calculating Compilers for Concurrency

  2023cites this paper
• Fair Operational Semantics

  2023cites this paper
• RENOVATING ENGINEERING DEPARTEMENTS’ CREATION HERITAGE TO MEET CONTEMPORARY CHALLENGES: FRUGAL VALIDATION PATTERNS AND CONSTRUCTIVE PROOF LOGICS FOR NEW ENGINEERING RULES

  2023cites this paper
• Towards End-to-End Verified TEEs via Verified Interface Conformance and Certified Compilers

  2023cites this paper
• Stuttering for Free

  2023influential citation
• DimSum: A Decentralized Approach to Multi-language Semantics and Verification

  2023cites this paper
• Semantic Transformation Framework for Rewriting Rules

  2023cites this paper
• Conditional Contextual Refinement

  2023cites this paper
• CN: Verifying Systems C Code with Separation-Logic Refinement Types

  2023cites this paper
• A Correctness and Incorrectness Program Logic

  2023cites this paper
• Reverse Template Processing Using Abstract Interpretation

  2023cites this paper
• State of the Art for Addressing Hazards from Common Causes in Engineering Digital Instrumentation & Control (I&C) Systems

  2023cites this paper
• Accepted proofs: Objective truth, or culturally robust

  2023cites this paper
• Conditional Contextual Refinement (CCR)

  2022influential citation
• Alpinist: An Annotation-Aware GPU Program Optimizer

  2022cites this paper
• Finding typing compiler bugs

  2022cites this paper
• VIP: verifying real-world C idioms with integer-pointer casts

  2022cites this paper
• Towards effective preservation of robust safety properties

  2022cites this paper
• Simuliris: a separation logic framework for verifying concurrent program optimizations

  2022cites this paper
• Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code

  2022cites this paper
• Specialized Accelerators and Compiler Flows: Replacing Accelerator APIs with a Formal Software/Hardware Interface

  2022cites this paper
• Shellac: A Compiler Synthesizer for Concurrent Programs

  2022cites this paper
• ORIGAMI: Folding Data Structures to Reduce Timing Side-Channel Leakage

  2022cites this paper
• Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler

  2022cites this paper
• A novel data-driven approach on inferring loop invariants for C programs

  2022cites this paper
• Verified Compilation and Optimization of Floating-Point Programs in CakeML (Artifact)

  2022cites this paper
• Abstract interpretation repair

  2022cites this paper
• Monadic compiler calculation (functional pearl)

  2022cites this paper
• Random testing of a higher-order blockchain language (experience report)

  2022cites this paper
• Some remarks about Dependent Type Theory

  2021cites this paper
• A formal treatment of the role of verified compilers in secure computation

  2021cites this paper
• Flexible Refinement Proofs in Separation Logic

  2021cites this paper
• Dynaplex: analyzing program complexity using dynamically inferred recurrence relations

  2021cites this paper
• Practical and Efficient in-Enclave Verification of Privacy Compliance

  2021cites this paper
• Certifying the synthesis of heap-manipulating programs

  2021cites this paper
• Extracting functional programs from Coq, in Coq

  2021cites this paper
• Abstraction Logic: The Marriage of Contextual Refinement and Separation Logic

  2021cites this paper
• Robustly Safe Compilation, an Efficient Form of Secure Compilation

  2021cites this paper
• Доверя'й, но проверя'й: SFI safety for native-compiled Wasm

  2021cites this paper
• Catala: a programming language for the law

  2021cites this paper
• Formally Validating a Practical Verification Condition Generator (extended version)

  2021cites this paper
• Formally verified speculation and deoptimization in a JIT compiler

  2021cites this paper
• Functional Correctness of C Implementations of Dijkstra's, Kruskal's, and Prim's Algorithms

  2021cites this paper
• A Self-certifying Compilation Framework for WebAssembly

  2021influential citation
• Efficient Verification of Optimized Code: Correct High-speed X25519

  2021cites this paper
• Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities - (Invited Paper)

  2021cites this paper
• Project-Team Moscova Mobility, Security, Concurrency, Verification and Analysis

  2021cites this paper
• The Braga Method: Extracting Certified Algorithms from Complex Recursive Schemes in Coq

  2021cites this paper
• Practical End-to-End Verification of Cyber-Physical Systems

  2021cites this paper
• Touring the MetaCoq Project (Invited Paper)

  2021cites this paper
• Provable multicore schedulers with Ipanema: application to work conservation

  2020cites this paper