서브메뉴
검색
Increasing the Practicality of Verification Using Incomplete Solutions
Increasing the Practicality of Verification Using Incomplete Solutions
상세정보
- 자료유형
- 학위논문 서양
- 최종처리일시
- 20260202103640
- ISBN
- 9798314873939
- DDC
- 004
- 서명/저자
- Increasing the Practicality of Verification Using Incomplete Solutions
- 발행사항
- [Sl] : University of Michigan, 2025
- 발행사항
- Ann Arbor : ProQuest Dissertations & Theses, 2025
- 형태사항
- 110 p
- 주기사항
- Source: Dissertations Abstracts International, Volume: 86-11, Section: B.
- 주기사항
- Advisor: Kapritsos, Manos.
- 학위논문주기
- Thesis (Ph.D.)--University of Michigan, 2025.
- 초록/해제
- 요약Building correct software systems is challenging. To ensure correctness, developers have increasingly turned to formal verification to help achieve this goal. Verification provides strong assurances of correctness by construction. Developers write proof annotations to show that their implementation adheres to desired properties captured in a formal specification. Checking if the implementation meets the specification is automated by encoding the proof, specification, and implementation as a satisfiability query and is checked by a Satisfiability Modulo Theories (SMT) solver. However, two fundamental challenges limit the guarantees and the ease of verifying programs with automated theorem provers: the inability to prove the correctness of a specification and the incompleteness of underlying SMT solvers. These shortcomings inevitably require manual effort and expertise to overcome, deterring the broader adoption of automated verification. This dissertation demonstrates how lightweight techniques can assist developers in overcoming the fundamental limitations of verifying programs with automated theorem provers. First, it explores how classic testing practices can be adapted to test formal specifications. Accordingly, this dissertation presents IronSpec, a specification testing framework that integrates automatic and manual testing techniques to enhance the reliability of formal specifications. Next, this dissertation examines the debugging challenges of failing proofs. Even with a correct specification, a proof may fail for different reasons; unfortunately, underlying SMT solvers do not differentiate between them. To help resolve these debugging dilemmas, this dissertation introduces the Finitized Proof Projection technique and a proof assistant, ProofLens. ProofLens embodies this technique, helping to identify hints about why a proof failed by creating and verifying a finite approximation of the original program. Finally, as an application of formal verification and in the greater pursuit of building robust systems, this dissertation proves that the original criteria for learning values in the Paxos protocol is stronger than necessary. While verification helps ensure program correctness, it cannot guard against hardware failures. Paxos is a standard building block in state machine replication, a practice commonly used to build robust systems in the presence of hardware failures. This dissertation proves how the discrete numbering of ballots in Paxos enables a safe relaxation of the criteria for learning values.
- 일반주제명
- Computer science
- 일반주제명
- Engineering
- 일반주제명
- Information technology
- 기타저자
- University of Michigan Computer Science & Engineering
- 기본자료저록
- Dissertations Abstracts International. 86-11B.
- 전자적 위치 및 접속
- 로그인 후 원문을 볼 수 있습니다.
MARC
008260126s2025 us c eng d■001000017358078
■00520260202103640
■006m o d
■007cr#unu||||||||
■020 ▼a9798314873939
■035 ▼a(MiAaPQ)AAI32092523
■035 ▼a(MiAaPQ)umichrackham006035
■040 ▼aMiAaPQ▼cMiAaPQ
■0820 ▼a004
■1001 ▼aGoldweber, Eli David.
■24510▼aIncreasing the Practicality of Verification Using Incomplete Solutions
■260 ▼a[Sl]▼bUniversity of Michigan▼c2025
■260 1▼aAnn Arbor▼bProQuest Dissertations & Theses▼c2025
■300 ▼a110 p
■500 ▼aSource: Dissertations Abstracts International, Volume: 86-11, Section: B.
■500 ▼aAdvisor: Kapritsos, Manos.
■5021 ▼aThesis (Ph.D.)--University of Michigan, 2025.
■520 ▼aBuilding correct software systems is challenging. To ensure correctness, developers have increasingly turned to formal verification to help achieve this goal. Verification provides strong assurances of correctness by construction. Developers write proof annotations to show that their implementation adheres to desired properties captured in a formal specification. Checking if the implementation meets the specification is automated by encoding the proof, specification, and implementation as a satisfiability query and is checked by a Satisfiability Modulo Theories (SMT) solver. However, two fundamental challenges limit the guarantees and the ease of verifying programs with automated theorem provers: the inability to prove the correctness of a specification and the incompleteness of underlying SMT solvers. These shortcomings inevitably require manual effort and expertise to overcome, deterring the broader adoption of automated verification. This dissertation demonstrates how lightweight techniques can assist developers in overcoming the fundamental limitations of verifying programs with automated theorem provers. First, it explores how classic testing practices can be adapted to test formal specifications. Accordingly, this dissertation presents IronSpec, a specification testing framework that integrates automatic and manual testing techniques to enhance the reliability of formal specifications. Next, this dissertation examines the debugging challenges of failing proofs. Even with a correct specification, a proof may fail for different reasons; unfortunately, underlying SMT solvers do not differentiate between them. To help resolve these debugging dilemmas, this dissertation introduces the Finitized Proof Projection technique and a proof assistant, ProofLens. ProofLens embodies this technique, helping to identify hints about why a proof failed by creating and verifying a finite approximation of the original program. Finally, as an application of formal verification and in the greater pursuit of building robust systems, this dissertation proves that the original criteria for learning values in the Paxos protocol is stronger than necessary. While verification helps ensure program correctness, it cannot guard against hardware failures. Paxos is a standard building block in state machine replication, a practice commonly used to build robust systems in the presence of hardware failures. This dissertation proves how the discrete numbering of ballots in Paxos enables a safe relaxation of the criteria for learning values.
■590 ▼aSchool code: 0127.
■650 4▼aComputer science
■650 4▼aEngineering
■650 4▼aInformation technology
■653 ▼aFormal verification
■653 ▼aAutomated theorem proving
■653 ▼aDistributed systems
■653 ▼aSpecification testing
■653 ▼aSatisfiability Modulo Theories
■690 ▼a0984
■690 ▼a0489
■690 ▼a0537
■71020▼aUniversity of Michigan▼bComputer Science & Engineering.
■7730 ▼tDissertations Abstracts International▼g86-11B.
■790 ▼a0127
■791 ▼aPh.D.
■792 ▼a2025
■793 ▼aEnglish
■85640▼uhttp://www.riss.kr/pdu/ddodLink.do?id=T17358078▼nKERIS▼z이 자료의 원문은 한국교육학술정보원에서 제공합니다.
