Verifying pointer safety for programs with unknown calls

DOI10.1016/j.jsc.2010.06.003zbMath1208.68149OpenAlexW2142567519MaRDI QIDQ604389

Guanhua He, Shengchao Qin, Chenguang Luo, Wei-Ngan Chin, Florin Craciun

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

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

Related Items (1)

Verifying pointer safety for programs with unknown calls

Uses Software

• HIP
• FreeRTOS

Cites Work

• Unnamed Item
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Verifying pointer safety for programs with unknown calls
• Bottom-Up Shape Analysis
• Separation and information hiding
• Scalable Shape Analysis for Systems Code
• Guided Static Analysis
• Abductive analysis of modular logic programs
• Modular specification of frame properties in JML
• Mining specifications
• Compositional shape analysis by means of bi-abduction
• Automated Verification of Shape and Size Properties Via Separation Logic
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Programming Languages and Systems
• Tools and Algorithms for the Construction and Analysis of Systems

This page was built for publication: Verifying pointer safety for programs with unknown calls