Date of Award
8-2013
Document Type
Dissertation
Degree Name
Doctor of Philosophy (PhD)
Legacy Department
Computer Science
Committee Chair/Advisor
Sitaraman, Murali
Committee Member
Dean , Brian C
Committee Member
Hallstrom , Jason O
Committee Member
Pargas , Roy P
Abstract
Developing a verifying compiler---a compiler that proves that components are correct with respect to their specifications---is a grand challenge for the computing community. The prevailing view of the software engineering community is that this problem is necessarily difficult because, to-date, the resultant verification conditions necessary to prove software correctness have required powerful automated provers and deep mathematical insight to dispatch. This seems counter-intuitive, however, since human programmers only rarely resort to deep mathematics to assure themselves that their code works.
In this work, we show that well-specified and well-engineered software supported by a flexible, extensible mathematical system can yield verification conditions that are sufficiently straightforward to be dispatched by a minimalist rewrite prover. We explore techniques for making such a system both powerful and user-friendly, and for tuning an automated prover to the verification task. In addition to influencing the design of our own system, RESOLVE, this exploration benefits the greater verification community by informing specification and theory design and encouraging greater integration between nuanced mathematical systems and powerful programming languages.
This dissertation presents the design and an implementation of a minimalist rewrite prover tuned for the software verification task. It supports the prover with the design and implementation of a flexible, extensible mathematical system suitable for use with an industrial-strength programming language. This system is employed within a well-integrated specification framework. The dissertation validates the central thesis that verification conditions for well-engineered software can be dispatched easily by applying these tools and methods to a number of benchmark components and collecting and analyzing the resulting data.
Recommended Citation
Smith, Hampton, "Engineering Specifications and Mathematics for Verified Software" (2013). All Dissertations. 1132.
https://tigerprints.clemson.edu/all_dissertations/1132