Per-dereference verification of temporal heap safety via adaptive context-sensitive analysis

<a class="pub-badge pub-badge--doi" href="https://doi.org/10.1007/978-3-030-32304-2_4" rel="nofollow">DOI 10.1007/978-3-030-32304-2_4</a><a class="pub-badge pub-badge--grey" href="https://zbmath.org/1539.68077" rel="nofollow">zbMATH</a><a class="pub-badge pub-badge--mardi" href="https://portal.mardi4nfdi.de/wiki/Item:Q6536280" rel="nofollow">MaRDI QID Q6536280</a><a class="pub-badge pub-badge--grey" href="https://fdo.portal.mardi4nfdi.de/fdo/Q6536280" rel="nofollow">FDO</a>

Authors Hua Yan, Shiping Chen, Yulei Sui, Yueqian Zhang, Changwei Zou, Jingling Xue

Publication date 19 April 2024

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

• Establishing local temporal heap safety properties with applications to compile-time memory management
• scientific article; zbMATH DE number 2090863
• Verifying pointer safety for programs with unknown calls
• Automatically verifying temporal properties of pointer programs with cyclic proof
• Automatically verifying temporal properties of pointer programs with cyclic proof

Cites work

• scientific article; zbMATH DE number 2087445 (Why is no real title available?)
• scientific article; zbMATH DE number 1903378 (Why is no real title available?)
• Abstractions from proofs
• Compositional shape analysis by means of bi-abduction
• Learning minimal abstractions
• Pick your contexts well, understanding object-sensitivity
• Points-to analysis with efficient strong updates
• Scalable Shape Analysis for Systems Code
• Semi-sparse flow-sensitive pointer analysis
• Software model checking
• Tools and Algorithms for the Construction and Analysis of Systems

This page was built for publication: Per-dereference verification of temporal heap safety via adaptive context-sensitive analysis

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