Please use this identifier to cite or link to this item:
Title: Enhancing Total Correctness Proofs in Program Verification
Keywords: software verification, total correctness, termination inference, non-termination inference, resource logic, proof slicing
Issue Date: 26-Nov-2014
Citation: LE TON CHANH (2014-11-26). Enhancing Total Correctness Proofs in Program Verification. ScholarBank@NUS Repository.
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.
Appears in Collections:Ph.D Theses (Open)

Show full item record
Files in This Item:
File Description SizeFormatAccess SettingsVersion 
LeTonChanh.pdf744.11 kBAdobe PDF



Page view(s)

checked on Nov 8, 2019


checked on Nov 8, 2019

Google ScholarTM


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.