서브메뉴
검색
Rely-Guarantee Semantics for Separation-Logic-Based Specification Extraction
Rely-Guarantee Semantics for Separation-Logic-Based Specification Extraction
상세정보
- 자료유형
- 학위논문 서양
- 최종처리일시
- 20250211152031
- ISBN
- 9798384023357
- DDC
- 004
- 저자명
- He, Paul.
- 서명/저자
- Rely-Guarantee Semantics for Separation-Logic-Based Specification Extraction
- 발행사항
- [Sl] : University of Pennsylvania, 2024
- 발행사항
- Ann Arbor : ProQuest Dissertations & Theses, 2024
- 형태사항
- 151 p
- 주기사항
- Source: Dissertations Abstracts International, Volume: 86-02, Section: A.
- 주기사항
- Advisor: Zdancewic, Steve.
- 학위논문주기
- Thesis (Ph.D.)--University of Pennsylvania, 2024.
- 초록/해제
- 요약While formal verification promises correctness guarantees about software, these guarantees themselves must be verified. This dissertation focuses on the soundness of the Heapster verification tool, which converts imperative programs into functional specifications. Heapster is able to do this by using a type system based on separation logic to guarantee memory safety, ensuring that pointer operations can be erased in the functional program. We prove the soundness of this type system using a novel concept called rely-guarantee permissions as the semantics of types. These rely-guarantee permissions are derived from rely-guarantee reasoning, a technique for reasoning about concurrent code. We show that this approach is expressive enough to represent types to type check imperative programs that use complex features like pointers, linked lists, and Rust life-times. Additionally, we show that the semantics are flexible enough to represent the extraction of equivalent functional programs-with these features erased-as part of the type checking process. To increase confidence in the correctness of these results and thus in the correctness of Heapster, all our proofs are formalized in Coq.
- 일반주제명
- Computer science
- 일반주제명
- Computer engineering
- 일반주제명
- Information science
- 키워드
- Heapster
- 키워드
- Semantics
- 키워드
- Separation logic
- 기타저자
- University of Pennsylvania Computer and Information Science
- 기본자료저록
- Dissertations Abstracts International. 86-02A.
- 전자적 위치 및 접속
- 로그인 후 원문을 볼 수 있습니다.
MARC
008250123s2024 us c eng d■001000017162602
■00520250211152031
■006m o d
■007cr#unu||||||||
■020 ▼a9798384023357
■035 ▼a(MiAaPQ)AAI31334358
■040 ▼aMiAaPQ▼cMiAaPQ
■0820 ▼a004
■1001 ▼aHe, Paul.
■24510▼aRely-Guarantee Semantics for Separation-Logic-Based Specification Extraction
■260 ▼a[Sl]▼bUniversity of Pennsylvania▼c2024
■260 1▼aAnn Arbor▼bProQuest Dissertations & Theses▼c2024
■300 ▼a151 p
■500 ▼aSource: Dissertations Abstracts International, Volume: 86-02, Section: A.
■500 ▼aAdvisor: Zdancewic, Steve.
■5021 ▼aThesis (Ph.D.)--University of Pennsylvania, 2024.
■520 ▼aWhile formal verification promises correctness guarantees about software, these guarantees themselves must be verified. This dissertation focuses on the soundness of the Heapster verification tool, which converts imperative programs into functional specifications. Heapster is able to do this by using a type system based on separation logic to guarantee memory safety, ensuring that pointer operations can be erased in the functional program. We prove the soundness of this type system using a novel concept called rely-guarantee permissions as the semantics of types. These rely-guarantee permissions are derived from rely-guarantee reasoning, a technique for reasoning about concurrent code. We show that this approach is expressive enough to represent types to type check imperative programs that use complex features like pointers, linked lists, and Rust life-times. Additionally, we show that the semantics are flexible enough to represent the extraction of equivalent functional programs-with these features erased-as part of the type checking process. To increase confidence in the correctness of these results and thus in the correctness of Heapster, all our proofs are formalized in Coq.
■590 ▼aSchool code: 0175.
■650 4▼aComputer science
■650 4▼aComputer engineering
■650 4▼aInformation science
■653 ▼aHeapster
■653 ▼aRely-guarantee permissions
■653 ▼aSemantics
■653 ▼aSeparation logic
■690 ▼a0984
■690 ▼a0464
■690 ▼a0723
■71020▼aUniversity of Pennsylvania▼bComputer and Information Science.
■7730 ▼tDissertations Abstracts International▼g86-02A.
■790 ▼a0175
■791 ▼aPh.D.
■792 ▼a2024
■793 ▼aEnglish
■85640▼uhttp://www.riss.kr/pdu/ddodLink.do?id=T17162602▼nKERIS▼z이 자료의 원문은 한국교육학술정보원에서 제공합니다.
