On the public citation graph

CN: Verifying Systems C Code with Separation-Logic Refinement Types

https://doi.org/10.1145/3571194
0 signed · 68 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/11609773_28openalex-snapshot
What’s Decidable About Arrays?
inferredcites →https://doi.org/10.1007/3-540-45937-5_16openalex-snapshot
CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs
inferredcites →https://doi.org/10.1007/978-3-030-17184-1_3openalex-snapshot
Semi-automated Reasoning About Non-determinism in C Expressions
inferredcites →https://doi.org/10.1007/978-3-319-12466-7_1openalex-snapshot
Certified Complexity (CerCo)
inferredcites →https://doi.org/10.1007/978-3-319-41528-4_22openalex-snapshot
Automatic Verification of Iterated Separating Conjunctions Using Symbolic Execution
inferredcites →https://doi.org/10.1007/978-3-642-05089-3_51openalex-snapshot
Verifying the Microsoft Hyper-V Hypervisor with VCC
inferredcites →https://doi.org/10.1007/s10817-009-9155-4openalex-snapshot
A Formally Verified Compiler Back-end
inferredcites →https://doi.org/10.1007/s10817-016-9369-1openalex-snapshot
A Formal C Memory Model for Separation Logic
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.1016/0304-3975(87)90045-4openalex-snapshot
Linear logic
inferredcites →https://doi.org/10.1017/cbo9781107256552openalex-snapshot
Program Logics for Certified Compilers
inferredcites →https://doi.org/10.1017/s0956796806006216openalex-snapshot
Dependent ML An approach to practical programming with dependent types
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.1017/s095679682100023xopenalex-snapshot
Cogent: uniqueness types and certifying compilation
inferredcites →https://doi.org/10.1109/eucnc.2016.7561034openalex-snapshot
A high assurance virtualization platform for ARMv8
inferredcites →https://doi.org/10.1109/eucnc40664.2017openalex-snapshot
2017 European Conference on Networks and Communications (EuCNC)
inferredcites →https://doi.org/10.1109/lics.2002.1029817openalex-snapshot
Separation logic: a logic for shared mutable data structures
inferredcites →https://doi.org/10.1109/msec.2022.3158196openalex-snapshot
Developing With Formal Methods at BedRock Systems, Inc.
inferredcites →https://doi.org/10.1109/sp40001.2021.00049openalex-snapshot
A Secure and Formally Verified Linux KVM Hypervisor
inferredcites →https://doi.org/10.1145/1111320.1111042openalex-snapshot
Formal certification of a compiler back-end or
inferredcites →https://doi.org/10.1145/1379022.1375602openalex-snapshot
Liquid types
inferredcites →https://doi.org/10.1145/1743546.1743574openalex-snapshot
seL4
inferredcites →https://doi.org/10.1145/174675openalex-snapshot
Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '94
inferredcites →https://doi.org/10.1145/2535838.2535841openalex-snapshot
CakeML
inferredcites →https://doi.org/10.1145/2560537openalex-snapshot
Comprehensive formal verification of an OS microkernel
inferredcites →https://doi.org/10.1145/2663171.2663188openalex-snapshot
The rust language
inferredcites →https://doi.org/10.1145/2676726.2676970openalex-snapshot
Functors are Type Refinement Systems
inferredcites →https://doi.org/10.1145/2908080.2908081openalex-snapshot
Into the depths of C: elaborating the de facto standards
inferredcites →https://doi.org/10.1145/2914770.2837621openalex-snapshot
Model checking for symbolic-heap separation logic with inductive predicates
inferredcites →https://doi.org/10.1145/2951913.2951924openalex-snapshot
A new verified compiler backend for CakeML
inferredcites →https://doi.org/10.1145/3018610.3018621openalex-snapshot
Verified compilation of CakeML to multiple machine-code targets
inferredcites →https://doi.org/10.1145/3290380openalex-snapshot
Exploring C semantics and pointer provenance
inferredcites →https://doi.org/10.1145/3378426openalex-snapshot
seL4 in Australia
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/3470569openalex-snapshot
The dogged pursuit of bug-free C programs
inferredcites →https://doi.org/10.1145/3477132.3483560openalex-snapshot
Formal Verification of a Multiprocessor Hypervisor on Arm Relaxed Memory Hardware
inferredcites →https://doi.org/10.1145/3498681openalex-snapshot
VIP: verifying real-world C idioms with integer-pointer casts
inferredcites →https://doi.org/10.1145/3519939.3523434openalex-snapshot
Islaris: verification of machine code against authoritative ISA semantics
inferredcites →https://doi.org/10.1145/512760.512766openalex-snapshot
Syntactic control of interference
inferredcites →https://doi.org/10.3233/jcs-160558openalex-snapshot
Provably secure memory isolation for Linux on ARM
inferredcites →https://doi.org/10.5281/zenodo.7320413openalex-snapshot
Data for "CN: Verifying Systems C Code with Separation-Logic Refinement Types"

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-74776-2_8openalex-snapshot
Should We Balance? Towards Formal Verification of the Linux Kernel Scheduler
inferred← citeshttps://doi.org/10.1016/j.cola.2024.101275openalex-snapshot
Towards a Dynabook for verified VM construction
inferred← citeshttps://doi.org/10.1016/j.scico.2026.103535openalex-snapshot
From C to verifiable Rust: Towards practical migration of code and specifications
inferred← citeshttps://doi.org/10.1109/dsn69566.2026.00081openalex-snapshot
AnBridge: Protecting On-Device AI with Android Virtualization Framework
inferred← citeshttps://doi.org/10.1109/icse55347.2025.00090openalex-snapshot
Neurosymbolic Modular Refinement Type Inference
inferred← citeshttps://doi.org/10.1109/iraset60544.2024.10549013openalex-snapshot
C Programs Formal Verification Using Maude
inferred← citeshttps://doi.org/10.1145/3632911openalex-snapshot
VST-A: A Foundationally Sound Annotation Verifier
inferred← citeshttps://doi.org/10.1145/3635800.3636965openalex-snapshot
Ownership Types for Verification of Programs with Pointer Arithmetic
inferred← citeshttps://doi.org/10.1145/3656413openalex-snapshot
Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq
inferred← citeshttps://doi.org/10.1145/3656422openalex-snapshot
RefinedRust: A Type System for High-Assurance Verification of Rust Programs
inferred← citeshttps://doi.org/10.1145/3689773openalex-snapshot
StarMalloc: Verifying a Modern, Hardened Memory Allocator
inferred← citeshttps://doi.org/10.1145/3694715.3695980openalex-snapshot
Practical Verification of System-Software Components Written in Standard C
inferred← citeshttps://doi.org/10.1145/3704879openalex-snapshot
Fulminate: Testing CN Separation-Logic Specifications in C
inferred← citeshttps://doi.org/10.1145/3704903openalex-snapshot
Generically Automating Separation Logic by Functors, Homomorphisms, and Modules
inferred← citeshttps://doi.org/10.1145/3729284openalex-snapshot
Destabilizing Iris
inferred← citeshttps://doi.org/10.1145/3747509openalex-snapshot
Formal Semantics and Program Logics for a Fragment of OCaml
inferred← citeshttps://doi.org/10.1145/3763151openalex-snapshot
Compositional Symbolic Execution for the Next 700 Memory Models
inferred← citeshttps://doi.org/10.1145/3764115openalex-snapshot
Bennet: Randomized Specification Testing for Heap-Manipulating Programs
inferred← citeshttps://doi.org/10.1145/3779212.3790171openalex-snapshot
Highly Automated Verification of Security Properties for Unmodified System Software
inferred← citeshttps://doi.org/10.1145/3786180.3788313openalex-snapshot
CNnotator: LLM-Guided Memory Safety Annotation Synthesis
inferred← citeshttps://doi.org/10.1145/3808278openalex-snapshot
Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows
inferred← citeshttps://doi.org/10.1145/3814943.3816182openalex-snapshot
A Pointer-Ownership Model for C Inspired by Rust
inferred← citeshttps://doi.org/10.1145/3832783.3837530openalex-snapshot
Generating Loop Invariants for Deductive Verification using Iterator Profiles
inferred← citeshttps://doi.org/10.1145/3837729.3840481openalex-snapshot
Fusion: A Fold and Unfold Annotation Synthesis Tool for Viper-Based Verification
inferred← citeshttps://doi.org/10.1145/3837729.3842144openalex-snapshot
Property-Based Testing of Separation Logic Specifications
inferred← citeshttps://doi.org/10.1145/3839513openalex-snapshot
Random Testing via Runtime Abstract Interpretation
inferred← citeshttps://doi.org/10.64552/wipiec.v10i1.53openalex-snapshot
C Software Formal Verification
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.