Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations

被引：0
|
作者：
Xavier Leroy
Sandrine Blazy
机构：
[1] INRIA Paris-Rocquencourt,
[2] ENSIIE,undefined
来源：
Journal of Automated Reasoning | 2008年 / 41卷
关键词：
Memory model; C; Program verification; Compilation; Compiler correctness; The Coq proof assistant;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
This article presents the formal verification, using the Coq proof assistant, of a memory model for low-level imperative languages such as C and compiler intermediate languages. Beyond giving semantics to pointer-based programs, this model supports reasoning over transformations of such programs. We show how the properties of the memory model are used to prove semantic preservation for three passes of the Compcert verified compiler.
引用
收藏
页码：1 / 31
页数：30
相关论文
共 50 条
  • [1] Formal verification of a C-like memory model and its uses for verifying program transformations
    Leroy, Xavier
    Blazy, Sandrine
    [J]. JOURNAL OF AUTOMATED REASONING, 2008, 41 (01) : 1 - 31
  • [2] Formal verification of a memory model for C-like imperative languages
    Blazy, S
    Leroy, X
    [J]. FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2005, 3785 : 280 - 299
  • [3] Formal verification for C program
    Qian, Junyan
    Xu, Baowen
    [J]. INFORMATICA, 2007, 18 (02) : 289 - 304
  • [4] REFINER: Towards Formal Verification of Model Transformations
    Wijs, Anton
    Engelen, Luc
    [J]. NASA FORMAL METHODS, NFM 2014, 2014, 8430 : 258 - 263
  • [5] A formal verification technique for behavioural model-to-model transformations
    de Putter, Sander
    Wijs, Anton
    [J]. FORMAL ASPECTS OF COMPUTING, 2018, 30 (01) : 3 - 43
  • [6] Formal Verification Techniques for Model Transformations: A Tridimensional Classification
    Amrani, Moussa
    Combemale, Benoit
    Lucio, Levi
    Selim, Gehan M. K.
    Dingel, Juergen
    Le Traon, Yves
    Vangheluwe, Hans
    Cordy, James R.
    [J]. JOURNAL OF OBJECT TECHNOLOGY, 2015, 14 (03):
  • [7] TSOtool: A program for verifying memory systems using the memory consistency model
    Hangal, S
    Vahia, D
    Manovit, C
    [J]. 31ST ANNUAL INTERNATIONAL SYMPOSIUM ON COMPUTER ARCHITECTURE, PROCEEDINGS, 2004, : 114 - 123
  • [8] Formal Verification Techniques for Model Transformations Specified By-Demonstration
    Gabmeyer, Sebastian
    [J]. 2012 PROCEEDINGS OF THE 27TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE), 2012, : 390 - 393
  • [9] Automated Formal Verification of Model Transformations Using the Invariants Mechanism
    Ulitin, Boris
    Babkin, Eduard
    Babkina, Tatiana
    Vizgunov, Arsenii
    [J]. PERSPECTIVES IN BUSINESS INFORMATICS RESEARCH, BIR 2019, 2019, 365 : 59 - 73
  • [10] Formal verification of coherence for a shared memory multiprocessor model
    Barrio-Solórzano, M
    Beato, ME
    Cuesta, CE
    de la Fuente, P
    [J]. PARALLEL COMPUTING TECHNOLOGIES, 2001, 2127 : 17 - 26
12345