Automated Verification of Shape and Size
Despite their popularity and importance, pointer based programs remain a major challenge for program verification. In this paper, we propose an automated verification system that is concise, precise and expressive for ensuring the safety of pointer-based programs. Our approach uses user-definable sh...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
2007
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/1721.1/35709 |
| _version_ | 1826205864683372544 |
|---|---|
| author | Nguyen, Huu Hai David, Cristina Qin, Shengchao Chin, Wei Ngan |
| author_facet | Nguyen, Huu Hai David, Cristina Qin, Shengchao Chin, Wei Ngan |
| author_sort | Nguyen, Huu Hai |
| collection | MIT |
| description | Despite their popularity and importance, pointer based programs remain a major challenge for program verification. In this paper, we propose an automated verification system that is concise, precise and expressive for ensuring the safety of pointer-based programs. Our approach uses user-definable shape predicates to allow programmers to describe a wide range of data structures with their associated size properties. To support automatic verification, we design a new entailment checking procedure that can handle well-founded inductive predicates using unfold/fold reasoning. We have proven the soundness and termination of our verification system, and have built a prototype system. |
| first_indexed | 2024-09-23T13:20:20Z |
| format | Article |
| id | mit-1721.1/35709 |
| institution | Massachusetts Institute of Technology |
| language | English |
| last_indexed | 2024-09-23T13:20:20Z |
| publishDate | 2007 |
| record_format | dspace |
| spelling | mit-1721.1/357092019-04-12T08:35:03Z Automated Verification of Shape and Size Nguyen, Huu Hai David, Cristina Qin, Shengchao Chin, Wei Ngan Verification Separation Logic Despite their popularity and importance, pointer based programs remain a major challenge for program verification. In this paper, we propose an automated verification system that is concise, precise and expressive for ensuring the safety of pointer-based programs. Our approach uses user-definable shape predicates to allow programmers to describe a wide range of data structures with their associated size properties. To support automatic verification, we design a new entailment checking procedure that can handle well-founded inductive predicates using unfold/fold reasoning. We have proven the soundness and termination of our verification system, and have built a prototype system. Singapore-MIT Alliance (SMA) 2007-01-11T19:23:42Z 2007-01-11T19:23:42Z 2007-01 Article http://hdl.handle.net/1721.1/35709 en Computer Science (CS) 162917 bytes application/pdf application/pdf |
| spellingShingle | Verification Separation Logic Nguyen, Huu Hai David, Cristina Qin, Shengchao Chin, Wei Ngan Automated Verification of Shape and Size |
| title | Automated Verification of Shape and Size |
| title_full | Automated Verification of Shape and Size |
| title_fullStr | Automated Verification of Shape and Size |
| title_full_unstemmed | Automated Verification of Shape and Size |
| title_short | Automated Verification of Shape and Size |
| title_sort | automated verification of shape and size |
| topic | Verification Separation Logic |
| url | http://hdl.handle.net/1721.1/35709 |
| work_keys_str_mv | AT nguyenhuuhai automatedverificationofshapeandsize AT davidcristina automatedverificationofshapeandsize AT qinshengchao automatedverificationofshapeandsize AT chinweingan automatedverificationofshapeandsize |