Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations

No abstract is available for this paper.

• Publication year

  2014

• Venue

  ACM Transactions on Programming Languages and Systems

• Publication date

  2014-03-01

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1145/2576235
• 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 rely-guarantee-based simulation for verifying concurrent program transformations

  2012cited by this paper
• A separation logic for refining concurrent objects

  2011cited by this paper
• A kripke logical relation between ML and assembly

  2011cited by this paper
• Relaxed-memory concurrency and verified compilation

  2011cited by this paper
• Fine-grained Concurrency with Separation Logic

  2011cited by this paper
• Verifying a Compiler for Java Threads

  2010cited by this paper
• Simplifying Linearizability Proofs with Reduction and Abstraction

  2010cited by this paper
• Formal Derivation of Concurrent Garbage Collectors

  2010cited by this paper
• Verifying Local Transformations on Relaxed Memory Models

  2010cited by this paper
• A Formally Verified Compiler Back-end

  2009influential reference
• A model of cooperative threads

  2009cited by this paper
• Abstraction for concurrent objects

  2009cited by this paper
• Biorthogonality, step-indexing and compiler correctness

  2009cited by this paper
• Local rely-guarantee reasoning

  2009cited by this paper
• Modular fine-grained concurrency verification

  2008influential reference
• Foundations of the C++ concurrency memory model

  2008cited by this paper
• A Marriage of Rely/Guarantee and Separation Logic

  2007cited by this paper
• A general framework for certifying garbage collectors and their mutators

  2007cited by this paper
• Relational separation logic

  2007cited by this paper
• HP Laboratories

  2006cited by this paper
• Transactional Locking II

  2006influential reference
• Correctness-preserving derivation of concurrent garbage collection algorithms

  2006cited by this paper
• Variables as Resource in Hoare Logics

  2006cited by this paper
• A parallel, incremental, mostly concurrent garbage collector for servers

  2005influential reference
• Simple relational correctness proofs for static analyses and program transformations

  2004cited by this paper
• Separation logic: a logic for shared mutable data structures

  2002cited by this paper
• The coq proof assistant reference manual

  2000cited by this paper
• Compiler Correctness for Concurrent Languages

  1996cited by this paper
• Compiler correctness for parallel languages

  1995cited by this paper
• Full abstraction for a shared variable parallel language

  1993influential reference
• Guest editor's introduction to the special section on the third international conference on computer languages

  1992cited by this paper
• Mostly parallel garbage collection

  1991cited by this paper
• The existence of refinement mappings

  1988cited by this paper
• Tentative steps toward a development method for interfering programs

  1983cited by this paper
• Proof of correctness of data representations

  1972cited by this paper

• A Forward Simulation-Based Hierarchy of Linearizable Concurrent Objects

  2026cites this paper
• A Brief History of Formal Methods in China

  2025cites this paper
• A Brookes-Style Denotational Semantics for Release/Acquire Concurrency

  2025cites this paper
• A Denotational Approach to Release/Acquire Concurrency

  2024cites this paper
• A Proof System for the SMrCaIT Calculus

  2024cites this paper
• Compositional Semantics for Shared-Variable Concurrency

  2024cites this paper
• Data reification in a concurrent rely-guarantee algebra

  2024cites this paper
• A Compositional Theory of Linearizability

  2023cites this paper
• Survey of the Formal Verification of Operating Systems in Power Monitoring System

  2023cites this paper
• Sequential reasoning for optimizing compilers under weak memory concurrency

  2022cites this paper
• Abstraction for Crash-Resilient Objects (Extended Version)

  2021cites this paper
• CSim2

  2021influential citation
• Rely-Guarantee Reasoning about Messaging System for Autonomous Vehicles

  2020cites this paper
• Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example

  2019cites this paper
• Pointer life cycle types for lock-free data structures with memory reclamation

  2019cites this paper
• Verified compilation of linearizable data structures: mechanizing rely guarantee for semantic refinement

  2018cites this paper
• Test-Based Security Certification of Composite Services

  2018cites this paper
• Decoupling lock-free data structures from memory reclamation for static analysis

  2018cites this paper
• Compilation of Linearizable Data Structures

  2017cites this paper
• VERIFIED COMPILATION OF CONCURRENT MANAGED

  2017cites this paper
• High-Assurance Separation Kernels: A Survey on Formal Methods

  2017cites this paper
• Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology

  2017cites this paper
• A Higher-Order Logic for Concurrent Termination-Preserving Refinement

  2017cites this paper
• Interactive Theorem Proving: 8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Proceedings

  2017cites this paper
• Compositional Verification and Refinement of Concurrent Value-Dependent Noninterference

  2016cites this paper
• Compositional Reasoning for Shared-variable Concurrent Programs

  2016cites this paper
• Towards certified compilation of RTFM-core applications

  2016cites this paper
• Short Paper: On High-Assurance Information-Flow-Secure Programming Languages

  2015cites this paper
• Automated and Modular Refinement Reasoning for Concurrent Programs

  2015cites this paper
• Refinement Verification of Concurrent Programs and Its Applications

  2014cites this paper
• Verified Compilation of Linearizable Data Structures ∗ Mechanizing Rely Guarantee for Semantic Refinement

  year unknowncites this paper