Per-dereference verification of temporal heap safety via adaptive context-sensitive analysis
From MaRDI portal
Publication:6536280
DOI10.1007/978-3-030-32304-2_4zbMATH Open1539.68077MaRDI QIDQ6536280FDOQ6536280
Authors: Hua Yan, Shiping Chen, Yulei Sui, Yueqian Zhang, Changwei Zou, Jingling Xue
Publication date: 19 April 2024
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
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- 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)