DC Field | Value | Language |
---|---|---|
dc.contributor.author | Lee, O | ko |
dc.contributor.author | Yang, Hongseok | ko |
dc.contributor.author | Yi, KK | ko |
dc.date.accessioned | 2017-08-08T06:54:48Z | - |
dc.date.available | 2017-08-08T06:54:48Z | - |
dc.date.created | 2017-08-02 | - |
dc.date.created | 2017-08-02 | - |
dc.date.created | 2017-08-02 | - |
dc.date.issued | 2005 | - |
dc.identifier.citation | PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS, v.3444, pp.124 - 140 | - |
dc.identifier.issn | 0302-9743 | - |
dc.identifier.uri | http://hdl.handle.net/10203/225297 | - |
dc.description.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. | - |
dc.language | English | - |
dc.publisher | SPRINGER-VERLAG BERLIN | - |
dc.title | Automatic verification of pointer programs using grammar-based shape analysis | - |
dc.type | Article | - |
dc.identifier.wosid | 000229101800010 | - |
dc.identifier.scopusid | 2-s2.0-24644443912 | - |
dc.type.rims | ART | - |
dc.citation.volume | 3444 | - |
dc.citation.beginningpage | 124 | - |
dc.citation.endingpage | 140 | - |
dc.citation.publicationname | PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS | - |
dc.contributor.localauthor | Yang, Hongseok | - |
dc.contributor.nonIdAuthor | Lee, O | - |
dc.contributor.nonIdAuthor | Yi, KK | - |
dc.description.isOpenAccess | N | - |
dc.type.journalArticle | Article; Proceedings Paper | - |
dc.subject.keywordPlus | LOGIC | - |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.