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
- Abstractions from proofs
- Compositional shape analysis by means of bi-abduction
- Tools and Algorithms for the Construction and Analysis of Systems
- Scalable Shape Analysis for Systems Code
- Software model checking
- Title not available (Why is that?)
- Pick your contexts well, understanding object-sensitivity
- Title not available (Why is that?)
- Semi-sparse flow-sensitive pointer analysis
- Points-to analysis with efficient strong updates
- Learning minimal abstractions
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)
