Full metadata record
DC Field | Value | Language |
---|---|---|
dc.contributor.author | 이욱세 | - |
dc.date.accessioned | 2019-09-09T05:35:11Z | - |
dc.date.available | 2019-09-09T05:35:11Z | - |
dc.date.issued | 2005-04 | - |
dc.identifier.citation | European Symposium on Programming; ESOP 2005: Programming Languages and Systems, Page. 124-140 | en_US |
dc.identifier.isbn | 978-3-540-25435-5 | - |
dc.identifier.uri | https://link.springer.com/chapter/10.1007/978-3-540-31987-0_10 | - |
dc.identifier.uri | https://repository.hanyang.ac.kr/handle/20.500.11754/110400 | - |
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. | en_US |
dc.language.iso | en_US | en_US |
dc.publisher | SPRINGER-VERLAG BERLIN | en_US |
dc.subject | Abstract State | en_US |
dc.subject | Abstract Domain | en_US |
dc.subject | Pointer Program | en_US |
dc.subject | Separation Logic | en_US |
dc.subject | Symbolic Location | en_US |
dc.title | Automatic Verification of Pointer Programs Using Grammar-Based Shape Analysis | en_US |
dc.type | Article | en_US |
dc.identifier.doi | 10.1007/978-3-540-31987-0_10 | - |
dc.relation.journal | LECTURE NOTES IN COMPUTER SCIENCE | - |
dc.contributor.googleauthor | Lee, Oukseh | - |
dc.contributor.googleauthor | Yang, Hongseok | - |
dc.contributor.googleauthor | Yi, Kwangkeun | - |
dc.relation.code | 2007206327 | - |
dc.sector.campus | E | - |
dc.sector.daehak | COLLEGE OF ENGINEERING SCIENCES[E] | - |
dc.sector.department | DEPARTMENT OF COMPUTER SCIENCE AND ENGINEERING | - |
dc.identifier.pid | oukseh | - |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.