Safety verification of dynamic storage management in coq

被引：0
|
作者：
Xiang, Sen [1 ]
Chen, Yiyun [1 ]
Lin, Chunxiao [1 ]
Li, Long [1 ]
机构：
[1] Department of Computer Science and Technology, University of Science and Technology of China, Hefei 230027, China
来源：
Jisuanji Yanjiu yu Fazhan/Computer Research and Development | 2007年 / 44卷 / 02期
关键词：
Software engineering;
D O I：
10.1360/crad20070225
中图分类号：
学科分类号：
摘要：
引用
收藏
页码：361 / 367
相关论文
共 50 条
  • [21] Formal Modeling and Verification of Paxos Based on Coq
    Li Y.-N.
    Deng Y.-X.
    Liu J.
    Ruan Jian Xue Bao/Journal of Software, 2020, 31 (08): : 2362 - 2374
  • [22] Formal verification of cP systems using Coq
    Yezhou Liu
    Radu Nicolescu
    Jing Sun
    Journal of Membrane Computing, 2021, 3 : 205 - 220
  • [23] Coq Implementation of OO Verification Framework VeriJ
    Zhang, Ke
    Qiu, Zongyan
    SOFTWARE ENGINEERING AND FORMAL METHODS: 14TH INTERNATIONAL CONFERENCE, SEFM 2016, 2016, 9763 : 270 - 276
  • [24] Modeling and Verification of CKB Consensus Protocol in Coq
    Luan, Xiaokun
    Sun, Meng
    2021 21ST INTERNATIONAL CONFERENCE ON SOFTWARE QUALITY, RELIABILITY AND SECURITY COMPANION (QRS-C 2021), 2021, : 660 - 667
  • [25] MCOQ : Mutation Analysis for Coq Verification Projects
    Jain, Kush
    Palmskog, Karl
    Celik, Ahmet
    Arias, Emilio Jesus Gallego
    Gligoric, Milos
    2020 ACM/IEEE 42ND INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING: COMPANION PROCEEDINGS (ICSE-COMPANION 2020), 2020, : 89 - 92
  • [26] Circuits as streams in Coq: Verification of a sequential multiplier
    Paulin-Mohring, C
    TYPES FOR PROOFS AND PROGRAMS, 1996, 1158 : 216 - 230
  • [27] Formal Verification of Distributed Dynamic Thermal Management
    Ismail, Muhammad
    Hasan, Osman
    Ebi, Thomas
    Shafique, Muhammad
    Henkel, Joerg
    2013 IEEE/ACM INTERNATIONAL CONFERENCE ON COMPUTER-AIDED DESIGN (ICCAD), 2013, : 248 - 255
  • [28] Propellant Storage and Injection of Safety Management
    Yue Chun-guo
    Zhang Yu-xiang
    Zhang You-hong
    Chang Xin-long
    Zhang Shi-ying
    2011 3RD WORLD CONGRESS IN APPLIED COMPUTING, COMPUTER SCIENCE, AND COMPUTER ENGINEERING (ACC 2011), VOL 2, 2011, 2 : 271 - 276
  • [29] A Coq library for internal verification of running-times
    McCarthy, Jay
    Fetscher, Burke
    New, Max S.
    Feltey, Daniel
    Findler, Robert Bruce
    SCIENCE OF COMPUTER PROGRAMMING, 2018, 164 : 49 - 65
  • [30] Verification of Management Methods for Power Storage in Wind Parks
    Sourkounis, Constantinos
    Richter, Florian
    Ni, Bingchang
    CPE: 2009 COMPATIBILITY AND POWER ELECTRONICS, 2009, : 134 - 138
12345