Practical abstractions for automated verification of message passing concurrency

DOI10.1007/978-3-030-34968-4_22zbMATH Open1540.68156MaRDI QIDQ6536355

Wytse Oortwijn, Marieke Huisman

Publication date: 19 April 2024

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A semantics for concurrent separation logic
• Resources, concurrency, and local reasoning
• 25 years of model checking. History, achievements, perspectives
• An abstraction technique for describing concurrent program behaviour
• Verifying data- and control-oriented properties combining static and runtime verification: theory and tools
• Concurrency verification. Introduction to compositional and noncompositional methods
• Viper: A Verification Infrastructure for Permission-Based Reasoning
• Modular Reasoning for Message-Passing Programs
• Combining Model Checking and Deduction
• Permission-Based Separation Logic for Message-Passing Concurrency
• A Marriage of Rely/Guarantee and Separation Logic
• Modular Reasoning about Separation of Concurrent Data Structures
• Communicating State Transition Systems for Fine-Grained Concurrent Resources
• Concurrent Separation Logic and Operational Semantics
• Software reliability methods. Foreword by Edmund M. Clarke

This page was built for publication: Practical abstractions for automated verification of message passing concurrency