A refinement-based framework for computing loop behavior

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

The development, certification and evolution of dependable software requires the ability to analyze software artifacts in all their extensive detail. This, in turn, is contingent upon availability of reliable, certified tools that can rigorously analyze the behavior and properties of software artifacts. One of the most difficult challenges in the development of such a tool is the ability to derive the function of a loop from a static analysis of its source code. In this paper, we discuss the main tenets of our approach to this problem, based on a relation-theoretic refinement calculus, and outline its results, insights, and prospects.

Original languageEnglish (US)
Title of host publication31st Annual IEEE Software Engineering Workshop, SEW-31 2007 - Proceedings
Pages144-153
Number of pages10
DOIs
StatePublished - 2007
Event31st Annual IEEE Software Engineering Workshop, SEW-31 2007 - Columbia, MD, United States
Duration: Mar 6 2007Mar 8 2007

Publication series

NameProceedings - International Conference on Software Engineering
ISSN (Print)0270-5257

Other

Other31st Annual IEEE Software Engineering Workshop, SEW-31 2007
CountryUnited States
CityColumbia, MD
Period3/6/073/8/07

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • Computing loop behavior
  • Function extraction
  • Loop functions
  • Loop invariants
  • Refinement calculus
  • Relational calculus

Fingerprint Dive into the research topics of 'A refinement-based framework for computing loop behavior'. Together they form a unique fingerprint.

Cite this