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 条
  • [41] 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
  • [42] Verification Systems and Programs in Regional Television Stations That Are Members of the CIRCOM Network
    Ruas-Araujo, Jose
    Rodriguez-Martelo, Talia
    Maiz-Bar, Carmen
    JOURNALISM AND MEDIA, 2022, 3 (01): : 1 - 12
  • [43] Calculating Parallel Programs in Coq Using List Homomorphisms
    Frédéric Loulergue
    Wadoud Bousdira
    Julien Tesson
    International Journal of Parallel Programming, 2017, 45 : 300 - 319
  • [44] Calculating Parallel Programs in Coq Using List Homomorphisms
    Loulergue, Frederic
    Bousdira, Wadoud
    Tesson, Julien
    INTERNATIONAL JOURNAL OF PARALLEL PROGRAMMING, 2017, 45 (02) : 300 - 319
  • [45] Interaction Trees Representing Recursive and Impure Programs in Coq
    Xia, Li-yao
    Zakowski, Yannick
    He, Paul
    Hur, Chung-Kil
    Malecha, Gregory
    Pierce, Benjamin C.
    Zdancewic, Steve
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2020, 4 (POPL):
  • [46] Mostly-Automated Verification of Low-Level Programs in Computational Separation Logic
    Chlipala, Adam
    ACM SIGPLAN NOTICES, 2011, 46 (06) : 234 - 245
  • [47] Mostly-Automated Verification of Low-Level Programs in Computational Separation Logic
    Chlipala, Adam
    PLDI 11: PROCEEDINGS OF THE 2011 ACM CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION, 2011, : 234 - 245
  • [48] Kleene Algebra with Tests and Coq Tools for while Programs
    Pous, Damien
    INTERACTIVE THEOREM PROVING, ITP 2013, 2013, 7998 : 180 - 196
  • [49] A Combined Computational and Experimental Study to Investigate the Role of COQ9 in Promoting COQ Biosynthesis
    Aydin, Deniz
    Lohman, Danielle C.
    Pagliarini, David J.
    Dal Peraro, Matteo
    BIOPHYSICAL JOURNAL, 2018, 114 (03) : 460A - 460A
  • [50] Scallina: Translating Verified Programs from Coq to Scala
    El Bakouny, Youssef
    Mezher, Dani
    PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2018, 2018, 11275 : 131 - 145
12345