1 option
Program Synthesis for Declarative Systems / Haoxian Chen.
- Format:
- Book
- Thesis/Dissertation
- Author/Creator:
- Chen, Haoxian, author.
- Language:
- English
- Subjects (All):
- Computer science.
- Computer engineering.
- Information science.
- Computer and Information Science--Penn dissertations.
- Penn dissertations--Computer and Information Science.
- Local Subjects:
- Computer science.
- Computer engineering.
- Information science.
- Computer and Information Science--Penn dissertations.
- Penn dissertations--Computer and Information Science.
- Physical Description:
- 1 online resource (145 pages)
- Distribution:
- Ann Arbor : ProQuest Dissertations & Theses, 2023
- Contained In:
- Dissertations Abstracts International 84-12A.
- Place of Publication:
- [Philadelphia, Pennsylvania] : University of Pennsylvania, 2022.
- Language Note:
- English
- Summary:
- 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.
- Notes:
- Source: Dissertations Abstracts International, Volume: 84-12, Section: A.
- Advisors: Loo, Boon Thau; Committee members: Naik, Mayur; Scedrov, Andre; Liu, Vincent; Wang, Yuepeng.
- Department: Computer and Information Science.
- Ph.D. University of Pennsylvania 2023.
- Local Notes:
- School code: 0175
- ISBN:
- 9798379750794
- Access Restriction:
- Restricted for use by site license.
The Penn Libraries is committed to describing library materials using current, accurate, and responsible language. If you discover outdated or inaccurate language, please fill out this feedback form to report it and suggest alternative language.