Please use this identifier to cite or link to this item: http://scholarbank.nus.edu.sg/handle/10635/14856
Title: Progressive program reasoning
Authors: RAZVAN VOICU
Keywords: program verification semantics liveness assertions logic
Issue Date: 30-May-2005
Source: RAZVAN VOICU (2005-05-30). Progressive program reasoning. ScholarBank@NUS Repository.
Abstract: This thesis presents a general program reasoning framework that is: (a)able to express a wide range of properties of programs, including but not limited to safety, liveness, and temporal properties; (b) compositional, in a Hoare-logic, assume-guarantee fashion; (c) allows the use of assertions; (d) has potential for combining automated methods with user-provided information; (e) incremental, in the sense that it is not needed for the reasoning process to complete in order to derive useful information about the program; rather, useful information can be derived after every reasoning step. We base our work on a semantics, called the progressive semantics, which captures an abstraction of the sequence of events in a program, as opposed to a at set of states. Program properties are descriptions, or rather, approximations of this semantics. Our approximation scheme uses a set of sets of states (or family) to approximate a set of states. Thus, an approximation of the progressive semantics at a program point is a sequence of families. To be able to reason symbolically about program behavior, we de ne assertion languages whose formulas are interpreted as sequences of families. We present the entire framework centered around a propagation operator, computing the strongest-postcondition of assertions across program points. Assertions are freely associated with any program points. Further, an assertion is not just a specification of properties which are to be proved, but may also be used as an assumption in order to prove other assertions, including itself. We thus introduce a notion of conditional correctness, which makes the entire framework incremental. Each assertion is initially assumed, and may, in the verification process, become proved. In the end, a proved program is correct on the proviso that its (hopefully few) unproven assertions are correct.
URI: http://scholarbank.nus.edu.sg/handle/10635/14856
Appears in Collections:Ph.D Theses (Open)

Show full item record
Files in This Item:
File Description SizeFormatAccess SettingsVersion 
Razvan_Voicu.PhDThesis.Progressive_Program_Reasoning.2004.pdf1.28 MBAdobe PDF

OPEN

NoneView/Download

Page view(s)

275
checked on Dec 11, 2017

Download(s)

201
checked on Dec 11, 2017

Google ScholarTM

Check


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