CSimpl: a rely-guarantee-based framework for verifying concurrent programs

DOI10.1007/978-3-662-54577-5_28MaRDI QIDQ3303910zbMATH OpenOpenAlexFDO

Authors David Sanán, Yongwang Zhao, Zhé Hóu, Fuyuan Zhang, Alwen Tiu, Yang Liu

Publication date 5 August 2020

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/10072/395143

zbMATH Keywords

concurrent programinference ruleparallel compositionproof systemsequential program

Mathematics Subject Classification ID

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

Recommendations

• Compositional reasoning for shared-variable concurrent programs
• Verification of concurrent systems with VerCors
• scientific article; zbMATH DE number 1956564
• A Coq library for verification of concurrent programs
• Specification and verification of concurrent programs through refinements

Cites work

• A Marriage of Rely/Guarantee and Separation Logic
• A Structural Proof of the Soundness of Rely/guarantee Rules
• An axiomatic proof technique for parallel programs
• scientific article; zbMATH DE number 1956564 (Why is no real title available?)
• Local rely-guarantee reasoning
• Logic for Programming, Artificial Intelligence, and Reasoning
• The Rely-Guarantee method for verifying shared variable concurrent programs

Cited in

(8)

• Proof tactics for assertions in separation logic
• A rely-guarantee-based simulation for verifying concurrent program transformations
• scientific article; zbMATH DE number 1487492 (Why is no real title available?)
• CompCertTSO
• A parametric rely-guarantee reasoning framework for concurrent reactive systems
• Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding
• ConcurrentHOL
• Clean - An Abstract Imperative Programming Language and its Theory

Describes a project that uses

Uses Software

• seL4
• CSimpl
• Isabelle/HOL
• Locales

This page was built for publication: CSimpl: a rely-guarantee-based framework for verifying concurrent programs

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