Practical abstractions for automated verification of shared-memory concurrency

DOI10.1007/978-3-030-39322-9_19MaRDI QIDQ784156zbMATH OpenOpenAlexFDO

Authors Wytse Oortwijn, Dilian Gurov, Marieke Huisman

Publication date 5 August 2020

Full work available at URL http://hdl.handle.net/20.500.11850/465582

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• An abstraction technique for describing concurrent program behaviour
• Practical abstractions for automated verification of message passing concurrency
• An integrated specification and verification technique for highly concurrent data structures
• Compositional reasoning for shared-variable concurrent programs
• Safety and Liveness in Concurrent Pointer Programs

Cited in

(5)

• Effective Abstractions for Verification under Relaxed Memory Models
• scientific article; zbMATH DE number 7295368 (Why is no real title available?)
• Parameterized Verification of Asynchronous Shared-Memory Systems
• Practical abstractions for automated verification of message passing concurrency
• Caper

Describes a project that uses

Uses Software

• CIVL
• Viper
• VerCors
• Threader
• VeriFast
• Chalice

This page was built for publication: Practical abstractions for automated verification of shared-memory concurrency

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q784156)