Boolean BI 논리를 위한 정리 증명기
- Title
- Boolean BI 논리를 위한 정리 증명기
- Authors
- 박종현
- Date Issued
- 2013
- Publisher
- 포항공과대학교
- 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 ofseparation logic that excludes separating implication. As the first step towards a verification tool using full separation logic, we develop a nested sequent calculusfor 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 sequentcalculus is that its sequent may have not only smaller child sequents but also multiple parent sequents, thus producing a graph structure of sequents instead ofa 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.
- URI
- http://postech.dcollection.net/jsp/common/DcLoOrgPer.jsp?sItemId=000001560718
https://oasis.postech.ac.kr/handle/2014.oak/1856
- Article Type
- Thesis
- 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.