Please use this identifier to cite or link to this item: http://scholarbank.nus.edu.sg/handle/10635/119267
Title: Enhancing Total Correctness Proofs in Program Verification
Authors: LE TON CHANH
Keywords: software verification, total correctness, termination inference, non-termination inference, resource logic, proof slicing
Issue Date: 26-Nov-2014
Source: 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.
URI: http://scholarbank.nus.edu.sg/handle/10635/119267
Appears in Collections:Ph.D Theses (Open)

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

OPEN

NoneView/Download

Page view(s)

118
checked on Jan 21, 2018

Download(s)

94
checked on Jan 21, 2018

Google ScholarTM

Check


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