Enhancing Total Correctness Proofs in Program Verification

Abstract

Recent advances in software verification mainly focus on partial correctness with safety properties of software systems. This thesis develops methodologies to enhance expressiveness, focusing on program termination and non-termination reasoning, and scalability, focusing on the concept of modularity, of total correctness proofs in program verification. Firstly, we introduce a unified logical framework for specifying and verifying termination and non-termination properties of programs in terms of resource reasoning. Secondly, we present a modular inference mechanism for summarizing termination and non-termination behaviors of each method in programs with abduction and case analysis. Lastly, we develop a formal framework for proof slicing in verification that can aggressively reduce the size of the discharged proof obligations as a means of performance improvement. The experimental results show the scalability and efficiency of our mechanisms against state-of-the-art systems.