Verification of the Schorr-Waite Algorithm – From Trees to Graphs

DOI10.1007/978-3-642-20551-4_5zbMath1326.68095OpenAlexW1546264185MaRDI QIDQ3003486

Ralph Matthes, Mathieu Giorgino, Marc Pantel, Martin Strecker

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

program refinementpointer algorithmsverification of imperative programs

Mathematics Subject Classification ID

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

Related Items (3)

Reasoning about memory layouts ⋮ Verification of the Schorr-Waite Algorithm – From Trees to Graphs ⋮ A Machine-Checked Framework for Relational Separation Logic

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Isabelle/HOL. A proof assistant for higher-order logic
• Proving pointer programs in higher-order logic
• Experience report
• Verification of the Schorr-Waite Algorithm – From Trees to Graphs
• Imperative Functional Programming with Isabelle/HOL
• The Zipper
• Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction
• An efficient machine-independent procedure for garbage collection in various list structures

This page was built for publication: Verification of the Schorr-Waite Algorithm – From Trees to Graphs