Part of the book series:Lecture Notes in Computer Science ((LNPSE,volume 10548))
Included in the following conference series:
1407Accesses
Abstract
Acertifying algorithm verifies the correctness of its output at runtime by producing awitness in addition to an input-output pair. If awitness predicate holds for the triple, the input-output pair is correct. Achecker algorithm decides the witness predicate. While certifyingsequential algorithms are well-established, we considerdistributed algorithms. In this paper, we investigate certifying distributed algorithms that verify their distributed output. While the witness predicate states a property in the network, for distributed checking, additional predicates are decided for each component. We illustrate the applicability by examples.
This is a preview of subscription content,log in via an institution to check access.
Access this chapter
Subscribe and save
- Get 10 units per month
- Download Article/Chapter or eBook
- 1 Unit = 1 Article or 1 Chapter
- Cancel anytime
Buy Now
- Chapter
- JPY 3498
- Price includes VAT (Japan)
- eBook
- JPY 5719
- Price includes VAT (Japan)
- Softcover Book
- JPY 7149
- Price includes VAT (Japan)
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
For distributed algorithms, the global input is often the network itself.
References
Hallé, S.: When RV meets CEP. In: Falcone, Y., Sánchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 68–91. Springer, Cham (2016). doi:10.1007/978-3-319-46982-9_6
Korman, A., Kutten, S., Peleg, D.: Proof labeling schemes. Distrib. Comput.22(4), 215–233 (2010). doi:10.1007/s00446-010-0095-3
Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann Publishers Inc., San Francisco (1996)
McConnell, R.M., Mehlhorn, K., Näher, S., Schweitzer, P.: Certifying algorithms. Comput. Sci. Rev.5, 119–161 (2011)
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)
Raynal, M.: Distributed Algorithms for Message-Passing Systems. Springer, Heidelberg (2013)
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). doi:10.1007/978-3-319-57288-8_27
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). doi:10.1007/978-3-319-22969-0_14
Author information
Authors and Affiliations
Humboldt University of Berlin, Berlin, Germany
Kim Völlinger
- Kim Völlinger
You can also search for this author inPubMed Google Scholar
Corresponding author
Correspondence toKim Völlinger.
Editor information
Editors and Affiliations
Microsoft Research, Redmond, Washington, USA
Shuvendu Lahiri
The University of Manchester, Manchester, United Kingdom
Giles Reger
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Völlinger, K. (2017). Verifying the Output of a Distributed Algorithm Using Certification. In: Lahiri, S., Reger, G. (eds) Runtime Verification. RV 2017. Lecture Notes in Computer Science(), vol 10548. Springer, Cham. https://doi.org/10.1007/978-3-319-67531-2_29
Download citation
Published:
Publisher Name:Springer, Cham
Print ISBN:978-3-319-67530-5
Online ISBN:978-3-319-67531-2
eBook Packages:Computer ScienceComputer Science (R0)
Share this paper
Anyone you share the following link with will be able to read this content:
Sorry, a shareable link is not currently available for this article.
Provided by the Springer Nature SharedIt content-sharing initiative