On the public citation graph
CompCertM: CompCert with C-assembly linking and lightweight modular verification
0 signed · 72 inferred · view as graph
Inferred edges come from two machine sources: sweeps of open repository metadata (mostly SSRN and Zenodo), and a bulk OpenAlex citation snapshot. Every row below is labelled with the one it came from. Neither is a complete citation index — absence here is not evidence of absence.
Is this your work? Sign in with ORCID and put your name on the
claims that are yours.
Reference health. See whether every reference in this work resolves to a
known work and none has been retracted — and get a dated CiteStamped
badge you can embed.
What this work says
Outgoing claims: the papers this work cites, builds on, or argues with.
inferredcites →https://doi.org/10.1007/978-3-319-89366-2_8openalex-snapshot
Fab ous Interoperability for ML and a Linear Language
inferredcites →https://doi.org/10.1007/978-3-642-19718-5_1openalex-snapshot
Verified Software Toolchain
inferredcites →https://doi.org/10.1007/978-3-642-54833-8_7openalex-snapshot
Verified Compilation for Shared-Memory C
inferredcites →https://doi.org/10.1007/978-3-642-54833-8_8openalex-snapshot
Verifying an Open Compiler Using Multi-language Semantics
inferredcites →https://doi.org/10.1017/cbo9781107256552openalex-snapshot
Program Logics for Certified Compilers
inferredcites →https://doi.org/10.1145/1111037.1111042openalex-snapshot
Formal certification of a compiler back-end or
inferredcites →https://doi.org/10.1145/1538788.1538814openalex-snapshot
Formal verification of a realistic compiler
inferredcites →https://doi.org/10.1145/1863543.1863566openalex-snapshot
The impact of higher-order state and control effects on local relational reasoning
inferredcites →https://doi.org/10.1145/2103621.2103666openalex-snapshot
The marriage of bisimulations and Kripke logical relations
inferredcites →https://doi.org/10.1145/2103656.2103666openalex-snapshot
The marriage of bisimulations and Kripke logical relations
inferredcites →https://doi.org/10.1145/2676726.2676975openalex-snapshot
Deep Specifications and Certified Abstraction Layers
inferredcites →https://doi.org/10.1145/2737924.2738005openalex-snapshot
A formal C memory model supporting integer-pointer casts
inferredcites →https://doi.org/10.1145/2784731.2784764openalex-snapshot
Pilsner: a compositionally verified compiler for a higher-order imperative language
inferredcites →https://doi.org/10.1145/2837614.2837642openalex-snapshot
Lightweight verification of separate compilation
inferredcites →https://doi.org/10.1145/2951913.2951941openalex-snapshot
Fully abstract compilation via universal embedding
inferredcites →https://doi.org/10.1145/3009837.3009850openalex-snapshot
A promising semantics for relaxed-memory concurrency
inferredcites →https://doi.org/10.1145/3062341.3062347openalex-snapshot
FunTAL: reasonably mixing a functional language with assembly
inferredcites →https://doi.org/10.1145/3290375openalex-snapshot
An abstract stack based approach to verified compositional compilation to machine code
inferredcites →https://doi.org/10.1145/3314221.3314595openalex-snapshot
Towards certified separate compilation for concurrent programs
inferredcites →https://doi.org/10.1145/3341689openalex-snapshot
The next 700 compiler correctness theorems (functional pearl)
inferredcites →https://doi.org/10.5555/3026877.3026928openalex-snapshot
CertiKOS: an extensible architecture for building certified concurrent OS kernels
What points at this work
Incoming claims: where this work appears in other papers’ reference lists and arguments.
inferred← citeshttps://doi.org/10.1007/978-3-030-99336-8_8openalex-snapshot
The Trusted Computing Base of the CompCert Verified Compiler
inferred← citeshttps://doi.org/10.1007/978-3-031-76554-4_8openalex-snapshot
Modeling Register Pairs in CompCert
inferred← citeshttps://doi.org/10.1016/j.sysarc.2023.103046openalex-snapshot
ThreadAbs: A template to build verified thread-local interfaces with software scheduler abstractions
inferred← citeshttps://doi.org/10.1016/j.sysarc.2023.103049openalex-snapshot
SimplMM: A simplified and abstract multicore hardware model for large scale system software formal verification
inferred← citeshttps://doi.org/10.1109/access.2025.3539584openalex-snapshot
A Formal Verification Library Design for Behavioral Refinement of CompCert Clight
inferred← citeshttps://doi.org/10.1109/csf54842.2022.9919680openalex-snapshot
SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation
inferred← citeshttps://doi.org/10.1109/csf57540.2023.00021openalex-snapshot
Towards End-to-End Verified TEEs via Verified Interface Conformance and Certified Compilers
inferred← citeshttps://doi.org/10.1109/csf64896.2025.00030openalex-snapshot
Symbolic Parallel Composition for Multi-language Protocol Verification
inferred← citeshttps://doi.org/10.1109/icse55347.2025.00081openalex-snapshot
Hetrify: Efficient Verification of Heterogeneous Programs on RISC-V
inferred← citeshttps://doi.org/10.1109/tse.2026.3692469openalex-snapshot
Hetrify+: Improving the Verification Efficiency of RISC-V Heterogeneous Programs via Memory Access Specialization
inferred← citeshttps://doi.org/10.1145/3428265openalex-snapshot
CompCertELF: verified separate compilation of C programs into ELF object files
inferred← citeshttps://doi.org/10.1145/3434327openalex-snapshot
Formally verified speculation and deoptimization in a JIT compiler
inferred← citeshttps://doi.org/10.1145/3437992.3439915openalex-snapshot
A minimalistic verified bootstrapped compiler (proof pearl)
inferred← citeshttps://doi.org/10.1145/3453483.3454097openalex-snapshot
CompCertO: compiling certified open C components
inferred← citeshttps://doi.org/10.1145/3473572openalex-snapshot
Modular, compositional, and executable formal semantics for LLVM IR
inferred← citeshttps://doi.org/10.1145/3473591openalex-snapshot
Compositional optimizations for CertiCoq
inferred← citeshttps://doi.org/10.1145/3498686openalex-snapshot
Verified compilation of C programs with a nominal memory model
inferred← citeshttps://doi.org/10.1145/3519939.3523734openalex-snapshot
Verifying optimizations of concurrent programs in the promising semantics
inferred← citeshttps://doi.org/10.1145/3571202openalex-snapshot
Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler
inferred← citeshttps://doi.org/10.1145/3571220openalex-snapshot
DimSum: A Decentralized Approach to Multi-language Semantics and Verification
inferred← citeshttps://doi.org/10.1145/3591266openalex-snapshot
Cakes That Bake Cakes: Dynamic Computation in CakeML
inferred← citeshttps://doi.org/10.1145/3622823openalex-snapshot
Melocoton: A Program Logic for Verified Interoperability Between OCaml and C
inferred← citeshttps://doi.org/10.1145/3632914openalex-snapshot
Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules
inferred← citeshttps://doi.org/10.1145/3658644.3670288openalex-snapshot
SECOMP: Formally Secure Compilation of Compartmentalized C Programs
inferred← citeshttps://doi.org/10.1145/3704881openalex-snapshot
Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting
inferred← citeshttps://doi.org/10.1145/3704897openalex-snapshot
VeriRT: An End-to-End Verification Framework for Real-Time Distributed Systems
inferred← citeshttps://doi.org/10.1145/3704900openalex-snapshot
Unifying Compositional Verification and Certified Compilation with a Three-Dimensional Refinement Algebra
inferred← citeshttps://doi.org/10.1145/3705593openalex-snapshot
Formal Verification of Just-in-Time Compilation
inferred← citeshttps://doi.org/10.1145/3705593.3705596openalex-snapshot
Background on Just-in-Time Compilation
inferred← citeshttps://doi.org/10.1145/3705593.3705597openalex-snapshot
Background on the CompCert Compiler
inferred← citeshttps://doi.org/10.1145/3705593.3705598openalex-snapshot
Designing Formally Verified JITs
inferred← citeshttps://doi.org/10.1145/3705593.3705599openalex-snapshot
Formally Verified Speculative Optimizations
inferred← citeshttps://doi.org/10.1145/3705593.3705600openalex-snapshot
Formal Verification of Impure Coq JITs
inferred← citeshttps://doi.org/10.1145/3705593.3705601openalex-snapshot
Formal Verification of a JIT Backend Compiler
inferred← citeshttps://doi.org/10.1145/3705593.3705604openalex-snapshot
Relating the Developments to the Book
inferred← citeshttps://doi.org/10.1145/3729276openalex-snapshot
CompCertOC: Verified Compositional Compilation of Multi-threaded Programs with Shared Stacks
inferred← citeshttps://doi.org/10.1145/3776682openalex-snapshot
Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic Back-Translation
inferred← citeshttps://doi.org/10.1145/3797874openalex-snapshot
Denotation-based Compositional Compiler Verification
inferred← citeshttps://doi.org/10.1145/3808263openalex-snapshot
Let It Flow: A Formally Verified Compilation Framework for Asynchronous Dataflow
inferred← citeshttps://doi.org/10.70675/bfb1bf73z45cez4651z9900z881984e8c420openalex-snapshot
Formal Verification of Just-in-Time Compilation
Editorial review for independent work. ICSAC — the Institute for Complexity
Science and Advanced Computing — runs a structured editorial panel for researchers
publishing outside journals, and publishes on CiteStamp rails. Submission is free
and goes through ORCID: icsacinstitute.org/submit.