Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free
From MaRDI portal
Publication:2058383
DOI10.1007/s10703-021-00370-8OpenAlexW3139745505MaRDI QIDQ2058383
Thomas Pani, Florian Zuleger, Georg Weissenbacher
Publication date: 8 December 2021
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10703-021-00370-8
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Programs with lists are counter automata
- A scalable lock-free stack algorithm
- The Rely-Guarantee method for verifying shared variable concurrent programs
- Automated resource analysis with Coq proof objects
- Automatically proving termination and memory safety for programs with pointer arithmetic
- Complexity and resource bound analysis of imperative programs using difference constraints
- Rely-guarantee termination and cost analyses of loops with concurrent interleavings
- Closed-form upper bounds in static cost analysis
- Resource Analysis of Complex Programs with Cost Equations
- Automatic Inference of Resource Consumption Bounds
- Static Analysis of Run-Time Errors in Embedded Critical Parallel C Programs
- From Shapes to Amortized Complexity
- Thread Quantification for Concurrent Shape Analysis
- Thread-Modular Verification Is Cartesian Abstract Interpretation
- Shape-Value Abstraction for Verifying Linearizability
- Modular Safety Checking for Fine-Grained Concurrency
- RGSep Action Inference
- Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs
- Aspect-oriented linearizability proofs
- Proving that non-blocking algorithms don't block
- Compositional shape analysis by means of bi-abduction
- An Integrated Specification and Verification Technique for Highly Concurrent Data Structures
- Formal Techniques for Networked and Distributed Systems – FORTE 2004
This page was built for publication: Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free
