On the public citation graph
Compositional Verification and Refinement of Concurrent Value-Dependent Noninterference
0 signed · 84 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/3-540-45949-9openalex-snapshot
Isabelle/HOL: A Proof Assistant for Higher-Order Logic
inferredcites →https://doi.org/10.1007/978-3-319-08970-6_25openalex-snapshot
An Isabelle Proof Method Language
inferredcites →https://doi.org/10.1007/978-3-319-27436-2_12openalex-snapshot
Using Dynamic Pushdown Networks to Automate a Modular Information-Flow Analysis
inferredcites →https://doi.org/10.1007/978-3-319-28766-9_7openalex-snapshot
Disjunctive Information Flow for Communicating Processes
inferredcites →https://doi.org/10.1007/978-3-540-71316-6_13openalex-snapshot
On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning
inferredcites →https://doi.org/10.1007/978-3-540-71316-6_35openalex-snapshot
Dependent Types for Low-Level Programming
inferredcites →https://doi.org/10.1007/978-3-540-74407-8_18openalex-snapshot
A Marriage of Rely/Guarantee and Separation Logic
inferredcites →https://doi.org/10.1007/978-3-642-11957-6_28openalex-snapshot
Enforcing Stateful Authorization and Information Flow Policies in Fine
inferredcites →https://doi.org/10.1007/978-3-642-35308-6_12openalex-snapshot
Noninterference for Operating System Kernels
inferredcites →https://doi.org/10.1007/s10207-007-0019-9openalex-snapshot
Dynamic security labels and static information flow control
inferredcites →https://doi.org/10.1007/s10817-015-9360-2openalex-snapshot
Eisbach: A Proof Method Language for Isabelle
inferredcites →https://doi.org/10.1016/0011-684x(85)90108-xopenalex-snapshot
Communicating sequential processes
inferredcites →https://doi.org/10.1016/j.entcs.2009.08.017openalex-snapshot
On Refinement-Closed Security Properties and Nondeterministic Compositions
inferredcites →https://doi.org/10.1016/s0304-3975(02)00010-5openalex-snapshot
Noninterference for concurrent programs and thread systems
inferredcites →https://doi.org/10.1109/csf.2011.22openalex-snapshot
Assumptions and Guarantees for Compositional Noninterference
inferredcites →https://doi.org/10.1109/csf.2015.17openalex-snapshot
Hybrid Monitors for Concurrent Noninterference
inferredcites →https://doi.org/10.1109/csfw.2000.856937openalex-snapshot
Probabilistic noninterference for multi-threaded programs
inferredcites →https://doi.org/10.1109/jsac.2002.806121openalex-snapshot
Language-based information-flow security
inferredcites →https://doi.org/10.1109/lics.2000.855785openalex-snapshot
Imperative programming with dependent types
inferredcites →https://doi.org/10.1109/secpri.2001.924289openalex-snapshot
Preserving information flow properties under refinement
inferredcites →https://doi.org/10.1109/sp.2011.12openalex-snapshot
Verification of Information Flow and Access Control Policies with Dependent Types
inferredcites →https://doi.org/10.1145/1111037.1111046openalex-snapshot
A logic for information flow in object-oriented programs
inferredcites →https://doi.org/10.1145/1111320.1111046openalex-snapshot
A logic for information flow in object-oriented programs
inferredcites →https://doi.org/10.1145/2034574.2034811openalex-snapshot
Secure distributed programming with value-dependent types
inferredcites →https://doi.org/10.1145/2034773.2034811openalex-snapshot
Secure distributed programming with value-dependent types
inferredcites →https://doi.org/10.1145/2505879.2505895openalex-snapshot
Dependent types for enforcement of information flow and erasure policies in heterogeneous data structures
inferredcites →https://doi.org/10.1145/2576235openalex-snapshot
Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations
inferredcites →https://doi.org/10.1145/2603088.2603123openalex-snapshot
Compositional verification of termination-preserving refinement of concurrent programs
inferredcites →https://doi.org/10.1145/2676726.2676994openalex-snapshot
Dependent Information Flow Types
inferredcites →https://doi.org/10.1145/2694344.2694372openalex-snapshot
A Hardware Design Language for Timing-Sensitive Information-Flow Security
inferredcites →https://doi.org/10.1145/2775054.2694372openalex-snapshot
A Hardware Design Language for Timing-Sensitive Information-Flow Security
inferredcites →https://doi.org/10.25405/ncl.34131210openalex-snapshot
Development methods for computer programs including a notion of interference
inferredcites →https://doi.org/10.3233/jcs-1999-72-305openalex-snapshot
Probabilistic noninterference in a concurrent language1
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-03638-6_2openalex-snapshot
Tracking Information Flow via Delayed Output
inferred← citeshttps://doi.org/10.1007/978-3-030-25543-5_13openalex-snapshot
SecCSL: Security Concurrent Separation Logic
inferred← citeshttps://doi.org/10.1007/978-3-030-30942-8_11openalex-snapshot
A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems
inferred← citeshttps://doi.org/10.1007/978-3-030-30942-8_32openalex-snapshot
Value-Dependent Information-Flow Security on Weak Memory Models
inferred← citeshttps://doi.org/10.1007/978-3-030-54997-8_21openalex-snapshot
An Abstract Semantics of Speculative Execution for Reasoning About Security Vulnerabilities
inferred← citeshttps://doi.org/10.1007/978-3-030-89051-3_6openalex-snapshot
Fully Abstract and Robust Compilation
inferred← citeshttps://doi.org/10.1007/978-3-031-08166-8_4openalex-snapshot
A Case Study in Information Flow Refinement for Low Level Systems
inferred← citeshttps://doi.org/10.1007/978-3-031-71162-6_25openalex-snapshot
Detecting Speculative Execution Vulnerabilities on Weak Memory Models
inferred← citeshttps://doi.org/10.1007/978-3-031-98208-8_19openalex-snapshot
Detecting Speculative Data Flow Vulnerabilities Using Weakest Precondition Reasoning
inferred← citeshttps://doi.org/10.1007/978-3-319-66197-1_19openalex-snapshot
Modular Verification of Information Flow Security in Component-Based Systems
inferred← citeshttps://doi.org/10.1007/978-3-319-66402-6_26openalex-snapshot
A Better Composition Operator for Quantitative Information Flow Analyses
inferred← citeshttps://doi.org/10.1007/978-3-319-71237-6_3openalex-snapshot
Taming Message-Passing Communication in Compositional Reasoning About Confidentiality
inferred← citeshttps://doi.org/10.1007/978-3-319-89722-6openalex-snapshot
Principles of Security and Trust
inferred← citeshttps://doi.org/10.1007/978-3-319-89722-6_3openalex-snapshot
Compositional Non-interference for Concurrent Programs via Separation and Framing
inferred← citeshttps://doi.org/10.1007/s10703-021-00376-2openalex-snapshot
Information-flow control on ARM and POWER multicore processors
inferred← citeshttps://doi.org/10.1007/s10817-025-09744-7openalex-snapshot
Relative Security: (Dis)Proving Resilience Against Semantic Optimization Vulnerabilities in Isabelle/HOL
inferred← citeshttps://doi.org/10.1016/j.cola.2019.100904openalex-snapshot
Enforcing globally dependent flow policies in message-passing systems
inferred← citeshttps://doi.org/10.1016/j.cose.2021.102343openalex-snapshot
A security type verifier for smart contracts
inferred← citeshttps://doi.org/10.1016/j.jlamp.2017.12.003openalex-snapshot
MAC A verified static information-flow control library
inferred← citeshttps://doi.org/10.1017/s0956796821000162openalex-snapshot
Verified secure compilation for mixed-sensitivity concurrent programs
inferred← citeshttps://doi.org/10.1109/csf.2017.17openalex-snapshot
Towards a Flow- and Path-Sensitive Information Flow Analysis
inferred← citeshttps://doi.org/10.1109/csf.2018.00023openalex-snapshot
A Permission-Dependent Type System for Secure Information Flow Analysis
inferred← citeshttps://doi.org/10.1109/csf.2018.00031openalex-snapshot
Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic “Constant-Time”
inferred← citeshttps://doi.org/10.1109/csf49147.2020.00014openalex-snapshot
VERONICA: Expressive and Precise Concurrent Information Flow Security
inferred← citeshttps://doi.org/10.1109/csf49147.2020.00034openalex-snapshot
Rely/Guarantee Reasoning for Noninterference in Non-Blocking Algorithms
inferred← citeshttps://doi.org/10.1109/csf51468.2021.00010openalex-snapshot
On Compositional Information Flow Aware Refinement
inferred← citeshttps://doi.org/10.1109/csf51468.2021.00017openalex-snapshot
Backwards-directed information flow analysis for concurrent programs
inferred← citeshttps://doi.org/10.1109/csf51468.2021.00020openalex-snapshot
Secure Compilation of Constant-Resource Programs
inferred← citeshttps://doi.org/10.1109/eurosp.2018.00010openalex-snapshot
COVERN: A Logic for Compositional Verification of Information Flow Control
inferred← citeshttps://doi.org/10.1109/eurosp53844.2022.00036openalex-snapshot
Compositional Information Flow Monitoring for Reactive Programs
inferred← citeshttps://doi.org/10.1109/formalise58978.2023.00017openalex-snapshot
A Dafny-based approach to thread-local information flow analysis
inferred← citeshttps://doi.org/10.1109/sp40001.2021.00003openalex-snapshot
Compositional Non-Interference for Fine-Grained Concurrent Programs
inferred← citeshttps://doi.org/10.1109/sp40001.2021.00049openalex-snapshot
A Secure and Formally Verified Linux KVM Hypervisor
inferred← citeshttps://doi.org/10.1145/2993600.2993603openalex-snapshot
Future-dependent Flow Policies with Prophetic Variables
inferred← citeshttps://doi.org/10.1145/3264820.3264824openalex-snapshot
Prudent Design Principles for Information Flow Control
inferred← citeshttps://doi.org/10.1145/3276485openalex-snapshot
A derivation framework for dependent security label inference
inferred← citeshttps://doi.org/10.1145/3371075openalex-snapshot
Formal verification of a constant-time preserving C compiler
inferred← citeshttps://doi.org/10.1145/3434291openalex-snapshot
Mechanized logical relations for termination-insensitive noninterference
inferred← citeshttps://doi.org/10.1145/3460860openalex-snapshot
An Extended Account of Trace-relating Compiler Correctness and Secure Compilation
inferred← citeshttps://doi.org/10.1145/3485476openalex-snapshot
SecRSL: security separation logic for C11 release-acquire concurrency
inferred← citeshttps://doi.org/10.1145/3719027.3765138openalex-snapshot
Generalized Security-Preserving Refinement for Concurrent Systems
inferred← citeshttps://doi.org/10.3233/jcs-200036openalex-snapshot
A permission-dependent type system for secure information flow analysis
inferred← citeshttps://doi.org/10.32657/10356/136764openalex-snapshot
Securing software systems via fuzz testing and verification
inferred← citeshttps://doi.org/10.4230/lipics.itp.2019.27openalex-snapshot
Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security
inferred← citeshttps://doi.org/10.48550/arxiv.2001.11142openalex-snapshot
VERONICA: Expressive and Precise Concurrent Information Flow Security (Extended Version with Technical Appendices)
inferred← citeshttps://doi.org/10.48550/arxiv.2006.14969openalex-snapshot
Fully Abstract and Robust Compilation and How to Reconcile the Two, Abstractly
inferred← citeshttps://doi.org/10.48550/arxiv.2109.03602openalex-snapshot
SecRSL: Security Separation Logic for C11 Release-Acquire Concurrency (Extended version with technical appendices)
inferred← citeshttps://doi.org/10.5204/thesis.eprints.226908openalex-snapshot
Static analysis of software components for information flow security
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.