COMPLX: A Verification Framework for Concurrent Imperative Programs

CPP, pp. 138-150, 2017.

Cited by: 4|Bibtex|Views52
EI
Other Links: dblp.uni-trier.de|dl.acm.org|academic.microsoft.com

Abstract:

We propose a concurrency reasoning framework for imperative programs, based on the Owicki-Gries (OG) foundational shared-variable concurrency method. Our framework combines the approaches of Hoare-Parallel, a formalisation of OG in Isabelle/HOL for a simple while-language, and Simpl, a generic imperative language embedded in Isabelle/HOL,...More

Code:

Data:

Your rating :
0

 

Tags
Comments