검색 상세

ProverPSL: A Theorem Prover for Full Separation Logic

ProverPSL: 분리 논리 정리 증명기

DinhHoangMai (딘황마이)

원문보기

  • 발행기관 Pohang University of Science and Technology
  • 지도교수Park Sungwoo
  • 발행년도2016
  • 학위수여년월2016. 2
  • 학위명석사
  • 학과 및 전공일반대학원 컴퓨터공학과
  • 원문페이지52
  • 본문언어영어
  • 저작권포항공과대학교 논문은 저작권에 의해 보호받습니다.
초록 moremore
This report presents a theorem prover for automated verification of program specifications written in separation logic. Our prover supports all new connectives in separation logic including separating conjunction and separating implication. To assist the prover, we integrate a high efficient SMT solver to process arithmetic expression relations, and also present a method to apply inference rules with associativity property.
This report presents a theorem prover for automated verification of program specifications written in separation logic. Our prover supports all new connectives in separation logic including separating conjunction and separating implication. To assist the prover, we integrate a high efficient SMT solver to process arithmetic expression relations, and also present a method to apply inference rules with associativity property.
목차 moremore
I Introduction 1
II Preliminaries 4
2.1 Separation Logic 4
...
I Introduction 1
II Preliminaries 4
2.1 Separation Logic 4
2.2 PSL Proof System 7
2.2.1 Syntax 7
2.2.2 World Sequents 8
2.2.3 Inference Rules 10
III ProverPSL 11
3.1 Overall Method and Challenges 11
3.2 Rule Category 13
3.3 Proof Search Strategy 14
3.4 Rule Application 19
3.4.1 Standard Rules 19
3.4.2 Atomic Rules 19
3.4.3 Contradiction Rules 21
3.4.4 Expanded Rules 22
IV Implementation 29
V Conclusion 33
5.1 Summary 33
5.2 Discussion 34