×

Verification of the Schorr-Waite algorithm – from trees to graphs. (English) Zbl 1326.68095

Alpuente, María (ed.), Logic-based program synthesis and transformation. 20th international symposium, LOPSTR 2010, Hagenberg, Austria, July 23–25, 2010. Revised selected papers. Berlin: Springer (ISBN 978-3-642-20550-7/pbk). Lecture Notes in Computer Science 6564, 67-83 (2011).
Summary: This article proposes a method for proving the correctness of graph algorithms by manipulating their spanning trees enriched with additional references. We illustrate this concept with a proof of the correctness of a (pseudo-)imperative version of the Schorr-Waite algorithm by refinement of a functional one working on trees. It is composed of two orthogonal steps of refinement – functional to imperative and tree to graph – finally merged to obtain the result. Our imperative specifications use monadic constructs and syntax sugar, making them close to common imperative languages. This work has been realized within the Isabelle/HOL proof assistant.
For the entire collection see [Zbl 1214.68005].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
05C85 Graph algorithms (graph-theoretic aspects)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI HAL

References:

[1] Abrial, J.-R.: Event based sequential program development: Application to constructing a pointer program. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 51–74. Springer, Heidelberg (2003) · doi:10.1007/978-3-540-45236-2_5
[2] Bornat, R.: Proving pointer programs in Hoare logic. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 102–126. Springer, Heidelberg (2000) · Zbl 0963.68036 · doi:10.1007/10722010_8
[3] Bubel, R.: The schorr-waite-algorithm. In: Beckert, B., Hähnle, R., Schmitt, P.H. (eds.) Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334, pp. 569–587. Springer, Heidelberg (2007) · doi:10.1007/978-3-540-69061-0_15
[4] Bulwahn, L., Krauss, A., Haftmann, F., Erkök, L., Matthews, J.: Imperative functional programming with isabelle/HOL. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 134–149. Springer, Heidelberg (2008) · Zbl 1165.68352 · doi:10.1007/978-3-540-71067-7_14
[5] Filliâtre, J.-C., Marché, C.: The why/Krakatoa/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173–177. Springer, Heidelberg (2007) · Zbl 05216226 · doi:10.1007/978-3-540-73368-3_21
[6] Giorgino, M., Strecker, M.: Verification of BDD algorithms by refinement of trees. Technical report, IRIT (2010), http://www.irit.fr/ Mathieu.Giorgino/Publications/GiSt2010BDD.html · Zbl 1372.68062
[7] Giorgino, M., Strecker, M., Matthes, R., Pantel, M.: Verification of the Schorr-Waite algorithm - From trees to graphs (January 2010), http://www.irit.fr/ Mathieu.Giorgino/Publications/SchorrWaite_TreesGraphs.html · Zbl 1326.68095
[8] Hubert, T., Marché, C.: A case study of C source code verification: the Schorr-Waite algorithm. In: Software Engineering and Formal Methods (SEFM). IEEE Computer Society, Los Alamitos (2005)
[9] Huet, G.: Functional pearl: The zipper. Journal of Functional Programming 7(5), 549–554 (1997) · Zbl 0893.68014 · doi:10.1017/S0956796897002864
[10] Klein, G., Derrin, P., Elphinstone, K.: Experience report: sel4 – formally verifying a high-performance microkernel. In: International Conference on Functional Programming (ICFP). ACM, New York (2009) · Zbl 1302.68090
[11] Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. Information and Computation 199, 200–227 (2005) · Zbl 1081.68008 · doi:10.1016/j.ic.2004.10.007
[12] Nipkow, T., Paulson, L., Wenzel, M.: Isabelle/HOL. A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002) · Zbl 0994.68131 · doi:10.1007/3-540-45949-9
[13] O’Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001) · Zbl 0999.68045 · doi:10.1007/3-540-44802-0_1
[14] Rittweiler, T., Haftmann, F.: Haskabelle – converting Haskell source files to Isabelle/HOL theories (2009), http://www.cl.cam.ac.uk/research/hvg/Isabelle/haskabelle.html
[15] Schirmer, N., Wenzel, M.: State spaces – the locale way. ENTCS 254, 161–179 (2009)
[16] Schorr, H., Waite, W.: An efficient machine independent procedure for garbage collection in various list structures. Communications of the ACM 10, 501–506 (1967) · Zbl 0149.12608 · doi:10.1145/363534.363554
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.