Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors

DOI10.1007/978-3-540-69166-2_5MaRDI QIDQ3522062zbMATH OpenOpenAlexFDO

Authors Christopher L. Conway, Dennis Dams, Kedar S. Namjoshi, Clark Barrett

Publication date 28 August 2008

Published in Static Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-69166-2_5

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• On the non-approximability of points-to analysis
• A Systematic Approach to Probabilistic Pointer Analysis
• A formally-verified alias analysis
• scientific article; zbMATH DE number 1975596
• Verifying pointer safety for programs with unknown calls

Cited in

(12)

• On the non-approximability of points-to analysis
• Practical void safety
• Verifying pointer and string analyses with region type systems
• Predicate extension of symbolic memory graphs for the analysis of memory safety correctness
• New results on the computability and complexity of points-to analysis
• Partitioned memory models for program analysis
• Verifying pointer and string analyses with region type systems
• A Posteriori Soundness for Non-deterministic Abstract Interpretations
• Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction
• Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
• Mathematics of Program Construction
• Languages and Compilers for Parallel Computing

Describes a project that uses

Uses Software

• CCured
• SAFECode

This page was built for publication: Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors

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