서브메뉴
검색
Combining Datalog and SAT-Based Solving in Code-Reasoning Tools- [electronic resource]
Combining Datalog and SAT-Based Solving in Code-Reasoning Tools- [electronic resource]
상세정보
- 자료유형
- 학위논문
- Control Number
- 0016935042
- International Standard Book Number
- 9798380848657
- Dewey Decimal Classification Number
- 004
- Main Entry-Personal Name
- Bembenek, Aaron.
- Publication, Distribution, etc. (Imprint
- [S.l.] : Harvard University., 2023
- Publication, Distribution, etc. (Imprint
- Ann Arbor : ProQuest Dissertations & Theses, 2023
- Physical Description
- 1 online resource(193 p.)
- General Note
- Source: Dissertations Abstracts International, Volume: 85-05, Section: B.
- General Note
- Advisor: Chong, Stephen.
- Dissertation Note
- Thesis (Ph.D.)--Harvard University, 2023.
- Restrictions on Access Note
- This item must not be sold to any third party vendors.
- Summary, Etc.
- 요약Datalog and SAT solving are powerful forms of automated logic that are both used to reason about the correctness of software. However, they are very different, and they are not typically combined in the same automated reasoning tool. This dissertation explores how to build code-reasoning tools that combine these complementary technologies, through two main thrusts: 1) the design and implementation of the logic-centric programming language Formulog, and 2) a progression of tools for Datalog program synthesis. In doing so, it explores the challenge of combining Datalog and SAT-based reasoning at multiple levels, viewing it variously as a language design problem, a system implementation problem, and a constraint solving problem. A domain-specific language for writing static analyses (programs that analyze other programs), Formulog augments Datalog with first-order functional programming and SMT solving, an extension to SAT solving. In Formulog, SMT formulas are data that can be constructed and inspected; a novel type system allows expressive SMT formulas while ensuring that neither normal evaluation nor SMT solving crashes. Formulog's combination of features makes it possible to state a range of SMT-based analyses in a way that is both close to their formal specifications, and amenable to high-level optimizations and efficient evaluation.In addition to the design of Formulog, this dissertation presents implementation strategies for achieving good runtime performance. This includes a compiler from Formulog to Souffle (an established Datalog system), as well as "eager evaluation," a novel parallel execution algorithm for Datalog that leads to improved SMT solving times when used to evaluate Formulog programs. Thanks to these techniques, Formulog's performance is competitive with (and some-times much better than) non-Datalog reference implementations on diverse SMT-based case studies: refinement type checking, bottom-up points-to analysis, and symbolic execution. Finally, the dissertation presents a progression of tools for synthesizing Datalog programs (i.e., generating them automatically from specifications). Each tool explores a different way of combining Datalog and SAT/SMT solving; the ultimate solution takes advantage of answer set programming (ASP)-a constraint solving paradigm that subsumes Datalog and SAT-like reasoning-and achieves nearly order-of-magnitude geometric mean speedups over the prior state-of-the-art solution. This work elucidates connections between Datalog and SAT/SMT solving (for example, it shows that every Datalog program is the basis of a theoretically efficient SMT theory), and suggests the potential of using ASP to reason about Datalog programs.
- Subject Added Entry-Topical Term
- Computer science.
- Subject Added Entry-Topical Term
- Computer engineering.
- Index Term-Uncontrolled
- Datalog programs
- Index Term-Uncontrolled
- Logic programming
- Index Term-Uncontrolled
- Static analyses
- Index Term-Uncontrolled
- Program synthesis
- Index Term-Uncontrolled
- SAT solving
- Index Term-Uncontrolled
- SMT solving
- Added Entry-Corporate Name
- Harvard University Engineering and Applied Sciences - Computer Science
- Host Item Entry
- Dissertations Abstracts International. 85-05B.
- Host Item Entry
- Dissertation Abstract International
- Electronic Location and Access
- 로그인을 한후 보실 수 있는 자료입니다.
- Control Number
- joongbu:640799
MARC
008240220s2023 ulk 00 kor■001000016935042
■00520240214101846
■006m o d
■007cr#unu||||||||
■020 ▼a9798380848657
■035 ▼a(MiAaPQ)AAI30639178
■040 ▼aMiAaPQ▼cMiAaPQ
■0820 ▼a004
■1001 ▼aBembenek, Aaron.▼0(orcid)0000-0002-3677-701X
■24510▼aCombining Datalog and SAT-Based Solving in Code-Reasoning Tools▼h[electronic resource]
■260 ▼a[S.l.]▼bHarvard University. ▼c2023
■260 1▼aAnn Arbor▼bProQuest Dissertations & Theses▼c2023
■300 ▼a1 online resource(193 p.)
■500 ▼aSource: Dissertations Abstracts International, Volume: 85-05, Section: B.
■500 ▼aAdvisor: Chong, Stephen.
■5021 ▼aThesis (Ph.D.)--Harvard University, 2023.
■506 ▼aThis item must not be sold to any third party vendors.
■520 ▼aDatalog and SAT solving are powerful forms of automated logic that are both used to reason about the correctness of software. However, they are very different, and they are not typically combined in the same automated reasoning tool. This dissertation explores how to build code-reasoning tools that combine these complementary technologies, through two main thrusts: 1) the design and implementation of the logic-centric programming language Formulog, and 2) a progression of tools for Datalog program synthesis. In doing so, it explores the challenge of combining Datalog and SAT-based reasoning at multiple levels, viewing it variously as a language design problem, a system implementation problem, and a constraint solving problem. A domain-specific language for writing static analyses (programs that analyze other programs), Formulog augments Datalog with first-order functional programming and SMT solving, an extension to SAT solving. In Formulog, SMT formulas are data that can be constructed and inspected; a novel type system allows expressive SMT formulas while ensuring that neither normal evaluation nor SMT solving crashes. Formulog's combination of features makes it possible to state a range of SMT-based analyses in a way that is both close to their formal specifications, and amenable to high-level optimizations and efficient evaluation.In addition to the design of Formulog, this dissertation presents implementation strategies for achieving good runtime performance. This includes a compiler from Formulog to Souffle (an established Datalog system), as well as "eager evaluation," a novel parallel execution algorithm for Datalog that leads to improved SMT solving times when used to evaluate Formulog programs. Thanks to these techniques, Formulog's performance is competitive with (and some-times much better than) non-Datalog reference implementations on diverse SMT-based case studies: refinement type checking, bottom-up points-to analysis, and symbolic execution. Finally, the dissertation presents a progression of tools for synthesizing Datalog programs (i.e., generating them automatically from specifications). Each tool explores a different way of combining Datalog and SAT/SMT solving; the ultimate solution takes advantage of answer set programming (ASP)-a constraint solving paradigm that subsumes Datalog and SAT-like reasoning-and achieves nearly order-of-magnitude geometric mean speedups over the prior state-of-the-art solution. This work elucidates connections between Datalog and SAT/SMT solving (for example, it shows that every Datalog program is the basis of a theoretically efficient SMT theory), and suggests the potential of using ASP to reason about Datalog programs.
■590 ▼aSchool code: 0084.
■650 4▼aComputer science.
■650 4▼aComputer engineering.
■653 ▼aDatalog programs
■653 ▼aLogic programming
■653 ▼aStatic analyses
■653 ▼aProgram synthesis
■653 ▼aSAT solving
■653 ▼aSMT solving
■690 ▼a0984
■690 ▼a0464
■690 ▼a0800
■71020▼aHarvard University▼bEngineering and Applied Sciences - Computer Science.
■7730 ▼tDissertations Abstracts International▼g85-05B.
■773 ▼tDissertation Abstract International
■790 ▼a0084
■791 ▼aPh.D.
■792 ▼a2023
■793 ▼aEnglish
■85640▼uhttp://www.riss.kr/pdu/ddodLink.do?id=T16935042▼nKERIS▼z이 자료의 원문은 한국교육학술정보원에서 제공합니다.
■980 ▼a202402▼f2024
