Practical formal methods for software analysis and development

Simple item page
dc.contributor.advisorDillig, Isil
dc.contributor.committeeMemberChaudhuri, Swarat
dc.contributor.committeeMemberBornholt, James
dc.contributor.committeeMemberAiken, Alex
dc.contributor.committeeMemberMcMillan, Kenneth
dc.creatorFerles, Konstantinos
dc.date.accessioned2021-05-04T20:16:22Z
dc.date.available2021-05-04T20:16:22Z
dc.date.created2020-12
dc.date.issued2021-03-14
dc.date.submittedDecember 2020
dc.date.updated2021-05-04T20:16:23Z
dc.description.abstractFormal methods techniques for improving software correctness and reliability fall into two categories, namely, program analysis and program synthesis. Program analysis techniques automatically find defects (or prove the absence thereof) in existing software. In a dual way, program synthesis techniques generate correct-by-construction code from high-level specifications. In this thesis, we propose an array of formal method techniques that further improve the state-of-the-art of program analysis techniques, while also applying program synthesis techniques in previously unexplored domains. Broadly speaking, the long history of program analysis can be summarized as the battle between precision and scalability. As a first step in this thesis, we propose a technique called program trimming that helps arbitrary safety-checking tools to achieve a better balance between precision and scalability. In a nutshell, program trimming semantically simplifies the program by eliminating provably correct execution paths. Because the number of execution paths is a typical scalability bottleneck for some techniques (e.g., symbolic execution) and a source of imprecision for others (e.g., abstract interpretation), program trimming can be used to improve both precision and scalability of program analysis tools. We have implemented our technique in a tool called Trimmer and showed that Trimmer significantly improves the behavior of two different program analyzers over a set of challenging verification benchmarks. Program synthesis, on the other hand, has only recently started to appear in more practical aspects of software development. Formal method techniques in this area aim to ease programming for several domains while targeting a broad range of programmers, from novices to experts. In this thesis, we propose a novel program synthesis technique, implemented in a tool called Expresso, that aids experts in writing correct and efficient concurrent programs. Specifically, Expresso allows programmers to implement concurrent programs using the implicit signaling paradigm, where the programmer specifies the condition under which a thread should block but she does not need to worry about explicitly signaling other threads when this condition becomes true. Given such an implicit signaling program, Expresso generates an efficient and correct-by-construction program that does not contain deadlocks caused by improper signaling. Our evaluation shows that Expresso is able to synthesize efficient implementations of real-world monitors with performance comparable to the one written by programming experts. Finally, we observe that certain monitors require their clients to use their API in a manner that conforms to a context-free specification. Statically verifying that a client conforms to a context-free API protocol cannot be handled by any prior technique. To rectify this and ensure that client applications properly use such protocols, we propose CFPChecker, a tool that verifies the correct usage of context-free API protocols. Given a program, P, and an API protocol expressed as a parameterized context-free grammar, GS, CFPChecker either proves that P conforms to GS or provides a genuine program trace that demonstrates an API misuse. We have evaluated our proposed technique on a wide variety of popular context-free API protocols and several clients drawn from popular open-source applications. Our experiments show that CFPChecker is effective in both verifying the correct usage and finding counterexamples of context-free API protocols.
dc.description.departmentComputer Scienceseng
dc.format.mimetypeapplication/pdf
dc.identifier.urihttps://hdl.handle.net/2152/85545
dc.identifier.urihttp://dx.doi.org/10.26153/tsw/12509
dc.subjectSoftware correctness
dc.subjectSoftware reliability
dc.subjectProgram verification
dc.subjectProgram synthesis
dc.titlePractical formal methods for software analysis and development
dc.typeThesis
dc.type.materialtext
thesis.degree.departmentComputer Sciences
thesis.degree.disciplineComputer Science
thesis.degree.grantorThe University of Texas at Austin
thesis.degree.levelDoctoral
thesis.degree.nameDoctor of Philosophy

Access full-text files

Original bundle

Now showing 1 - 1 of 1
Thumbnail Image
Name:
FERLES-DISSERTATION-2020.pdf
Size:
2.96 MB
Format:
Adobe Portable Document Format
Download

License bundle

Now showing 1 - 2 of 2
No Thumbnail Available
Name:
PROQUEST_LICENSE.txt
Size:
4.46 KB
Format:
Plain Text
Description:
Download
No Thumbnail Available
Name:
LICENSE.txt
Size:
1.85 KB
Format:
Plain Text
Description:
Download

Collections

UT Electronic Theses and Dissertations