Verification of the Schorr-Waite algorithm -- from trees to graphs

DOI10.1007/978-3-642-20551-4_5MaRDI QIDQ3003486zbMATH OpenOpenAlexFDO

Authors Mathieu Giorgino, Martin Strecker, Ralph Matthes, Marc Pantel

Publication date 27 May 2011

Published in Logic-Based Program Synthesis and Transformation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-20551-4_5

zbMATH Keywords

pointer algorithmsprogram refinementverification of imperative programs

Mathematics Subject Classification ID

Graph algorithms (graph-theoretic aspects) (05C85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm
• Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction
• Proving pointer programs in higher-order logic
• Proving pointer programs in higher-order logic.
• Verified efficient implementation of Gabow's strongly connected component algorithm

Cites work

• An efficient machine-independent procedure for garbage collection in various list structures
• Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction
• Experience report: seL4, formally verifying a high-performance microkernel
• scientific article; zbMATH DE number 1612488 (Why is no real title available?)
• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• Imperative Functional Programming with Isabelle/HOL
• Isabelle/HOL. A proof assistant for higher-order logic
• Proving pointer programs in higher-order logic
• The Zipper
• Verification of the Schorr-Waite algorithm -- from trees to graphs

Cited in

(5)

• Verified efficient implementation of Gabow's strongly connected component algorithm
• Verification of the Schorr-Waite algorithm -- from trees to graphs
• A machine-checked framework for relational separation logic
• Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm
• Reasoning about memory layouts

Describes a project that uses

Uses Software

• Why3
• KRAKATOA
• Caduceus
• Haskabelle
• Isabelle/HOL

This page was built for publication: Verification of the Schorr-Waite algorithm -- from trees to graphs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3003486)