Date of Award
12-2022
Document Type
Dissertation
Degree Name
Doctor of Philosophy (PhD)
Department
Computer Science
Committee Chair/Advisor
Murali Sitaraman
Committee Member
Brian C. Dean
Committee Member
Jason O. Hallstrom
Committee Member
Eileen T. Kraemer
Abstract
Formal software verification systems must be designed to adapt to growth in the scope and complexity of software, driven by expanding capabilities of computer hardware and domain of potential usage. They must provide specification languages that are flexible and rich enough to allow software developers to write precise and comprehensible specifications for a full spectrum of object-based software components. Rich specification languages allow for arbitrary extensions to the library of mathematical theories, and critically, verification of programs with such specifications require a universal automated prover. Most existing verification systems either incorporate specification languages limited to first-order logic, which lacks the richness necessary to write adequate specifications, or provide automated provers covering only a fixed collection of mathematical theories, which lack the compass to specify and verify sophisticated object-based software.
This dissertation presents an overall design of Uni-Prover, a universal automated prover for atomic sequents to verify software specified with rich languages. Such a prover is a necessary element of any adequate automated verification system of the future. The design contains components to accommodate changes or upgrades that may happen. The congruence class registry at the center of Uni-Prover handles all core manipulations necessary to verify programs, and it includes a multi-level organization for effective searching of the registry. The full functional behavior of the registry component is described mathematically, and a prototype implementation is given. Additionally, the "contiguous instantiation strategy," a strategy that requires neither user-supplied heuristics nor triggers when instantiating universally quantified theorems in any theory, is detailed to minimize verification steps by avoiding the proliferation of sequents in the instantiation process.
Recommended Citation
Mbwambo, Nicodemus Msafiri John, "Uni-Prover: A Universal Automated Prover for Specificationally Rich Languages" (2022). All Dissertations. 3247.
https://tigerprints.clemson.edu/all_dissertations/3247