More Web Proxy on the site http://driver.im/

research-article

Open access

Modular Control Plane Verification via Temporal Invariants

Authors:

Timothy Alberdingk Thijm,

David WalkerAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 7, Issue PLDI

Article No.: 108, Pages 50 - 75

https://doi.org/10.1145/3591222

Published: 06 June 2023 Publication History

Abstract

Monolithic control plane verification cannot scale to hyperscale network architectures with tens of thousands of nodes, heterogeneous network policies and thousands of network changes a day. Instead, modular verification offers improved scalability, reasoning over diverse behaviors, and robustness following policy updates. We introduce Timepiece, a new modular control plane verification system. While one class of verifiers, starting with Minesweeper, were based on analysis of stable paths, we show that such models, when deployed naïvely for modular verification, are unsound. To rectify the situation, we adopt a routing model based around a logical notion of time and develop a sound, expressive, and scalable verification engine.

Our system requires that a user specifies interfaces between module components. We develop methods for defining these interfaces using predicates inspired by temporal logic, and show how to use those interfaces to verify a range of network-wide properties such as reachability or access control. Verifying a prefix-filtering policy using a non-modular verification engine times out on an 80-node fattree network after 2 hours. However, Timepiece verifies a 2,000-node fattree in 2.37 minutes on a 96-core virtual machine. Modular verification of individual routers is embarrassingly parallel and completes in seconds, which allows verification to scale beyond non-modular engines, while still allowing the full power of SMT-based symbolic reasoning.

References

[1]

Anubhavnidhi Abhashkumar, Aaron Gember-Jacobson, and Aditya Akella. 2020. Tiramisu: Fast multilayer network verification. In NSDI. USENIX Association, Santa Clara, CA, USA. 201–219. https://www.usenix.org/system/files/nsdi20-paper-abhashkumar.pdf

[2]

Anubhavnidhi Abhashkumar, Kausik Subramanian, Alexey Andreyev, Hyojeong Kim, Nanda Kishore Salem, Jingyi Yang, Petr Lapukhov, Aditya Akella, and Hongyi Zeng. 2021. Running BGP in Data Centers at Scale. In 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21). USENIX Association, USA. 65–81. isbn:978-1-939133-21-2 https://www.usenix.org/conference/nsdi21/presentation/abhashkumar

[3]

Mohammad Al-Fares, Alexander Loukissas, and Amin Vahdat. 2008. A Scalable, Commodity Data Center Network Architecture. In SIGCOMM. ACM, Seattle, WA, USA. 63–74. https://doi.org/10.1145/1402946.1402967

Digital Library

[4]

Timothy Alberdingk Thijm and Ryan Beckett. 2023. Timepiece. https://github.com/alberdingk-thijm/Timepiece

[5]

Timothy Alberdingk Thijm and Ryan Beckett. 2023. Timepiece. https://zenodo.org/record/7799158

[6]

Timothy Alberdingk Thijm, Ryan Beckett, Aarti Gupta, and David Walker. 2022. Kirigami, the Verifiable Art of Network Cutting. In 2022 IEEE 30th International Conference on Network Protocols (ICNP). IEEE, Lexington, KY, USA. 1–12. https://doi.org/10.1109/ICNP55882.2022.9940333

[7]

Timothy Alberdingk Thijm, Ryan Beckett, Aarti Gupta, and David Walker. 2022. Modular Control Plane Verification via Temporal Invariants. https://doi.org/10.48550/arXiv.2204.10303 arxiv:2204.10303.

[8]

Rajeev Alur and Thomas A Henzinger. 1999. Reactive modules. Formal methods in system design, 15, 1 (1999), 7–48. https://doi.org/10.1023/A:1008739929481

Digital Library

[9]

Clark Barrett and Cesare Tinelli. 2018. Satisfiability modulo theories. In Handbook of model checking. Springer, Cham, Switzerland. 305–343. https://doi.org/10.1007/978-3-319-10575-8_11

[10]

Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker. 2017. A General Approach to Network Configuration Verification. In SIGCOMM. ACM, New York, NY, USA. 155–168. https://doi.org/10.1145/3098822.3098834

Digital Library

[11]

Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker. 2018. Control Plane Compression. In SIGCOMM. ACM, Budapest, Hungary. 476–489. isbn:978-1-4503-5567-4 https://doi.org/10.1145/3230543.3230583

Digital Library

[12]

Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker. 2019. Abstract Interpretation of Distributed Network Control Planes. Proc. ACM Program. Lang., 4, POPL (2019), Article 42, dec, 27 pages. https://doi.org/10.1145/3371110

Digital Library

[13]

Ryan Beckett and Ratul Mahajan. 2020. A General Framework for Compositional Network Modeling. In Proceedings of the 19th ACM Workshop on Hot Topics in Networks. Association for Computing Machinery, New York, NY, USA. 8–15. https://doi.org/10.1145/3422604.3425930

Digital Library

[14]

Ryan Beckett, Ratul Mahajan, Todd Millstein, Jitendra Padhye, and David Walker. 2016. Don’T Mind the Gap: Bridging Network-wide Objectives and Device-level Configurations. In SIGCOMM. ACM, New York, NY, USA. 328–341. https://doi.org/10.1145/2934872.2934909

Digital Library

[15]

Ryan Beckett, Ratul Mahajan, Todd Millstein, Jitu Padhye, and David Walker. 2017. Network Configuration Synthesis with Abstract Topologies. In PLDI. ACM, New York, NY, USA. 437–451. https://doi.org/10.1145/3062341.3062367

Digital Library

[16]

Mihaela Gheorghiu Bobaru, Corina S. Pasareanu, and Dimitra Giannakopoulou. 2008. Automated Assume-Guarantee Reasoning by Abstraction Refinement. In CAV (Lecture Notes in Computer Science, Vol. 5123). Springer-Verlag, Berlin, Heidelberg. 135–148. https://doi.org/10.1007/978-3-540-70545-1_14

Digital Library

[17]

CISCO. 2005. Using BGP Community Values to Control Routing Policy in Upstream Provider Network. https://www.cisco.com/c/en/us/support/docs/ip/border-gateway-protocol-bgp/28784-bgp-community.html

[18]

Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. 2000. Counterexample-Guided Abstraction Refinement. In CAV. Springer, Berlin, Heidelberg. 154–169. https://doi.org/10.1007/10722167_15

[19]

Jamieson M. Cobleigh, Dimitra Giannakopoulou, and Corina S. Pasareanu. 2003. Learning Assumptions for Compositional Verification. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS, Proceedings (Lecture Notes in Computer Science, Vol. 2619). Springer, Berlin, Heidelberg. 331–346. https://doi.org/10.1007/3-540-36577-X_24

[20]

Ariel Cohen and Kedar S. Namjoshi. 2007. Local Proofs for Global Safety Properties. In Computer Aided Verification (CAV), Proceedings (Lecture Notes in Computer Science, Vol. 4590). Springer, USA. 55–67. https://doi.org/10.5555/1519231.1519265

Digital Library

[21]

Matthew L Daggitt, Alexander JT Gurney, and Timothy G Griffin. 2018. Asynchronous convergence of policy-rich distributed Bellman-Ford routing protocols. In SIGCOMM. ACM, Budapest, Hungary. 103–116. https://doi.org/10.1145/3230543.3230561

Digital Library

[22]

Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In TACAS. Springer, Berlin, Heidelberg. 337–340. https://doi.org/10.1007/978-3-540-78800-3_24

[23]

Ankush Desai, Amar Phanishayee, Shaz Qadeer, and Sanjit A. Seshia. 2018. Compositional programming and testing of dynamic distributed systems. PACMPL, 2, OOPSLA (2018), 159:1–159:30. https://doi.org/10.1145/3276529

Digital Library

[24]

Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, and Sharon Shoham. 2018. Automated circular assume-guarantee reasoning. Formal Aspects of Computing, 30, 5 (2018), 571–595. https://doi.org/10.1007/s00165-017-0436-0

Digital Library

[25]

Seyed K. Fayaz, Tushar Sharma, Ari Fogel, Ratul Mahajan, Todd Millstein, Vyas Sekar, and George Varghese. 2016. Efficient Network Reachability Analysis using a Succinct Control Plane Representation. In OSDI. USENIX Association, Savannah, GA, USA. 217–232. https://dl.acm.org/doi/10.5555/3026877.3026895

[26]

Nick Feamster and Hari Balakrishnan. 2005. Detecting BGP Configuration Faults with Static Analysis. In NSDI. USENIX Association, USA. 43–56. https://doi.org/10.5555/1251203.1251207

Digital Library

[27]

Cormac Flanagan and Shaz Qadeer. 2003. Thread-modular model checking. In International SPIN Workshop on Model Checking of Software. Springer, Berlin, Heidelberg. 213–224. https://doi.org/10.1007/3-540-44829-2_14

[28]

Ari Fogel, Stanley Fung, Luis Pedrosa, Meg Walraed-Sullivan, Ramesh Govindan, Ratul Mahajan, and Todd Millstein. 2015. A General Approach to Network Configuration Analysis. In NSDI. USENIX Association, USA. 469–483. https://doi.org/10.5555/2789770.2789803

Digital Library

[29]

Aaron Gember-Jacobson, Raajay Viswanathan, Aditya Akella, and Ratul Mahajan. 2016. Fast Control Plane Analysis Using an Abstract Representation. In SIGCOMM. ACM, USA. 300–313. https://doi.org/10.1145/2934872.2934876

Digital Library

[30]

Dimitra Giannakopoulou, Kedar S Namjoshi, and Corina S Păsăreanu. 2018. Compositional reasoning. In Handbook of Model Checking. Springer, Cham, Switzerland. 345–383. https://doi.org/10.1007/978-3-319-10575-8_12

[31]

Nick Giannarakis, Devon Loehr, Ryan Beckett, and David Walker. 2020. NV: An Intermediate Language for Verification of Network Control Planes. In PLDI. Association for Computing Machinery, New York, NY, USA. 958–973. isbn:9781450376136 https://doi.org/10.1145/3385412.3386019

Digital Library

[32]

Timothy G. Griffin, F. Bruce Shepherd, and Gordon Wilfong. 2002. The Stable Paths Problem and Interdomain Routing. IEEE/ACM Trans. Networking, 10, 2 (2002), April, 232–243. https://ieeexplore.ieee.org/abstract/document/993304

Digital Library

[33]

Timothy G. Griffin and Joäo Luís Sobrinho. 2005. Metarouting. In SIGCOMM. ACM, New York, NY, USA. 1–12. https://doi.org/10.1145/1080091.1080094

Digital Library

[34]

Orna Grumberg and David E Long. 1994. Model checking and modular verification. ACM Transactions on Programming Languages and Systems (TOPLAS), 16, 3 (1994), 843–871. https://doi.org/10.1145/177492.177725

Digital Library

[35]

Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko. 2011. Threader: A Constraint-Based Verifier for Multi-threaded Programs. In Computer Aided Verification (CAV). Proceedings (Lecture Notes in Computer Science, Vol. 6806). Springer, Berlin, Heidelberg. 412–417. https://doi.org/10.1007/978-3-642-22110-1_32

[36]

Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath T. V. Setty, and Brian Zill. 2015. IronFleet: proving practical distributed systems correct. In SOSP. ACM, New York, NY, USA. 1–17. https://doi.org/10.1145/2815400.2815428

Digital Library

[37]

C. Hedrick. 1988. Routing Information Protocol. Internet Request for Comments. https://datatracker.ietf.org/doc/html/rfc1058

[38]

Thomas A Henzinger, Shaz Qadeer, and Sriram K Rajamani. 1998. You assume, we guarantee: Methodology and case studies. In International Conference on Computer Aided Verification. Springer, Berlin, Heidelberg. 440–451. https://doi.org/10.1007/BFb0028765

[39]

Thomas A. Henzinger, Shaz Qadeer, and Sriram K. Rajamani. 2000. Decomposing Refinement Proofs Using Assume-Guarantee Reasoning. In Proceedings of the 2000 IEEE/ACM International Conference on Computer-Aided Design (ICCAD). IEEE Computer Society, San Jose, CA, USA. 245–252. https://doi.org/10.5555/602902.602958

Digital Library

[40]

Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani, and Serdar Tasiran. 2002. An assume-guarantee rule for checking simulation. ACM Transactions on Programming Languages and Systems, 24, 1 (2002), 51–64. https://doi.org/10.1145/509705.509707

Digital Library

[41]

Internet2. 2013. About Internet2. https://meetings.internet2.edu/media/medialibrary/2013/08/01/AboutInternet2.pdf

[42]

Karthick Jayaraman, Nikolaj Bjørner, Jitu Padhye, Amar Agrawal, Ashish Bhargava, Paul-Andre C Bissonnette, Shane Foster, Andrew Helwer, Mark Kasten, Ivan Lee, Anup Namdhari, Haseeb Niaz, Aniruddha Parkhi, Hanukumar Pinnamraju, Adrian Power, Neha Milind Raje, and Parag Sharma. 2019. Validating Datacenters at Scale. In SIGCOMM. Association for Computing Machinery, Beijing, China. 200–213. isbn:9781450359566 https://doi.org/10.1145/3341302.3342094

Digital Library

[43]

Karthick Jayaraman, Nikolaj Bjørner, Jitu Padhye, Amar Agrawal, Ashish Bhargava, Paul-Andre C Bissonnette, Shane Foster, Andrew Helwer, Mark Kasten, Ivan Lee, Anup Namdhari, Haseeb Niaz, Aniruddha Parkhi, Hanukumar Pinnamraju, Adrian Power, Neha Milind Raje, and Parag Sharma. 2019. Validating Datacenters at Scale (Presentation at SIGCOMM 2019). https://conferences.sigcomm.org/sigcomm/2019/files/slides/paper_5_1.pptx

[44]

Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In POPL. ACM, New York, NY, USA. 637–650. https://doi.org/10.1145/2775051.2676980

Digital Library

[45]

Peyman Kazemian, Michael Chang, Hongyi Zeng, George Varghese, Nick McKeown, and Scott Whyte. 2013. Real Time Network Policy Checking Using Header Space Analysis. In NSDI. USENIX Association, USA. 99–112. https://doi.org/10.5555/2482626.2482638

Digital Library

[46]

Ahmed Khurshid, Xuan Zou, Wenxuan Zhou, Matthew Caesar, and P. Brighten Godfrey. 2013. VeriFlow: Verifying Network-Wide Invariants in Real Time. In NSDI. USENIX Association, USA. 15–28. https://doi.org/10.5555/2482626.2482630

Digital Library

[47]

R. P. Kurshan. 1988. Reducibility in analysis of coordination. In Discrete Event Systems: Models and Applications (LNCIS, Vol. 103). Springer, Berlin, Heidelberg. 19–39. https://doi.org/10.1007/BFb0042302

[48]

K Rustan M Leino. 2010. Dafny: An automatic program verifier for functional correctness. In International Conference on Logic for Programming Artificial Intelligence and Reasoning. Springer, Berlin, Heidelberg. 348–370. https://doi.org/10.1007/978-3-642-17511-4_20

[49]

Alessio Lomuscio, Ben Strulo, Nigel Walker, and Peng Wu. 2010. Assume-guarantee reasoning with local specifications. In ICFEM. Springer, Berlin, Heidelberg. 204–219. https://doi.org/10.1007/978-3-642-16901-4_15

[50]

Nuno P. Lopes, Nikolaj Bjørner, Patrice Godefroid, Karthick Jayaraman, and George Varghese. 2015. Checking Beliefs in Dynamic Networks. In NSDI. USENIX Association, Oakland, CA. 499–512. https://doi.org/10.5555/2789770.2789805

Digital Library

[51]

Nuno P Lopes and Andrey Rybalchenko. 2019. Fast BGP simulation of large datacenters. In VMCAI. Springer, Cham, Switzerland. 386–408. https://doi.org/10.1007/978-3-030-11245-5_18

[52]

K. Lougheed and Y. Rekhter. 1991. A Border Gateway Protocol 3 (BGP-3). Internet Request for Comments. https://datatracker.ietf.org/doc/html/rfc1267

[53]

Haojun Ma, Aman Goel, Jean-Baptiste Jeannin, Manos Kapritsos, Baris Kasikci, and Karem A. Sakallah. 2019. I4: incremental inference of inductive invariants for verification of distributed protocols. In SOSP. ACM, Huntsville, ON, Canada. 370–384. https://doi.org/10.1145/3341301.3359651

Digital Library

[54]

Kenneth L. McMillan. 1997. A Compositional Rule for Hardware Design Refinement. In Computer Aided Verification (CAV), Proceedings (Lecture Notes in Computer Science, Vol. 1254). Springer, Berlin, Heidelberg. 24–35. https://doi.org/10.1007/3-540-63166-6_6

[55]

Microsoft. 2021. Introduction to PLINQ. https://docs.microsoft.com/en-us/dotnet/standard/parallel-programming/introduction-to-plinq

[56]

Ron Miller. 2022. As overall cloud infrastructure market growth dips to 24%, AWS reports slowdown. https://techcrunch.com/2022/10/28/as-overall-cloud-infrastructure-market-growth-dips-to-24-aws-reports-slowdown/

[57]

Jayadev Misra and K. Mani Chandy. 1981. Proofs of Networks of Processes. IEEE Transactions on Software Engineering, 7, 4 (1981), 417–426. https://doi.org/10.1109/TSE.1981.230844

Digital Library

[58]

J. Moy. 1998. Open Shortest Path First Protocol Version 2. Internet Request for Comments. https://datatracker.ietf.org/doc/html/rfc2328

[59]

D. Oran. 1990. OSI IS-IS Intra-domain Routing Protocol. Internet Request for Comments. https://datatracker.ietf.org/doc/html/rfc1142

[60]

Susan S. Owicki and David Gries. 1976. Verifying Properties of Parallel Programs: An Axiomatic Approach. Commun. ACM, 19, 5 (1976), 279–285. https://doi.org/10.1145/360051.360224

Digital Library

[61]

Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, and Sharon Shoham. 2016. Ivy: safety verification by interactive generalization. In PLDI. ACM, New York, NY, USA. 614–630. https://doi.org/10.1145/2908080.2908118

Digital Library

[62]

Ivan Pepelnjak. 2018. Valley-Free Routing in Data Center Fabrics. https://blog.ipspace.net/2018/09/valley-free-routing-in-data-center.html

[63]

Amir Pnueli. 1984. In Transition From Global to Modular Temporal Reasoning about Programs. In Logics and Models of Concurrent Systems - Conference proceedings (NATO ASI Series, Vol. 13). Springer, Berlin, Heidelberg. 123–144. https://doi.org/10.1007/978-3-642-82453-1_5

[64]

Santhosh Prabhu, Kuan Yen Chou, Ali Kheradmand, Brighten Godfrey, and Matthew Caesar. 2020. Plankton: Scalable network configuration verification through model checking. In NSDI. USENIX Association, Santa Clara, CA, USA. 953–967. isbn:9781939133137 https://doi.org/10.5555/3388242.3388310

Digital Library

[65]

Ilya Sergey, James R. Wilcox, and Zachary Tatlock. 2018. Programming and proving with distributed protocols. Proceedings of ACM Programming Languages, 2, POPL (2018), 28:1–28:30. https://doi.org/10.1145/3158116

Digital Library

[66]

SMT-LIB. 2010. ArraysEx. https://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml

[67]

SMT-LIB. 2010. FixedSizeBitVectors. https://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml

[68]

SMT-LIB. 2010. Ints. https://smtlib.cs.uiowa.edu/theories-Ints.shtml

[69]

SMT-LIB. 2020. Unicode Strings. http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml

[70]

João Luís Sobrinho. 2005. An Algebraic Theory of Dynamic Network Routing. IEEE/ACM Trans. Netw., 13, 5 (2005), October, 1160–1173. https://ieeexplore.ieee.org/abstract/document/1528502

Digital Library

[71]

Tom Strickx and Jeremy Hartman. 2022. Cloudflare outage on June 21, 2022. https://blog.cloudflare.com/cloudflare-outage-on-june-21-2022/

[72]

Alan Tang, Ryan Beckett, Karthick Jayaraman, Todd Millstein, and George Varghese. 2022. LIGHTYEAR: Using Modularity to Scale BGP Control Plane Verification. arxiv:2204.09635. arxiv:2204.09635

[73]

Brandon Vigliarolo. 2022. After config error takes down Rogers, it promises to spend billions on reliability. https://www.theregister.com/2022/07/25/canadian_isp_rogers_outage/

[74]

Konstantin Weitz. 2016. Getting Started With Bagpipe. http://www.konne.me/bagpipe/started.html

[75]

Konstantin Weitz, Doug Woos, Emina Torlak, Michael D. Ernst, Arvind Krishnamurthy, and Zachary Tatlock. 2016. Scalable Verification of Border Gateway Protocol Configurations with an SMT Solver. In OOPSLA. Association for Computing Machinery, New York, NY, USA. 765–780. isbn:9781450344449 https://doi.org/10.1145/2983990.2984012

Digital Library

[76]

Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh, Suman Jana, and Gabriel Ryan. 2021. DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols. In OSDI. USENIX Association, USA. 405–421. https://www.usenix.org/conference/osdi21/presentation/yao

[77]

Fangdan Ye, Da Yu, Ennan Zhai, Hongqiang Harry Liu, Bingchuan Tian, Qiaobo Ye, Chunsheng Wang, Xin Wu, Tianchen Guo, Cheng Jin, Duncheng She, Qing Ma, Biao Cheng, Hui Xu, Ming Zhang, Zhiliang Wang, and Rodrigo Fonseca. 2020. Accuracy, Scalability, Coverage: A Practical Configuration Verifier on a Global WAN. In SIGCOMM (SIGCOMM ’20). Association for Computing Machinery, New York, NY, USA. 599–614. https://doi.org/10.1145/3387514.3406217

Digital Library

[78]

Peng Zhang, Aaron Gember-Jacobson, Yueshang Zuo, Yuhao Huang, Xu Liu, and Hao Li. 2022. Differential Network Analysis. In NSDI. USENIX Association, Renton, WA, USA. 601–615. https://www.usenix.org/conference/nsdi22/presentation/zhang-peng

Cited By

Moeller MJacobs JBelanger ODarais DSchlesinger CSmolka SFoster NSilva A(2024)KATch: A Fast Symbolic Verifier for NetKATProceedings of the ACM on Programming Languages10.1145/36564548:PLDI(1905-1928)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656454
Thijm TBeckett RGupta AWalker D(2024)Kirigami, the Verifiable Art of Network CuttingIEEE/ACM Transactions on Networking10.1109/TNET.2024.336037132:3(2447-2462)Online publication date: Jun-2024
https://doi.org/10.1109/TNET.2024.3360371
Abdous SDiwangkara SGhorbani S(2024)Tempus: Probabilistic Network Latency VerificationIEEE Access10.1109/ACCESS.2024.349873712(169896-169909)Online publication date: 2024
https://doi.org/10.1109/ACCESS.2024.3498737
Show More Cited By

Index Terms

Modular Control Plane Verification via Temporal Invariants
1. Networks
  1. Network protocols
    1. Protocol correctness
      1. Formal specifications
      2. Protocol testing and verification
2. Theory of computation
  1. Logic
    1. Automated reasoning
    2. Verification by model checking

Recommendations

Procedure-modular verification of control flow safety properties
FTFJP '10: Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs

This paper describes a novel technique for fully automated procedure-modular verification of Java programs equipped with method-local and global assertions that specify safety properties of sequences of method invocations. Modularity of verification is ...
An automata-theoretic approach to modular model checking

In modular verification the specification of a module consists of two part. One part describes the guaranteed behavior of the module. The other part describes the assumed behavior of the system in which the module is interacting. This is called the ...
An Interface Theory for Program Verification
Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles
Abstract
Program verification is the problem, for a given program and a specification , of constructing a proof of correctness for the statement “program satisfies specification ” () or a proof of violation ([inline-graphic not available: see fulltext]). ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 7, Issue PLDI

June 2023

2020 pages

EISSN:2475-1421

DOI:10.1145/3554310

Editor:
Michael Hicks
Amazon, USA

Issue’s Table of Contents

Copyright © 2023 Owner/Author.

This work is licensed under a Creative Commons Attribution 4.0 International License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 06 June 2023

Published in PACMPL Volume 7, Issue PLDI

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

NSF (National Science Foundation)

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
465
Total Downloads

Downloads (Last 12 months)320
Downloads (Last 6 weeks)37

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Moeller MJacobs JBelanger ODarais DSchlesinger CSmolka SFoster NSilva A(2024)KATch: A Fast Symbolic Verifier for NetKATProceedings of the ACM on Programming Languages10.1145/36564548:PLDI(1905-1928)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656454
Thijm TBeckett RGupta AWalker D(2024)Kirigami, the Verifiable Art of Network CuttingIEEE/ACM Transactions on Networking10.1109/TNET.2024.336037132:3(2447-2462)Online publication date: Jun-2024
https://doi.org/10.1109/TNET.2024.3360371
Abdous SDiwangkara SGhorbani S(2024)Tempus: Probabilistic Network Latency VerificationIEEE Access10.1109/ACCESS.2024.349873712(169896-169909)Online publication date: 2024
https://doi.org/10.1109/ACCESS.2024.3498737
Cohen JAppel A(2023)Specifying and Verifying a Real-World Packet Error-Correction SystemVerified Software. Theories, Tools and Experiments10.1007/978-3-031-66064-1_4(44-63)Online publication date: 23-Oct-2023
https://dl.acm.org/doi/10.1007/978-3-031-66064-1_4

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents