Computational Verification of Network Programs in Coq

被引：0
|
作者：
Stewart, Gordon [1 ]
机构：
[1] Princeton Univ, Princeton, NJ 08544 USA
来源：
CERTIFIED PROGRAMS AND PROOFS, CPP 2013 | 2013年 / 8307卷
基金：
美国国家科学基金会;
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We report on the design of the first fully automatic, machine-checked tool suite for verification of high-level network programs. The tool suite targets programs written in NetCore, a new declarative network programming language. Our work builds on a recent effort by Guha, Reitblatt, and Foster to build a machine-verified compiler from NetCore to OpenFlow, a new protocol for software-defined networking.
引用
收藏
页码：33 / 49
页数：17
相关论文
共 50 条
  • [31] 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
  • [32] 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
  • [33] Circuits as streams in Coq: Verification of a sequential multiplier
    Paulin-Mohring, C
    TYPES FOR PROOFS AND PROGRAMS, 1996, 1158 : 216 - 230
  • [34] Practical Tactics for Verifying C Programs in Coq
    Cao, Jingyuan
    Fu, Ming
    Feng, Xinyu
    CPP'15: PROCEEDINGS OF THE 2015 ACM CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, 2015, : 97 - 108
  • [35] 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
  • [36] Verification of PLC Properties Based on Formal Semantics in Coq
    Blech, Jan Olaf
    Biha, Sidi Ould
    SOFTWARE ENGINEERING AND FORMAL METHODS, 2011, 7041 : 58 - +
  • [37] QWIRE Practice: Formal Verification of Quantum Circuits in Coq
    Rand, Robert
    Paykin, Jennifer
    Zdancewic, Steve
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2018, (266): : 119 - 132
  • [38] Description and Verification of Pattern-Based Composition in Coq
    Liu, Qiang
    Ynag, Zhongyuan
    Xie, Jinkui
    ADVANCES IN COMPUTATIONAL SCIENCE AND ENGINEERING, 2009, 28 : 231 - 245
  • [39] Using Coq for Formal Modeling and Verification of Timed Connectors
    Hong, Weijiang
    Nawaz, M. Saqib
    Zhang, Xiyue
    Li, Yi
    Sun, Meng
    SOFTWARE ENGINEERING AND FORMAL METHODS, SEFM 2017, 2018, 10729 : 558 - 573
  • [40] Formalisation and verification of programmable logic controllers timers in Coq
    Wan, H.
    Chen, G.
    Song, X.
    Gu, M.
    IET SOFTWARE, 2011, 5 (01) : 32 - 42
12345