Please use this identifier to cite or link to this item:
https://doi.org/10.1007/978-3-540-70545-1_34
DC Field | Value | |
---|---|---|
dc.title | Enhancing program verification with lemmas | |
dc.contributor.author | Nguyen, H.H. | |
dc.contributor.author | Chin, W.-N. | |
dc.date.accessioned | 2013-07-04T08:40:39Z | |
dc.date.available | 2013-07-04T08:40:39Z | |
dc.date.issued | 2008 | |
dc.identifier.citation | Nguyen, H.H.,Chin, W.-N. (2008). Enhancing program verification with lemmas. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 5123 LNCS : 355-369. ScholarBank@NUS Repository. <a href="https://doi.org/10.1007/978-3-540-70545-1_34" target="_blank">https://doi.org/10.1007/978-3-540-70545-1_34</a> | |
dc.identifier.isbn | 3540705430 | |
dc.identifier.issn | 03029743 | |
dc.identifier.uri | http://scholarbank.nus.edu.sg/handle/10635/41990 | |
dc.description.abstract | One promising approach to verifying heap-manipulating programs is based on user-defined inductive predicates in separation logic. This approach can describe data structures with complex invariants and sound reasoning based on unfold/fold. However, an important component towards more expressive program verification is the use of lemmas that can soundly relate predicates beyond their original definitions. This paper outlines a new automatic mechanism for proving and applying user-specified lemmas under separation logic. © 2008 Springer-Verlag. | |
dc.description.uri | http://libproxy1.nus.edu.sg/login?url=http://dx.doi.org/10.1007/978-3-540-70545-1_34 | |
dc.source | Scopus | |
dc.subject | Entailment | |
dc.subject | Lemma Application | |
dc.subject | Lemma Proving | |
dc.subject | Program Verification | |
dc.subject | Separation Logic | |
dc.type | Conference Paper | |
dc.contributor.department | COMPUTER SCIENCE | |
dc.description.doi | 10.1007/978-3-540-70545-1_34 | |
dc.description.sourcetitle | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | |
dc.description.volume | 5123 LNCS | |
dc.description.page | 355-369 | |
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.