Abstract
We provide simple equational principles for deriving rely-guarantee-style inference rules and refinement laws based on idempotent semirings. We link the algebraic layer with concrete models of programs based on languages and execution traces. We have implemented the approach in Isabelle/HOL as a lightweight concurrency verification tool that supports reasoning about the control and data flow of concurrent programs with shared variables at different levels of abstraction. This is illustrated on a simple verification example. © 2014 Springer International Publishing Switzerland.
Cite
CITATION STYLE
Armstrong, A., Gomes, V. B. F., & Struth, G. (2014). Algebraic principles for rely-guarantee style concurrency verification tools. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8442 LNCS, pp. 78–93). Springer Verlag. https://doi.org/10.1007/978-3-319-06410-9_6
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
