Skip to main content
SpringerLink
Log in

On a Verification Framework for Certifying Distributed Algorithms: Distributed Checking and Consistency

  • Conference paper
  • First Online:
Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2018)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10854))

Abstract

A major problem in software engineering is assuring the correctness of a distributed system. A certifying distributed algorithm (CDA) computes for its input-output pair (i, o) an additional witness w – a formal argument for the correctness of (i, o). Each CDA features a witness predicate such that if the witness predicate holds for a triple (i, o, w), the input-output pair (i, o) is correct. An accompanying checker algorithm decides the witness predicate. Consequently, a user of a CDA does not have to trust the CDA but its checker algorithm. Usually, a checker is simpler and its verification is feasible. To sum up, the idea of a CDA is to adapt the underlying algorithm of a program at design-time such that it verifies its own output at runtime. While certifying sequential algorithms are well-established, there are open questions on how to apply certification to distributed algorithms. In this paper, we discuss distributed checking of a distributed witness; one challenge is that all parts of a distributed witness have to be consistent with each other. Furthermore, we present a method for formal instance verification (i.e. obtaining a machine-checked proof that a particular input-output pair is correct), and implement the method in a framework for the theorem prover Coq.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    https://github.com/voellinger/verified-certifying-distributed-algorithms/tree/master/Framework.

References

  1. Alkassar, E., Böhme, S., Mehlhorn, K., Rizkallah, C.: Verification of certifying computations. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 67–82. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_7

    Chapter  Google Scholar 

  2. Alkassar, E., Böhme, S., Mehlhorn, K., Rizkallah, C.: A framework for the verification of certifying computations. J. Autom. Reason. 52(3), 241–273 (2014)

    Article  MathSciNet  Google Scholar 

  3. Arkoudas, K., Rinard, M.C.: Deductive runtime certification. Electron. Notes Theor. Comput. Sci. 113, 45–63 (2005)

    Article  Google Scholar 

  4. Bruce, D., Hoàng, C.T., Sawada, J.: A certifying algorithm for 3-colorability of P\(^{5}\)-free graphs. In: Dong, Y., Du, D.-Z., Ibarra, O. (eds.) ISAAC 2009. LNCS, vol. 5878, pp. 594–604. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-10631-6_61

    Chapter  Google Scholar 

  5. Censor-Hillel, K., Fischer, E., Schwartzman, G., Vasudev, Y.: Fast distributed algorithms for testing graph properties. In: Gavoille, C., Ilcinkas, D. (eds.) DISC 2016. LNCS, vol. 9888, pp. 43–56. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-53426-7_4

    Chapter  MATH  Google Scholar 

  6. Corneil, D.G., Dalton, B., Habib, M.: LDFS-based certifying algorithm for the minimum path cover problem on cocomparability graphs. SIAM J. Comput. 42(3), 792–807 (2013)

    Article  MathSciNet  Google Scholar 

  7. Dolev, S.: Self-Stabilization. MIT Press, Cambridge (2000)

    MATH  Google Scholar 

  8. Duprat, J.: A Coq toolkit for graph theory. Rapport de recherche 15 (2001)

    Google Scholar 

  9. Finkler, U., Mehlhorn, K.: Checking priority queues. In: Proceedings of the Tenth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 1999, pp. 901–902. Society for Industrial and Applied Mathematics, Philadelphia (1999)

    Google Scholar 

  10. Glesner, S.: Program checking with certificates: separating correctness-critical code. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 758–777. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45236-2_41

    Chapter  Google Scholar 

  11. Heggernes, P., Kratsch, D.: Linear-time certifying recognition algorithms and forbidden induced subgraphs. Nord. J. Comput. 14(1), 87–108 (2007)

    MathSciNet  MATH  Google Scholar 

  12. Hell, P., Huang, J.: Certifying LexBFS recognition algorithms for proper interval graphs and proper interval bigraphs. SIAM J. Disc. Math. 18, 554–570 (2004)

    Article  MathSciNet  Google Scholar 

  13. Hung, R.W., Chang, M.S.: An efficient certifying algorithm for the Hamiltonian cycle problem on circular-arc graphs. Theoret. Comput. Sci. 412(39), 5351–5373 (2011)

    Article  MathSciNet  Google Scholar 

  14. INRIA: The Coq Proof Assistant. http://coq.inria.fr/

  15. Kaplan, H., Nussbaum, Y.: Certifying algorithms for recognizing proper circular-arc graphs and unit circular-arc graphs. Disc. Appl. Math. 157(15), 3216–3230 (2009)

    Article  MathSciNet  Google Scholar 

  16. Korman, A., Kutten, S., Peleg, D.: Proof labeling schemes. Distrib. Comput. 22(4), 215–233 (2010)

    Article  Google Scholar 

  17. Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann Publishers Inc., San Francisco (1996)

    MATH  Google Scholar 

  18. McConnell, R.M.: A certifying algorithm for the consecutive-ones property. In: Proceedings of the Fifteenth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2004, pp. 768–777. Society for Industrial and Applied Mathematics, Philadelphia (2004)

    Google Scholar 

  19. McConnell, R.M., Mehlhorn, K., Näher, S., Schweitzer, P.: Certifying algorithms. Comput. Sci. Rev. 5, 119–161 (2011)

    Article  Google Scholar 

  20. Mehlhorn, K., Näher, S.: From algorithms to working programs: on the use of program checking in LEDA. In: Brim, L., Gruska, J., Zlatuška, J. (eds.) MFCS 1998. LNCS, vol. 1450, pp. 84–93. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0055759

    Chapter  Google Scholar 

  21. Mostafa, M., Bonakdarpour, B.: Decentralized runtime verification of LTL specifications in distributed systems. In: Proceedings of the 2015 IEEE International Parallel and Distributed Processing Symposium, IPDPS 2015, pp. 494–503. IEEE Computer Society, Washington, DC (2015)

    Google Scholar 

  22. Necula, G.C., Lee, P.: The Design and implementation of a certifying compiler. In: Proceedings of the ACM SIGPLAN 1998 Conference on Programming Language Design and Implementation, PLDI 1998, pp. 333–344. ACM, New York (1998)

    Google Scholar 

  23. Nikolopoulos, S.D., Palios, L.: An O(nm)-time certifying algorithm for recognizing HHD-free graphs. Theor. Comput. Sci. 452, 117–131 (2012)

    Article  MathSciNet  Google Scholar 

  24. Noschinski, L., Rizkallah, C., Mehlhorn, K.: Verification of certifying computations through autocorres and simpl. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 46–61. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-06200-6_4

    Chapter  Google Scholar 

  25. Raynal, M.: Distributed Algorithms for Message-Passing Systems. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38123-2

    Book  MATH  Google Scholar 

  26. Rizkallah, C.: Verification of program computations. Ph.D. thesis (2015)

    Google Scholar 

  27. Schmidt, J.M.: Construction sequences and certifying 3-connectivity. Algorithmica 62, 192–208 (2012)

    Article  MathSciNet  Google Scholar 

  28. Völlinger, K.: Verifying the output of a distributed algorithm using certification. In: Lahiri, S., Reger, G. (eds.) RV 2017. LNCS, vol. 10548, pp. 424–430. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67531-2_29

    Chapter  Google Scholar 

  29. Völlinger, K., Akili, S.: Verifying a class of certifying distributed programs. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 373–388. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57288-8_27

    Chapter  Google Scholar 

  30. Völlinger, K., Reisig, W.: Certification of distributed algorithms solving problems with optimal substructure. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 190–195. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-22969-0_14

    Chapter  Google Scholar 

  31. Wilcox, J.R., Woos, D., Panchekha, P., Tatlock, Z., Wang, X., Ernst, M.D., Anderson, T.: Verdi: a framework for implementing and formally verifying distributed systems. In: ACM SIGPLAN Notices, vol. 50, pp. 357–368. ACM (2015)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Humboldt University of Berlin, Berlin, Germany

    Kim Völlinger & Samira Akili

Authors
  1. Kim Völlinger
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Samira Akili
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Kim Völlinger .

Editor information

Editors and Affiliations

  1. Technische Universität Dresden, Dresden, Germany

    Christel Baier

  2. Departamento de Informática, Universidade Nova de Lisboa, Caparica, Portugal

    Luís Caires

Rights and permissions

Reprints and permissions

Copyright information

© 2018 IFIP International Federation for Information Processing

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Völlinger, K., Akili, S. (2018). On a Verification Framework for Certifying Distributed Algorithms: Distributed Checking and Consistency. In: Baier, C., Caires, L. (eds) Formal Techniques for Distributed Objects, Components, and Systems. FORTE 2018. Lecture Notes in Computer Science(), vol 10854. Springer, Cham. https://doi.org/10.1007/978-3-319-92612-4_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-92612-4_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-92611-7

  • Online ISBN: 978-3-319-92612-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Societies and partnerships

Search

Navigation