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

inference ruleconcurrent programproof systemparallel compositionsequential 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

• scientific article; zbMATH DE number 1956564 (Why is no real title available?)
• 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
• Local rely-guarantee reasoning
• Logic for Programming, Artificial Intelligence, and Reasoning
• The Rely-Guarantee method for verifying shared variable concurrent programs

Cited in

(6)

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

Describes a project that uses

Uses Software

• CSimpl
• seL4
• Locales
• Isabelle/HOL

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)