Modular Safety Checking for Fine-Grained Concurrency

No abstract is available for this paper.

• Publication year

  2007

• Venue

  Sensors Applications Symposium

• Publication date

  2007-08-22

• Fields of study

  Computer Science, Engineering, Environmental Science

• Identifiers
  DOI 10.1007/978-3-540-74061-2_15
• 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 Marriage of Rely/Guarantee and Separation Logic

  2007cited by this paper
• Modular verification of a non-blocking stack

  2007cited by this paper
• Thread-modular shape analysis

  2007cited by this paper
• Formal Verification of a Lazy Concurrent List-Based Set Algorithm

  2006cited by this paper
• Proving correctness of highly-concurrent linearisable objects

  2006cited by this paper
• A Local Shape Analysis Based on Separation Logic

  2006cited by this paper
• Smallfoot: Modular Automatic Assertion Checking with Separation Logic

  2005cited by this paper
• Modular verification of multithreaded programs

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

  2005cited by this paper
• Symbolic Execution with Separation Logic

  2005cited by this paper
• Affective Dialogue Systems

  2004cited by this paper
• Zing: Exploiting Program Structure for Model Checking Concurrent Software

  2004cited by this paper
• A Semantics for Concurrent Separation Logic

  2004cited by this paper
• Reversible Communicating Systems

  2004cited by this paper
• Summarizing procedures in concurrent programs

  2004cited by this paper
• Separation and information hiding

  2004cited by this paper
• The Spec# Programming System: An Overview

  2004cited by this paper
• Resources, Concurrency and Local Reasoning

  2004cited by this paper
• Mobile Resource Guarantees for Smart Devices

  2004cited by this paper
• Automatically Verifying Concurrent Queue Algorithms

  2003cited by this paper
• Thread-Modular Model Checking

  2003cited by this paper
• Thread-Modular Abstraction Refinement

  2003cited by this paper
• Extended static checking for Java

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

  2002cited by this paper
• Four-slot fully asynchronous communication mechanism

  1990cited by this paper
• The specification statement

  1988cited by this paper
• Specification and Design of (Parallel) Programs

  1983cited by this paper
• Myths About the Mutual Exclusion Problem

  1981cited by this paper
• The Temporal Semantics of Concurrent Programs

  1979cited by this paper
• Verifying properties of parallel programs: an axiomatic approach

  1976cited by this paper
• Symbolic execution and program testing

  1976cited by this paper

• Compositional Verification in Concurrent Separation Logic with Permissions Regions

  2025cites this paper
• A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras

  2024cites this paper
• Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic

  2023cites this paper
• Diaframe: automated verification of fine-grained concurrent programs in Iris

  2022cites this paper
• Rely-guarantee bound analysis of parameterized concurrent shared-memory programs

  2021influential citation
• Practical Abstractions for Automated Verification of Shared-Memory Concurrency

  2020cites this paper
• Concise outlines for a complex logic: a proof outline checker for TaDA

  2020cites this paper
• An Abstraction Technique for Verifying Shared-Memory Concurrency

  2020cites this paper
• Separation logic

  2019cites this paper
• Title : Caper : Automatic Verification for Fine-Grained Concurrency

  2019cites this paper
• Modelling concurrent objects running on the TSO and ARMv8 memory models

  2019cites this paper
• Static Code Verification Through Process Models

  2018cites this paper
• Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part III

  2018cites this paper
• Observational Models for Linearizability Checking on Weak Memory Models

  2018cites this paper
• Caper - Automatic Verification for Fine-Grained Concurrency

  2017cites this paper
• Program Verification with Separation Logic and Rely Guarantee

  2017cites this paper
• An Observational Approach to Defining Linearizability on Weak Memory Models

  2017cites this paper
• Caper: automatic verification for fine-grained concurrency

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

  2017cites this paper
• Modular Labelled Sequent Calculi for Abstract Separation Logics

  2017cites this paper
• A Proof Method for Linearizability on TSO Architectures

  2017cites this paper
• Invariant generation for linearizability proofs

  2016influential citation
• Concurrent separation logic

  2016influential citation
• Model Checking Simulation Rules for Linearizability

  2016cites this paper
• Mechanized verification of fine-grained concurrent programs

  2015cites this paper
• Automated Theorem Proving for Assertions in Separation Logic with All Connectives

  2015cites this paper
• Construcción de programas que manejan dinámicamente la memoria

  2015cites this paper
• Featherweight VeriFast

  2015cites this paper
• A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures

  2014cites this paper
• Admit Your Weakness: Verifying Correctness on TSO Architectures

  2014cites this paper
• Symbolic Abstraction: Algorithms and Applications

  2014cites this paper
• Satisfiability modulo abstraction for separation logic with linked lists

  2014cites this paper
• Software verification with VeriFast: Industrial case studies

  2014cites this paper
• Using Coarse-Grained Abstractions to Verify Linearizability on TSO Architectures

  2014cites this paper
• Verifying Linearizability on TSO Architectures

  2014cites this paper
• Specifying Concurrent Program Based on TLA

  2014cites this paper
• Taxonomies for software security

  2014cites this paper
• Verifying Concurrent Programs by Controlling Alias Interference

  2014cites this paper
• Model checking unbounded concurrent lists

  2013cites this paper
• Proof search for propositional abstract separation logics via labelled sequents

  2013cites this paper
• A Taxonomy Built on Layers of Abstraction for Time and State Vulnerabilities

  2013cites this paper
• Concurrent verification for sequential programs

  2013cites this paper
• Proving Simpson's Four-Slot Algorithm Using Ownership Transfer

  2012cites this paper
• SecureChange public project deliverable D6.6: Development-time and on-device interplay

  2012cites this paper
• Parameterized Model Checking of Fine Grained Concurrency

  2012cites this paper
• A Primer on Separation Logic (and Automatic Program Verification and Analysis)

  2012cites this paper
• A Taxonomy of Time and State Attacks

  2012cites this paper
• Separation Logic Expressiveness and Copyless Message-Passing

  2012cites this paper
• Proving Copyless Message Passing

  2012cites this paper
• Logics and analyses for concurrent heap-manipulating programs

  2011cites this paper
• Mechanically verified proof obligations for linearizability

  2011cites this paper
• Formal Methods-Based Tools for Race, Deadlock, and Other Errors

  2011cites this paper
• Permission-Based Separation Logic for Message-Passing Concurrency

  2011cites this paper
• Annotation Inference for Separation Logic Based Verifiers

  2011cites this paper
• Classical BI: Its Semantics and Proof Theory

  2010cites this paper
• VeriFast: Imperative Programs as Proofs

  2010cites this paper
• Resource Reasoning and Labelled Separation Logic

  2010cites this paper
• Explicit Stabilisation for Modular Rely-Guarantee Reasoning

  2010cites this paper
• Tracking Heaps That Hop with Heap-Hop

  2010cites this paper
• A Shape Analysis for Non-linear Data Structures

  2010cites this paper
• Proposal for ACDC2011 Doctoral Symposium

  2010influential citation
• VSTTE 2010 workshop proceedings

  2010cites this paper
• Modular verification of linked lists with views via separation logic

  2010cites this paper
• RGSep Action Inference

  2010influential citation
• Proving that non-blocking algorithms don't block

  2009influential citation
• Abstract Transformers for Thread Correlation Analysis

  2009cites this paper
• Classical BI: a logic for reasoning about dualising resources

  2009cites this paper
• Formal Verification of Lock-Free Algorithms (Invited Paper)

  2009cites this paper
• Efficiently Inferring Thread Correlations Technical Report TR-09-59203

  2009cites this paper
• Proving Copyless Message Passing

  2009cites this paper
• Formal Verification of Lock-Free Algorithms

  2009cites this paper
• Local rely-guarantee reasoning

  2009cites this paper
• Proving Linearizability with Temporal Logic

  2008cites this paper
• Modular fine-grained concurrency verification

  2008cites this paper
• TTIC-TR-2008-1 October 2008 Local Rely-Guarantee Reasoning

  2008cites this paper
• Towards Automatic Stability Analysis for Rely-Guarantee Proofs

  2008cites this paper
• Shape-Value Abstraction for Verifying Linearizability

  2008cites this paper
• The VeriFast program verifier

  2008cites this paper
• Reasoning on Abstract Matrix Structures 36

  2008influential citation
• Thread Quantification for Concurrent Shape Analysis

  2008cites this paper
• Cooperative Reasoning for Automatic Software Verification 2

  2008cites this paper
• VeriCool: An Automatic Verifier for a Concurrent Object-Oriented Language

  2008cites this paper
• Cooperative reasoning for automatic software verification

  2007cites this paper
• A Marriage of Rely/Guarantee and Separation Logic

  2007cites this paper
• H-w U F Y R Automated Reasoning for Separation Logic

  2007influential citation
• The Stability Problem for Verification of Concurrent Object-Oriented Programs

  2007cites this paper
• Under Consideration for Publication in Formal Aspects of Computing Proving Linearizability with Temporal Logic

  year unknowncites this paper