Please use this identifier to cite or link to this item:
https://scholarbank.nus.edu.sg/handle/10635/41337
DC Field | Value | |
---|---|---|
dc.title | Automated verification of shape and size properties via separation logic | |
dc.contributor.author | Nguyen, H.H. | |
dc.contributor.author | David, C. | |
dc.contributor.author | Qin, S. | |
dc.contributor.author | Chin, W.-N. | |
dc.date.accessioned | 2013-07-04T08:25:09Z | |
dc.date.available | 2013-07-04T08:25:09Z | |
dc.date.issued | 2007 | |
dc.identifier.citation | Nguyen, H.H.,David, C.,Qin, S.,Chin, W.-N. (2007). Automated verification of shape and size properties via separation logic. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 4349 LNCS : 251-266. ScholarBank@NUS Repository. | |
dc.identifier.isbn | 3540697357 | |
dc.identifier.issn | 03029743 | |
dc.identifier.uri | http://scholarbank.nus.edu.sg/handle/10635/41337 | |
dc.description.abstract | 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. © Springer-Verlag Berlin Heidelberg 2007. | |
dc.source | Scopus | |
dc.type | Conference Paper | |
dc.contributor.department | COMPUTER SCIENCE | |
dc.description.sourcetitle | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | |
dc.description.volume | 4349 LNCS | |
dc.description.page | 251-266 | |
dc.identifier.isiut | NOT_IN_WOS | |
Appears in Collections: | Staff Publications |
Show simple item record
Files in This Item:
There are no files associated with this item.
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.