Sciweavers

Share
ACSC
2004
IEEE

Automatic Derivation of Loop Termination Conditions to Support Verification

9 years 7 months ago
Automatic Derivation of Loop Termination Conditions to Support Verification
This paper introduces a repeatable and constructive approach to the analysis of loop progress and termination conditions in imperative programs. It is applicable to all loops for which a variant function can be defined using only loop guard variables. The approach involves the algorithmic derivation of loop progress and termination conditions directly from the code itself. The derivation of these conditions has been automated in a prototype tool. The conditions yielded by the automated algorithms are useful for reasoning about correctness in verification based code inspections as well as for the documentation and assessment of program preconditions. Unlike existing formal approaches to termination investigation, which are reliant on the presence of formal specifications, this approach is applicable to undocumented programs as well as formally specified programs. We present the algorithms and formal methods implemented in a prototype tool for deriving loop progress and termination cond...
Daniel Powell
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2004
Where ACSC
Authors Daniel Powell
Comments (0)
books