Pointer logic for verification of pointer programs

DOI10.3724/SP.J.1001.2010.03620MaRDI QIDQ3071444zbMATH OpenOpenAlexFDO

Authors Zhao-Peng Li, Zhifang Wang, Baojian Hua, Yi-Yun Chen

Publication date 5 February 2011

Published in Journal of Software (Search for Journal in Brave)

Full work available at URL https://doi.org/10.3724/sp.j.1001.2010.03620

zbMATH Keywords

Hoare logicsoftware safetypointer logic

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Recommendations

• Proving pointer programs in higher-order logic.
• Proving pointer programs in higher-order logic
• scientific article; zbMATH DE number 1612488
• Scope Logic: An Extension to Hoare Logic for Pointers and Recursive Data Structures
• Programming Languages and Systems

Cited in

(23)

• Proving pointer programs in higher-order logic.
• scientific article; zbMATH DE number 2084334 (Why is no real title available?)
• Abstraction of object graphs in program verification
• scientific article; zbMATH DE number 1956491 (Why is no real title available?)
• Computer Science Logic
• Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
• Verifying pointer and string analyses with region type systems
• Calculating with pointers
• Verifying pointer safety for programs with unknown calls
• Time bounds for general function pointers
• scientific article; zbMATH DE number 1612488 (Why is no real title available?)
• A shape graph logic and a shape system
• Automatically proving termination and memory safety for programs with pointer arithmetic
• Reasoning About Sequences of Memory States
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Safe Modification of Pointer Programs in Refinement Calculus
• Exploiting pointer analysis in memory models for deductive verification
• Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction
• Static Analysis
• Proving pointer programs in higher-order logic
• Compositional Reasoning for Pointer Structures
• Programming Languages and Systems
• Programming Languages and Systems

This page was built for publication: Pointer logic for verification of pointer programs

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