Verifying pointer safety for programs with unknown calls

DOI10.1016/J.JSC.2010.06.003MaRDI QIDQ604389zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

verificationinferenceabductionseparation logic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

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

Cites work

• scientific article; zbMATH DE number 2161330 (Why is no real title available?)
• Abductive analysis of modular logic programs
• 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
• Bottom-Up Shape Analysis
• Compositional shape analysis by means of bi-abduction
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Guided Static Analysis
• Mining specifications
• Modular specification of frame properties in JML
• Programming Languages and Systems
• Scalable Shape Analysis for Systems Code
• Separation and information hiding
• Tools and Algorithms for the Construction and Analysis of Systems
• Verifying pointer safety for programs with unknown calls

Cited in

(8)

• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Languages and Compilers for Parallel Computing
• Automatically proving termination and memory safety for programs with pointer arithmetic
• Verifying pointer safety for programs with unknown calls
• Per-dereference verification of temporal heap safety via adaptive context-sensitive analysis
• Automated Verification of Shape and Size Properties Via Separation Logic
• Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors
• Automated inference of library specifications for source-sink property verification

Describes a project that uses

Uses Software

• HIP
• FreeRTOS

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)