On the public citation graph

An Iris Instance for Verifying CompCert C Programs

https://doi.org/10.1145/3632848
0 signed · 48 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.
Claim with ORCID
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.
See reference health

What this work says

Outgoing claims: the papers this work cites, builds on, or argues with.

inferredcites →https://doi.org/10.1007/978-3-030-25540-4_22openalex-snapshot
Cerberus-BMC: A Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C
inferredcites →https://doi.org/10.1007/978-3-030-44914-8_13openalex-snapshot
Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems
inferredcites →https://doi.org/10.1007/978-3-030-44914-8_16openalex-snapshot
Connecting Higher-Order Separation Logic to a First-Order Outside World
inferredcites →https://doi.org/10.1007/978-3-030-90870-6_4openalex-snapshot
Two Mechanisations of WebAssembly 1.0
inferredcites →https://doi.org/10.1007/978-3-319-06410-9_9openalex-snapshot
The VerCors Tool for Verification of Concurrent Programs
inferredcites →https://doi.org/10.1007/978-3-540-76637-7_3openalex-snapshot
Local Reasoning for Storable Locks and Threads
inferredcites →https://doi.org/10.1007/978-3-642-10672-9_13openalex-snapshot
A Fresh Look at Separation Algebras and Share Accounting
inferredcites →https://doi.org/10.1007/978-3-642-20398-5_4openalex-snapshot
VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java
inferredcites →https://doi.org/10.1007/s10817-018-9457-5openalex-snapshot
VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs
inferredcites →https://doi.org/10.1017/cbo9781107256552openalex-snapshot
Program Logics for Certified Compilers
inferredcites →https://doi.org/10.1017/s0956796818000151openalex-snapshot
Iris from the ground up: A modular foundation for higher-order concurrent separation logic
inferredcites →https://doi.org/10.1145/1538788.1538814openalex-snapshot
Formal verification of a realistic compiler
inferredcites →https://doi.org/10.1145/2487241.2487248openalex-snapshot
CompCertTSO
inferredcites →https://doi.org/10.1145/2676726.2676980openalex-snapshot
Iris
inferredcites →https://doi.org/10.1145/3133911openalex-snapshot
A verified messaging system
inferredcites →https://doi.org/10.1145/3158154openalex-snapshot
RustBelt: securing the foundations of the Rust programming language
inferredcites →https://doi.org/10.1145/3236772openalex-snapshot
MoSeL: a general, extensible modal framework for interactive proofs in separation logic
inferredcites →https://doi.org/10.1145/3290378openalex-snapshot
Iron: managing obligations in higher-order concurrent separation logic
inferredcites →https://doi.org/10.1145/3293880.3294106openalex-snapshot
From C to interaction trees: specifying, verifying, and testing a networked server
inferredcites →https://doi.org/10.1145/3314221.3314595openalex-snapshot
Towards certified separate compilation for concurrent programs
inferredcites →https://doi.org/10.1145/3341301.3359632openalex-snapshot
Verifying concurrent, crash-safe systems with Perennial
inferredcites →https://doi.org/10.1145/3371102openalex-snapshot
RustBelt meets relaxed memory
inferredcites →https://doi.org/10.1145/3453483.3454031openalex-snapshot
Transfinite Iris: resolving an existential dilemma of step-indexed separation logic
inferredcites →https://doi.org/10.1145/3453483.3454036openalex-snapshot
RefinedC: automating the foundational verification of C code with refined ownership types
inferredcites →https://doi.org/10.1145/3519939.3523432openalex-snapshot
Diaframe: automated verification of fine-grained concurrent programs in Iris
inferredcites →https://doi.org/10.1145/3547631openalex-snapshot
Later credits: resourceful reasoning for the later modality
inferredcites →https://doi.org/10.1145/3571220openalex-snapshot
DimSum: A Decentralized Approach to Multi-language Semantics and Verification
inferredcites →https://doi.org/10.1145/3591265openalex-snapshot
Iris-Wasm: Robust and Modular Verification of WebAssembly Programs
inferredcites →https://doi.org/10.1145/3622823openalex-snapshot
Melocoton: A Program Logic for Verified Interoperability Between OCaml and C
inferredcites →https://doi.org/10.4230/lipics.itp.2021.32openalex-snapshot
Verifying an HTTP Key-Value Server with Interaction Trees and VST
inferredcites →https://doi.org/10.46298/lmcs-17(3:9)2021openalex-snapshot
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity
inferredcites →https://doi.org/10.48550/arxiv.2207.06574openalex-snapshot
Bringing Iris into the Verified Software Toolchain
inferredcites →https://doi.org/10.5281/zenodo.1003420openalex-snapshot
The Coq Proof Assistant
inferredcites →https://doi.org/10.5281/zenodo.8423865openalex-snapshot
VST on Iris

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-031-60698-4_6openalex-snapshot
Verifying a C Implementation of Derecho’s Coordination Mechanism Using VST and Coq
inferred← citeshttps://doi.org/10.1007/978-3-031-98668-0_4openalex-snapshot
Raven: An SMT-Based Concurrency Verifier
inferred← citeshttps://doi.org/10.1007/978-3-032-22723-2_5openalex-snapshot
A Formal Interface for Concurrent Search Structure Templates
inferred← citeshttps://doi.org/10.1007/978-981-95-2921-6_1openalex-snapshot
Exploration and Application of Formal Methods in I&C of Nuclear Power Plants
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/facct71761.2026.00011openalex-snapshot
Making Time Observable: Compiler Correctness for Real-Time C Programs
inferred← citeshttps://doi.org/10.1145/3704847openalex-snapshot
Program Logics à la Carte
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/3704903openalex-snapshot
Generically Automating Separation Logic by Functors, Homomorphisms, and Modules
inferred← citeshttps://doi.org/10.1145/3728967openalex-snapshot
Freesia: Verifying Correctness of TEE Communication with Concurrent Separation Logic
inferred← citeshttps://doi.org/10.1145/3729311openalex-snapshot
PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs
inferred← citeshttps://doi.org/10.1145/3747509openalex-snapshot
Formal Semantics and Program Logics for a Fragment of OCaml
inferred← citeshttps://doi.org/10.1145/3779031.3779095openalex-snapshot
Building Blocks for Step-Indexed Program Logics
inferred← citeshttps://doi.org/10.1145/3828682openalex-snapshot
Completeness of Iris-Based Program Logics
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.