Higher-order Symbolic Execution

Simple item page
dc.contributor.advisorVan Horn, Daviden_US
dc.contributor.authorNguyen, Phucen_US
dc.contributor.departmentComputer Scienceen_US
dc.contributor.publisherDigital Repository at the University of Marylanden_US
dc.contributor.publisherUniversity of Maryland (College Park, Md.)en_US
dc.date.accessioned2020-02-01T06:40:08Z
dc.date.available2020-02-01T06:40:08Z
dc.date.issued2019en_US
dc.description.abstractThere are multiple challenges in designing a static verification system for an existing programming language. There is the technical challenge of achieving soundness and precision in the presence of expressive language features such as dynamic typing, higher-order functions, mutable state, control operators, and their idiomatic usage. There is also the practical challenge of allowing gradual adoption of verification in the face of large code bases in the real world. Failure to achieve this gradual property hinders the system’s adoption in practice: Existing correct but unverifiable components due to the lack of annotations, the unavailability or the source code, or the inherent incompleteness of static checking would require tedious modifications to a program to make it safe and executable again. This dissertation shows a simple framework for integrating rich static reasoning into an existing expressive programming language by leveraging dynamic checks and a novel form of symbolic execution. Higher-order symbolic execution enables gradual verification that is sound, precise, and modular for expressive programming languages. First, symbolic execution can be generalized to higher-orderprogramming languages: Symbolic functions do not make bug-finding and counterexample generation fundamentally more difficult, and the counterexample search is relatively complete with respect to the underlying first-order SMT solver. Next, finitized symbolic execution can be viewed as verification, where dynamic contracts are the specifications, and the lack of run-time errors signifies correctness. A further refinement to the semantics of applying symbolic functions yields a verifier that soundly handles higher-order imperative programs with challenging patterns such as higher-order stateful call-backs and aliases to mutable state. Finally, with a novel formulation of termination as a run-time contract, symbolic execution can also verify total-correctness. Using symbolic execution to statically verify dynamic checks has important consequences in scaling the tool in practice. Because symbolic execution closely models the standard semantics, dynamic language features and idioms such as first-class contracts and run-time type tests do not introduce new challenges to verification and bug-finding. Moreover, the method allows gradual addition and strengthening of specifications into an existing program without requiring a global re-factorization: The programmer can decide to stop adding contracts at any point and still have an executable and safe program. Properties that are unverifiable statically can be left as residual checks with the existing familiar semantics. Programmers benefit from static verification as much as possible without compromising language features that may not fit in a particular static discipline. In particular, this dissertation lays out the path to adding gradual theorem proving into an existing untyped, higher-order, imperative programming language.en_US
dc.identifierhttps://doi.org/10.13016/f1cz-eaja
dc.identifier.urihttp://hdl.handle.net/1903/25444
dc.language.isoenen_US
dc.subject.pqcontrolledComputer scienceen_US
dc.subject.pquncontrolleddynamic analysisen_US
dc.subject.pquncontrolledgradual-typingen_US
dc.subject.pquncontrolledstatic analysisen_US
dc.subject.pquncontrolledsymbolic executionen_US
dc.subject.pquncontrolledtheorem provingen_US
dc.subject.pquncontrolledverificationen_US
dc.titleHigher-order Symbolic Executionen_US
dc.typeDissertationen_US

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
Nguyen_umd_0117E_20443.pdf
Size:
559.04 KB
Format:
Adobe Portable Document Format
Download

Collections

UMD Theses and Dissertations
Computer Science Theses and Dissertations