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 条
  • [21] ON THE COMPUTATIONAL-COMPLEXITY OF OPTIMAL SORTING NETWORK VERIFICATION
    PARBERRY, I
    LECTURE NOTES IN COMPUTER SCIENCE, 1991, 505 : 252 - 269
  • [22] Formal verification of cP systems using Coq
    Liu, Yezhou
    Nicolescu, Radu
    Sun, Jing
    JOURNAL OF MEMBRANE COMPUTING, 2021, 3 (03) : 205 - 220
  • [23] Functional Verification of High Performance Adders in Coq
    Wang, Qian
    Song, Xiaoyu
    Gu, Ming
    Sun, Jiaguang
    JOURNAL OF APPLIED MATHEMATICS, 2014,
  • [24] Coinductive Natural Semantics for Compiler Verification in Coq
    Zuniga, Angel
    Bel-Enguix, Gemma
    MATHEMATICS, 2020, 8 (09)
  • [25] Modular development of hybrid systems for verification in Coq
    Niqui, Milad
    Tveretina, Olga
    HYBRID SYSTEMS: COMPUTATION AND CONTROL, 2008, 4981 : 638 - 641
  • [26] Foundational Program Verification in Coq with Automated Proofs
    Chlipala, Adam
    MSFP 2010: PROCEEDINGS OF THE 2010 ACM SIGPLAN WORKSHOP ON MATHEMATICALLY STRUCTURED FUNCTIONAL PROGRAMMING, 2010, : 19 - 19
  • [27] 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
  • [28] Formal verification of cP systems using Coq
    Yezhou Liu
    Radu Nicolescu
    Jing Sun
    Journal of Membrane Computing, 2021, 3 : 205 - 220
  • [29] Safety verification of dynamic storage management in coq
    Xiang, Sen
    Chen, Yiyun
    Lin, Chunxiao
    Li, Long
    Jisuanji Yanjiu yu Fazhan/Computer Research and Development, 2007, 44 (02): : 361 - 367
  • [30] 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
12345