Automatic Verification of Pointer Programs Using Grammar-Based Shape Analysis
- Title
- Automatic Verification of Pointer Programs Using Grammar-Based Shape Analysis
- Author
- 이욱세
- Keywords
- Abstract State; Abstract Domain; Pointer Program; Separation Logic; Symbolic Location
- Issue Date
- 2005-04
- Publisher
- SPRINGER-VERLAG BERLIN
- Citation
- European Symposium on Programming; ESOP 2005: Programming Languages and Systems, Page. 124-140
- Abstract
- We present a program analysis that can automatically discover the shape of complex pointer data structures. The discovered invariants are, then, used to verify the absence of safety errors in the program, or to check whether the program preserves the data consistency. Our analysis extends the shape analysis of Sagiv et al. with grammar annotations, which can precisely express the shape of complex data structures. We demonstrate the usefulness of our analysis with binomial heap construction and the Schorr-Waite tree traversal. For a binomial heap construction algorithm, our analysis returns a grammar that precisely describes the shape of a binomial heap; for the Schorr-Waite tree traversal, our analysis shows that at the end of the execution, the result is a tree and there are no memory leaks.
- URI
- https://link.springer.com/chapter/10.1007/978-3-540-31987-0_10https://repository.hanyang.ac.kr/handle/20.500.11754/110400
- ISBN
- 978-3-540-25435-5
- DOI
- 10.1007/978-3-540-31987-0_10
- Appears in Collections:
- COLLEGE OF ENGINEERING SCIENCES[E](공학대학) > COMPUTER SCIENCE AND ENGINEERING(컴퓨터공학과) > Articles
- Files in This Item:
There are no files associated with this item.
- Export
- RIS (EndNote)
- XLS (Excel)
- XML