DC Field | Value | Language |
---|---|---|
dc.contributor.author | Park, J | - |
dc.contributor.author | Seo, J | - |
dc.contributor.author | Park, S | - |
dc.date.accessioned | 2016-03-31T08:45:00Z | - |
dc.date.available | 2016-03-31T08:45:00Z | - |
dc.date.created | 2013-03-05 | - |
dc.date.issued | 2013-01 | - |
dc.identifier.issn | 1523-2867 | - |
dc.identifier.other | 2013-OAK-0000026726 | - |
dc.identifier.uri | https://oasis.postech.ac.kr/handle/2014.oak/15965 | - |
dc.description.abstract | While separation logic is acknowledged as an enabling technology for large-scale program verification, most of the existing verification tools use only a fragment of separation logic that excludes separating implication. As the first step towards a verification tool using full separation logic, we develop a nested sequent calculus for Boolean BI (Bunched Implications), the underlying theory of separation logic, as well as a theorem prover based on it. A salient feature of our nested sequent calculus is that its sequent may have not only smaller child sequents but also multiple parent sequents, thus producing a graph structure of sequents instead of a tree structure. Our theorem prover is based on backward search in a refinement of the nested sequent calculus in which weakening and contraction are built into all the inference rules. We explain the details of designing our theorem prover and provide empirical evidence of its practicality. | - |
dc.description.statementofresponsibility | X | - |
dc.language | English | - |
dc.publisher | ACM | - |
dc.relation.isPartOf | ACM SIGPLAN NOTICES | - |
dc.subject | Verification | - |
dc.subject | Separation logic | - |
dc.subject | Boolean BI | - |
dc.subject | Theorem prover | - |
dc.subject | Nested sequent calculus | - |
dc.subject | MUTABLE DATA-STRUCTURES | - |
dc.subject | SEPARATION LOGIC | - |
dc.subject | SHAPE-ANALYSIS | - |
dc.subject | VERIFICATION | - |
dc.subject | TABLEAUX | - |
dc.title | A Theorem Prover for Boolean BI | - |
dc.type | Article | - |
dc.contributor.college | 컴퓨터공학과 | - |
dc.identifier.doi | 10.1145/2429069.2429095 | - |
dc.author.google | Park J., Seo J., Park S. | - |
dc.relation.startpage | 219 | - |
dc.relation.lastpage | 231 | - |
dc.contributor.id | 10165554 | - |
dc.relation.journal | ACM SIGPLAN NOTICES | - |
dc.relation.index | SCI급, SCOPUS 등재논문 | - |
dc.relation.sci | SCI | - |
dc.collections.name | Conference Papers | - |
dc.type.rims | ART | - |
dc.identifier.bibliographicCitation | ACM SIGPLAN NOTICES, v.48, no.1, pp.219 - 231 | - |
dc.identifier.wosid | 000318629900019 | - |
dc.date.tcdate | 2019-01-01 | - |
dc.citation.endPage | 231 | - |
dc.citation.number | 1 | - |
dc.citation.startPage | 219 | - |
dc.citation.title | ACM SIGPLAN NOTICES | - |
dc.citation.volume | 48 | - |
dc.contributor.affiliatedAuthor | Park, S | - |
dc.identifier.scopusid | 2-s2.0-84874173271 | - |
dc.description.journalClass | 1 | - |
dc.description.journalClass | 1 | - |
dc.description.wostc | 5 | - |
dc.description.scptc | 13 | * |
dc.date.scptcdate | 2018-05-121 | * |
dc.type.docType | Article; Proceedings Paper | - |
dc.subject.keywordPlus | SHAPE-ANALYSIS | - |
dc.subject.keywordPlus | SEPARATION | - |
dc.subject.keywordPlus | VERIFICATION | - |
dc.subject.keywordAuthor | Verification | - |
dc.subject.keywordAuthor | Separation logic | - |
dc.subject.keywordAuthor | Boolean BI | - |
dc.subject.keywordAuthor | Theorem prover | - |
dc.subject.keywordAuthor | Nested sequent calculus | - |
dc.relation.journalWebOfScienceCategory | Computer Science, Software Engineering | - |
dc.description.journalRegisteredClass | scie | - |
dc.description.journalRegisteredClass | scopus | - |
dc.relation.journalResearchArea | Computer Science | - |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.
library@postech.ac.kr Tel: 054-279-2548
Copyrights © by 2017 Pohang University of Science ad Technology All right reserved.