Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction

DOI10.1007/978-3-642-32759-9_18zbMath1372.68062OpenAlexW2404373436MaRDI QIDQ4647844

Martin Strecker, Mathieu Giorgino

Publication date: 8 November 2012

Published in: FM 2012: Formal Methods (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-32759-9_18

zbMATH Keywords

binary decision diagrampointer algorithmsmodular program developmentverification of imperative algorithms

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (3)

Verification of the Schorr-Waite Algorithm – From Trees to Graphs ⋮ Modeling and Verifying Graph Transformations in Proof Assistants ⋮ Implementing and reasoning about hash-consed data structures in Coq

Uses Software

• Coq
• HOL-Boogie
• Isabelle/HOL
• Isabelle/Isar
• Why3
• VCC

This page was built for publication: Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction