A program logic for concurrent objects under fair scheduling

No abstract is available for this paper.

• Publication year

  2016

• Venue

  ACM-SIGACT Symposium on Principles of Programming Languages

• Publication date

  2016-01-11

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1145/2837614.2837635
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Modular Termination Verification for Non-blocking Concurrency (Extended Version)

  2016cited by this paper
• Modular Termination Verification for Non-blocking Concurrency

  2016cited by this paper
• Modular Termination Verification

  2015cited by this paper
• Modular Verification of Finite Blocking in Non-terminating Programs

  2015cited by this paper
• Compositional verification of termination-preserving refinement of concurrent programs

  2014influential reference
• Modular verification of linearizability with non-fixed linearization points

  2013cited by this paper
• Characterizing Progress Properties of Concurrent Objects via Contextual Refinements

  2013cited by this paper
• Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency

  2013cited by this paper
• Quantitative Reasoning for Proving Lock-Freedom

  2013influential reference
• Mechanically verified proof obligations for linearizability

  2011cited by this paper
• On the Nature of Progress

  2011influential reference
• Liveness-Preserving Atomicity Abstraction

  2011cited by this paper
• Deadlock-Free Channels and Locks

  2010cited by this paper
• A Basis for Verifying Multi-threaded Programs

  2009cited by this paper
• Proving that non-blocking algorithms don't block

  2009cited by this paper
• Abstraction for concurrent objects

  2009cited by this paper
• Local rely-guarantee reasoning

  2009influential reference
• Modular fine-grained concurrency verification

  2008influential reference
• Variables as Resource in Hoare Logics

  2006cited by this paper
• Static Deadlock Detection for Java Libraries

  2005cited by this paper
• A Lazy Concurrent List-Based Set Algorithm

  2005cited by this paper
• Ownership types for safe programming: preventing data races and deadlocks

  2002cited by this paper
• Refinement of fair action systems

  1998cited by this paper
• The rely-guarantee method for verifying shared variable concurrent programs

  1997cited by this paper
• Fair Simulation

  1997cited by this paper
• Simple, fast, and practical non-blocking and blocking concurrent queue algorithms

  1996cited by this paper
• Conjoining specifications

  1995cited by this paper
• Shared-state design modulo weak and strong process fairness

  1992cited by this paper
• Algorithms for scalable synchronization on shared-memory multiprocessors

  1991cited by this paper
• Linearizability: a correctness condition for concurrent objects

  1990cited by this paper
• A Proof Technique for Rely/Guarantee Properties

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

  1983influential reference

• Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness

  2025cites this paper
• CCR 2.0: High-level Reasoning for Conditional Refinements

  2025cites this paper
• Generalized Security-Preserving Refinement for Concurrent Systems

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

  2025cites this paper
• All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs

  2025cites this paper
• Encode the ∀∃ Relational Hoare Logic into Standard Hoare Logic

  2025cites this paper
• Practical Rely/Guarantee Verification of an Efficient Lock for seL4 on Multicore Architectures

  2024cites this paper
• Structural Temporal Logic for Mechanized Program Verification

  2024cites this paper
• Non-termination Proving at Scale

  2024cites this paper
• Fully Verified Instruction Scheduling

  2024cites this paper
• Refinement Composition Logic

  2024cites this paper
• Algebraic Effects Meet Hoare Logic in Cubical Agda

  2024cites this paper
• Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing

  2024cites this paper
• A program logic for obstruction-freedom

  2023cites this paper
• Conditional Contextual Refinement

  2023cites this paper
• SimplMM: A simplified and abstract multicore hardware model for large scale system software formal verification

  2023cites this paper
• <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline" id="d1e861" altimg="si142.svg"><mml:mi mathvariant="sans-serif">ThreadAbs</mml:mi></mml:math>: A template to build verified thread-local interfaces with software scheduler abstractions

  2023cites this paper
• Trillium: History-Sensitive Refinement in Separation Logic

  2023cites this paper
• Fair Operational Semantics

  2023cites this paper
• A Formal Approach to Design and Security Verification of Operating Systems for Intelligent Transportation Systems Based on Object Model

  2023cites this paper
• A Compositional Theory of Linearizability

  2023cites this paper
• Simuliris: a separation logic framework for verifying concurrent program optimizations

  2022cites this paper
• Verifying Contextual Refinement with Ownership Transfer

  2021cites this paper
• Actor-based model checking for Software-Defined Networks

  2021cites this paper
• Transfinite Iris: resolving an existential dilemma of step-indexed separation logic

  2021cites this paper
• Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement

  2021cites this paper
• Formal design and verification of system task in intelligent transportation systems based on micro-kernel architecture

  2021cites this paper
• Ghost Signals: Verifying Termination of Busy-Waiting (Extended Version)

  2020cites this paper
• Ghost Signals: Verifying Termination of Busy-Waiting

  2020cites this paper
• A separation logic to verify termination of busy-waiting for abrupt program exit

  2020cites this paper
• Actor-Based Model Checking for SDN Networks

  2020cites this paper
• Cloud computing based load balancing algorithm for erlang concurrent traffic

  2020cites this paper
• Verifying Termination of Busy-Waiting

  2020cites this paper
• TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs

  2019influential citation
• Building certified concurrent OS kernels

  2019cites this paper
• SDN-Actors: Modeling and Verification of SDN Programs

  2018cites this paper
• Paxos Consensus, Deconstructed and Abstracted (Extended Version)

  2018cites this paper
• 2 The Single-Decree Paxos Algorithm

  2018cites this paper
• Certified concurrent abstraction layers

  2018cites this paper
• A Concurrent Perspective on Smart Contracts

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

  2017influential citation
• Programming and proving with distributed protocols

  2017cites this paper
• Designing persistent heap for byte addressable NVRAM

  2017cites this paper
• Safety and Liveness of MCS Lock - Layer by Layer

  2017cites this paper
• Progress of concurrent objects with partial methods

  2017cites this paper
• Concurrent separation logic

  2016cites this paper
• Reasoning with time and data abstractions

  2016cites this paper
• Towards a Thread-Local Proof Technique for Starvation Freedom

  2016influential citation
• Lawyer: Modular Obligations-Based Liveness Reasoning in Higher-Order Impredicative Concurrent Separation Logic

  year unknowncites this paper
• This paper is included in the Proceedings of the 18th USENIX Symposium on Operating Systems Design and Implementation.

  year unknowninfluential citation
• This Paper Is Included in the Proceedings of the 12th Usenix Symposium on Operating Systems Design and Implementation (osdi '16). Certikos: an Extensible Architecture for Building Certified Concurrent Os Kernels Certikos: an Extensible Architecture for Building Certified Concurrent Os Kernels

  year unknowncites this paper