CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs

DOI10.1007/978-3-662-54577-5_28zbMath1452.68053OpenAlexW2600478067MaRDI QIDQ3303910

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

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 ruleproof systemconcurrent programparallel compositionsequential program

Mathematics Subject Classification ID

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)

Related Items (1)

Proof tactics for assertions in separation logic

Uses Software

• Unnamed Item
• Locales
• seL4
• CSimpl

Cites Work

• Unnamed Item
• An axiomatic proof technique for parallel programs
• The Rely-Guarantee method for verifying shared variable concurrent programs
• A Marriage of Rely/Guarantee and Separation Logic
• Local rely-guarantee reasoning
• A Structural Proof of the Soundness of Rely/guarantee Rules
• Logic for Programming, Artificial Intelligence, and Reasoning

This page was built for publication: CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs