Abstract
We report a case study in automated incremental assertionbased proof checking with PVS. Given an annotated distributed algorithm, our tool ProPar generates the proof obligations for partial correctness, plus a proof script per obligation. ProPar then lets PVS attempt to discharge all obligations by running the proof scripts. The Chang-Roberts algorithm elects a leader on a unidirectional ring with unique identities. With ProPar, we check its correctness with a very high degree of automation: over 90% of the proof obligations is discharged automatically. This case study underlines the feasibility of the approach and is, to the best of our knowledge, the first verification of the Chang-Roberts algorithm for arbitrary ring size in a proof checker. © Springer-Verlag Berlin Heidelberg 2007.
Cite
CITATION STYLE
Romijn, J., Wesselink, W., & Mooij, A. (2007). Assertion-based proof checking of chang-roberts leader election in PVS. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4762 LNCS, pp. 347–361). Springer Verlag. https://doi.org/10.1007/978-3-540-75596-8_25
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
