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 logicpointer logicsoftware safety

Mathematics Subject Classification ID

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

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)

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

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)