서브메뉴
검색
Program Synthesis for Declarative Systems- [electronic resource]
Program Synthesis for Declarative Systems- [electronic resource]
상세정보
- 자료유형
- 학위논문
- Control Number
- 0016931332
- International Standard Book Number
- 9798379750794
- Dewey Decimal Classification Number
- 004
- Main Entry-Personal Name
- Chen, Haoxian.
- Publication, Distribution, etc. (Imprint
- [S.l.] : University of Pennsylvania., 2023
- Publication, Distribution, etc. (Imprint
- Ann Arbor : ProQuest Dissertations & Theses, 2023
- Physical Description
- 1 online resource(145 p.)
- General Note
- Source: Dissertations Abstracts International, Volume: 84-12, Section: A.
- General Note
- Advisor: Loo, Boon Thau.
- Dissertation Note
- Thesis (Ph.D.)--University of Pennsylvania, 2023.
- Restrictions on Access Note
- This item must not be sold to any third party vendors.
- Summary, Etc.
- 요약Formal methods are essential in assuring system correctness. However, formal specification languages have steep learning curves, thus hindering broader application to system development in practice. To address this problem, we propose NetSpec, a tool that generates system specification via intuitive example-based interface, DeCon, a high-level language for Ethereum smart contracts that provides unified interfaces for contract implementation and specification, and DCV, a safety verification tool for DeCon.NetSpec aims to be i) highly expressive, capable of synthesizing network specifications with complex semantics; ii) scalable, by virtue of using a novel stochastic search algorithm to efficiently explore an unbounded solution space, and iii) robust, avoiding the need for exhaustive input-output examples by actively generating new examples. Our experiments demonstrate that NetSpec can synthesize a wide range of specifications used in network verification, analysis, and implementations. Furthermore, NetSpec improves upon existing approaches in terms of expressiveness, efficiency, and robustness to examples.DeCon, a specification language for Ethereum smart contracts, models a contract as a set of relational tables that store transaction records, driven by the observation that smart contract operations and contract-level properties can be naturally expressed as relational constraints. This relational representation enables convenient specification of contract properties, facilitates run-time monitoring of potential property violations, and brings clarity to debugging via data provenance. DeCon programs are compiled into executable Solidity programs, with instrumentation for run-time property monitoring. Our case studies demonstrate that DeCon can implement realistic smart contracts such as ERC20 and ERC721 digital tokens. The evaluation shows that DeCon has comparable efficiency with the open-source reference implementation, incurring 14% median gas overhead for execution, and another 16% median gas overhead for run-time verification.DCV is a sound and fully automatic verification tool for DeCon contracts. It proves safety properties by mathematical induction and can automatically infer inductive invariants without annotations from the developer. Our evaluation shows that DCV is effective in verifying smart contracts adapted from public repositories, and can verify contracts not supported by other tools. Furthermore, DCV significantly outperforms baseline tools in verification time.
- Subject Added Entry-Topical Term
- Computer science.
- Subject Added Entry-Topical Term
- Computer engineering.
- Subject Added Entry-Topical Term
- Information science.
- Index Term-Uncontrolled
- Computer networks
- Index Term-Uncontrolled
- Declarative programming
- Index Term-Uncontrolled
- Program synthesis
- Index Term-Uncontrolled
- Program verification
- Index Term-Uncontrolled
- Smart contracts
- Index Term-Uncontrolled
- NetSpec
- Index Term-Uncontrolled
- DeCon
- Added Entry-Corporate Name
- University of Pennsylvania Computer and Information Science
- Host Item Entry
- Dissertations Abstracts International. 84-12A.
- Host Item Entry
- Dissertation Abstract International
- Electronic Location and Access
- 로그인을 한후 보실 수 있는 자료입니다.
- Control Number
- joongbu:641753
MARC
008240221s2023 ulk 00 kor■001000016931332
■00520240214100003
■006m o d
■007cr#unu||||||||
■020 ▼a9798379750794
■035 ▼a(MiAaPQ)AAI30249291
■040 ▼aMiAaPQ▼cMiAaPQ
■0820 ▼a004
■1001 ▼aChen, Haoxian.
■24510▼aProgram Synthesis for Declarative Systems▼h[electronic resource]
■260 ▼a[S.l.]▼bUniversity of Pennsylvania. ▼c2023
■260 1▼aAnn Arbor▼bProQuest Dissertations & Theses▼c2023
■300 ▼a1 online resource(145 p.)
■500 ▼aSource: Dissertations Abstracts International, Volume: 84-12, Section: A.
■500 ▼aAdvisor: Loo, Boon Thau.
■5021 ▼aThesis (Ph.D.)--University of Pennsylvania, 2023.
■506 ▼aThis item must not be sold to any third party vendors.
■520 ▼aFormal methods are essential in assuring system correctness. However, formal specification languages have steep learning curves, thus hindering broader application to system development in practice. To address this problem, we propose NetSpec, a tool that generates system specification via intuitive example-based interface, DeCon, a high-level language for Ethereum smart contracts that provides unified interfaces for contract implementation and specification, and DCV, a safety verification tool for DeCon.NetSpec aims to be i) highly expressive, capable of synthesizing network specifications with complex semantics; ii) scalable, by virtue of using a novel stochastic search algorithm to efficiently explore an unbounded solution space, and iii) robust, avoiding the need for exhaustive input-output examples by actively generating new examples. Our experiments demonstrate that NetSpec can synthesize a wide range of specifications used in network verification, analysis, and implementations. Furthermore, NetSpec improves upon existing approaches in terms of expressiveness, efficiency, and robustness to examples.DeCon, a specification language for Ethereum smart contracts, models a contract as a set of relational tables that store transaction records, driven by the observation that smart contract operations and contract-level properties can be naturally expressed as relational constraints. This relational representation enables convenient specification of contract properties, facilitates run-time monitoring of potential property violations, and brings clarity to debugging via data provenance. DeCon programs are compiled into executable Solidity programs, with instrumentation for run-time property monitoring. Our case studies demonstrate that DeCon can implement realistic smart contracts such as ERC20 and ERC721 digital tokens. The evaluation shows that DeCon has comparable efficiency with the open-source reference implementation, incurring 14% median gas overhead for execution, and another 16% median gas overhead for run-time verification.DCV is a sound and fully automatic verification tool for DeCon contracts. It proves safety properties by mathematical induction and can automatically infer inductive invariants without annotations from the developer. Our evaluation shows that DCV is effective in verifying smart contracts adapted from public repositories, and can verify contracts not supported by other tools. Furthermore, DCV significantly outperforms baseline tools in verification time.
■590 ▼aSchool code: 0175.
■650 4▼aComputer science.
■650 4▼aComputer engineering.
■650 4▼aInformation science.
■653 ▼aComputer networks
■653 ▼aDeclarative programming
■653 ▼aProgram synthesis
■653 ▼aProgram verification
■653 ▼aSmart contracts
■653 ▼aNetSpec
■653 ▼aDeCon
■690 ▼a0984
■690 ▼a0464
■690 ▼a0723
■71020▼aUniversity of Pennsylvania▼bComputer and Information Science.
■7730 ▼tDissertations Abstracts International▼g84-12A.
■773 ▼tDissertation Abstract International
■790 ▼a0175
■791 ▼aPh.D.
■792 ▼a2023
■793 ▼aEnglish
■85640▼uhttp://www.riss.kr/pdu/ddodLink.do?id=T16931332▼nKERIS▼z이 자료의 원문은 한국교육학술정보원에서 제공합니다.
■980 ▼a202402▼f2024
미리보기
내보내기
chatGPT토론
Ai 추천 관련 도서
Подробнее информация.
- Бронирование
- 캠퍼스간 도서대출
- 서가에 없는 책 신고
- моя папка
