Verifying pointer safety for programs with unknown calls
DOI10.1016/J.JSC.2010.06.003zbMATH Open1208.68149OpenAlexW2142567519MaRDI QIDQ604389FDOQ604389
Authors: Chenguang Luo, Florin Craciun, Shengchao Qin, Guanhua He, Wei-Ngan Chin 
Publication date: 10 November 2010
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jsc.2010.06.003
Recommendations
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- Automated verification of recursive programs with pointers
- Automated Verification of Shape and Size Properties Via Separation Logic
- Static Analysis
- Pointer logic for verification of pointer programs
Specification and verification (program logics, model checking, etc.) (68Q60) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)
Cites Work
- Separation and information hiding
- Automated Verification of Shape and Size Properties Via Separation Logic
- Programming Languages and Systems
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- Compositional shape analysis by means of bi-abduction
- Tools and Algorithms for the Construction and Analysis of Systems
- Scalable Shape Analysis for Systems Code
- Mining specifications
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- Guided Static Analysis
- Title not available (Why is that?)
- Modular specification of frame properties in JML
- Bottom-Up Shape Analysis
- Abductive analysis of modular logic programs
- Verifying pointer safety for programs with unknown calls
Cited In (8)
- Automated Verification of Shape and Size Properties Via Separation Logic
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- Verifying pointer safety for programs with unknown calls
- Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors
- Automatically proving termination and memory safety for programs with pointer arithmetic
- Languages and Compilers for Parallel Computing
- Per-dereference verification of temporal heap safety via adaptive context-sensitive analysis
- Automated inference of library specifications for source-sink property verification
Uses Software
This page was built for publication: Verifying pointer safety for programs with unknown calls
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q604389)
