scholarly journals Exploiting Pointer Analysis in Memory Models for Deductive Verification

2019 ◽  
pp. 160-182
Author(s):  
Quentin Bouillaguet ◽  
François Bobot ◽  
Mihaela Sighireanu ◽  
Boris Yakobowski
Keyword(s):  
Memory Models ◽  
Pointer Analysis ◽  
Deductive Verification

scholarly journals Integrating Owicki–Gries for C11-Style Memory Models into Isabelle/HOL

2021 ◽  
Author(s):  
Sadegh Dalvandi ◽  
Brijesh Dongol ◽  
Simon Doherty ◽  
Heike Wehrheim
Keyword(s):  
Program Verification ◽  
Memory Models ◽  
Theorem Prover ◽  
Hoare Logic ◽  
Deductive Verification ◽  
High Level

AbstractWeak memory presents a new challenge for program verification and has resulted in the development of a variety of specialised logics. For C11-style memory models, our previous work has shown that it is possible to extend Hoare logic and Owicki–Gries reasoning to verify correctness of weak memory programs. The technique introduces a set of high-level assertions over C11 states together with a set of basic Hoare-style axioms over atomic weak memory statements (e.g. reads/writes), but retains all other standard proof obligations for compound statements. This paper takes this line of work further by introducing the first deductive verification environment in Isabelle/HOL for C11-like weak memory programs. This verification environment is built on the Nipkow and Nieto’s encoding of Owicki–Gries in the Isabelle theorem prover. We exemplify our techniques over several litmus tests from the literature and two non-trivial examples: Peterson’s algorithm and a read–copy–update algorithm adapted for C11. For the examples we consider, the proof outlines can be automatically discharged using the existing Isabelle tactics developed by Nipkow and Nieto. The benefit here is that programs can be written using a familiar pseudocode syntax with assertions embedded directly into the program.

A Measurement Modelling Framework for Complex Working Memory Models

2011 ◽  
Author(s):  
Klaus Oberauer ◽  
Jarrold Chris ◽  
Farrell Simon ◽  
Lewandowsky Stephan
Keyword(s):  
Working Memory ◽  
Memory Models ◽  
Modelling Framework ◽  
Working Memory Models

The Semantic Credentials of High-Dimensional Memory Models

2014 ◽  
Author(s):  
Curt Burgess ◽  
Sarah Maples
Keyword(s):  
Memory Models ◽  
High Dimensional

Pointer Analysis

2015 ◽  
Author(s):  
Yannis Smaragdakis ◽  
George Balatsouras
Keyword(s):  
Pointer Analysis

Heterogeneous-race-free memory models

2014 ◽  
Vol 42 (1) ◽  
pp. 427-440
Author(s):  
Derek R. Hower ◽  
Blake A. Hechtman ◽  
Bradford M. Beckmann ◽  
Benedict R. Gaster ◽  
Mark D. Hill ◽  
...  
Keyword(s):  
Memory Models

Dynamic partial order reduction for relaxed memory models

2015 ◽  
Vol 50 (6) ◽  
pp. 250-259 ◽  
Author(s):  
Naling Zhang ◽  
Markus Kusano ◽  
Chao Wang
Keyword(s):  
Partial Order ◽  
Order Reduction ◽  
Memory Models ◽  
Partial Order Reduction ◽  
Relaxed Memory
Sign in / Sign up

Export Citation Format

Share Document