Date of Award

Fall 1-1-2025

Document Type

Dissertation

Degree Name

Doctor of Philosophy (PhD)

Department

Computer Science

First Advisor

Shao, Zhong

Abstract

Formal verification has emerged as the most rigorous approach for building reliable computer systems. Certified systems, in particular, are accompanied by a formal specification and a machine-checkable proof of correctness, enabling independent verification by third parties. However, verifying large-scale, heterogeneous systems presents significant challenges that current techniques cannot adequately address. Such systems require compositional methods that can flexibly integrate diverse verification approaches, including program logic, certified compilation, and data abstraction. While compositional semantics offers a promising foundation, existing frameworks are typically built on specialized operational models that resist integration with one another. This dissertation presents a three-dimensional algebraic compositional structure that unifies diverse verification techniques within a single coherent foundation and enables systematic composition across program modules, abstraction levels, and system state components. This work first extends CompCertO to create the OpenTX and OpenTE frameworks, which conform to the three-dimensional compositional structure and demonstrate practical verification capabilities. Building on these foundations, the dissertation then develops a more general strategy-based semantic model with refinement conventions that also conforms to the three-dimensional approach and provides the core framework for compositional verification. All components are fully mechanized in the Rocq proof assistant, and their capabilities are demonstrated through multiple case studies.

Download

Share

COinS