Computational verification of network programs in Coq

DOI10.1007/978-3-319-03545-1_3MaRDI QIDQ2938038zbMATH OpenOpenAlexFDO

Authors Gordon Stewart

Publication date 13 January 2015

Published in Certified Programs and Proofs (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-03545-1_3

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• NetKAT -- a formal system for the verification of networks
• Netkat, semantic foundations for networks
• Modular development of certified program verifiers with a proof assistant,
• scientific article; zbMATH DE number 1670759
• Scaling network verification using symmetry and surgery

Cited in

(10)

• Building reliable, high-performance networks with the Nuprl proof development system
• Safe compositional network sketches: formal framework
• Efficient SMT-based network fault tolerance verification
• scientific article; zbMATH DE number 6905198 (Why is no real title available?)
• Some complexity results for stateful network verification
• Scaling network verification using symmetry and surgery
• Towards Certifying Network Calculus
• NetKAT -- a formal system for the verification of networks
• Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
• SAT based verification of network data planes

Describes a project that uses

Uses Software

• Anteater
• NetCore
• z3
• OTTER
• Coq

This page was built for publication: Computational verification of network programs in Coq

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2938038)