Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction
DOI10.1007/978-3-642-32759-9_18zbMATH Open1372.68062OpenAlexW2404373436MaRDI QIDQ4647844FDOQ4647844
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
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
binary decision diagrampointer algorithmsmodular program developmentverification of imperative algorithms
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)
Cited In (6)
- Title not available (Why is that?)
- Title not available (Why is that?)
- 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
Uses Software
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)