A relational approach to interprocedural shape analysis
Abstract
This article addresses the verification of properties of imperative programs with recursive procedure calls, heap-allocated storage, and destructive updating of pointer-valued fields, that is, interprocedural shape analysis . The article makes three contributions.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jan 01, 2010
- Source ID
- 10.1145/1667048.1667050
Entities
People
- Alexey Loginov
- Bertrand Jeannet
- Mooly Sagiv
- Thomas Reps
Organizations
- Division of Computing and Communication Foundations
- GrammaTech
- Institut National de Recherche en Informatique et en Automatique
- National Science Foundation
- Office of Naval Research
- Tel Aviv University
- University of Wisconsin–Madison