Mechanized proofs of opacity: a comparison of two techniques
- Submitting institution
-
The University of Sheffield
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 2547
- Type
- D - Journal article
- DOI
-
10.1007/s00165-017-0433-3
- Title of journal
- Formal Aspects of Computing
- Article number
- -
- First page
- 597
- Volume
- 30
- Issue
- 5
- ISSN
- 0934-5043
- Open access status
- Compliant
- Month of publication
- August
- Year of publication
- 2017
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
5
- Research group(s)
-
I - Verification
- Citation count
- 1
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Software transactional memory (STM) produces more reliable yet highly concurrent code. Opacity is the key correctness criteria, crucial for industrial take up: the latest chips have STM. Here we develop two different opacity proof methods, compare them, and mechanically verify all our results. These are the first, and so far only, methods to be mechanically verified. We show how one method allows a compositional proof, which helps reduce the complexity. The work is a result of a national and international collaboration (Kent, Surrey, ARM, Paderborn and Augsburg) funded by a series of EPSRC projects on the verification of concurrent algorithms.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -