Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction

DOI10.1007/978-3-642-32759-9_18MaRDI QIDQ4647844zbMATH OpenOpenAlexFDO

Authors Mathieu Giorgino, Martin Strecker

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

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

Recommendations

• Pointer logic for verification of pointer programs
• Computer Science Logic
• Completeness and expressiveness of pointer program verification by separation logic
• Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors
• Automated verification of recursive programs with pointers
• scientific article; zbMATH DE number 1487480
• Exploiting pointer analysis in memory models for deductive verification

Cited in

(6)

• scientific article; zbMATH DE number 2086515 (Why is no real title available?)
• scientific article; zbMATH DE number 2084334 (Why is no real title available?)
• Implementing and reasoning about hash-consed data structures in Coq
• Bddl: A Type System for Binary Decision Diagrams
• Modeling and verifying graph transformations in proof assistants
• Verification of the Schorr-Waite algorithm -- from trees to graphs

Describes a project that uses

Uses Software

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

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

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