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 条
  • [1] Computational Verification of Network Programs for Several OpenFlow Switches in Coq
    Date, Hiroaki
    Yoshiura, Noriaki
    COMPUTATIONAL SCIENCE AND ITS APPLICATIONS - ICCSA 2016, PT II, 2016, 9787 : 223 - 238
  • [2] Verification of Java programs in Coq
    Department of Computer Science, Royal Holloway University of London, Surrey, United Kingdom
    Comput. Sci. Electron. Eng. Conf., CEEC,
  • [3] A Coq Library for Verification of Concurrent Programs
    Affeldt, Reynald
    Kobayashi, Naoki
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 199 : 17 - 32
  • [4] Modular Verification of Programs with Effects and Effect Handlers in Coq
    Letan, Thomas
    Regis-Gianas, Yann
    Chifflier, Pierre
    Hiet, Guillaume
    FORMAL METHODS, 2018, 10951 : 338 - 354
  • [5] Verification of PCP-Related Computational Reductions in Coq
    Forster, Yannick
    Heiter, Edith
    Smolka, Gert
    INTERACTIVE THEOREM PROVING, ITP 2018, 2018, 10895 : 253 - 269
  • [6] Verification of computational electromagnetic programs
    Ida, N
    INTERNATIONAL JOURNAL OF NUMERICAL MODELLING-ELECTRONIC NETWORKS DEVICES AND FIELDS, 1996, 9 (1-2) : 159 - 165
  • [7] Analytical Verification of Computational Programs
    Petrenko, Sergey A.
    Stupin, Dmitry D.
    FIFTH INTERNATIONAL CONFERENCE ON ENGINEERING AND TELECOMMUNICATION (ENT-MIPT 2018), 2018, : 172 - 175
  • [8] COQ Cock Correct! Verification of Type Checking and Erasure for COQ, in COQ
    Sozeau, Matthieu
    Boulier, Simon
    Forster, Yannick
    Tabareau, Nicolas
    Winterhalter, Theo
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2020, 4 (POPL):
  • [9] Extracting functional programs from Coq, in Coq
    Annenkov, Danil
    Milo, Mikkel
    Nielsen, Jakob Botsch
    Spitters, Bas
    JOURNAL OF FUNCTIONAL PROGRAMMING, 2022, 32 (05)
  • [10] Tutorial: Practical Verification of Network Programs
    Foster, Nate
    Guha, Arjun
    Reitblatt, Mark
    Schlesinger, Cole
    2013 FORMAL METHODS IN COMPUTER-AIDED DESIGN (FMCAD), 2013, : 9 - +
12345