A refinement-based framework for computing loop behavior

Ali Mili

doi:10.1109/SEW.2007.87

A refinement-based framework for computing loop behavior

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	31st Annual IEEE Software Engineering Workshop, SEW-31 2007 - Proceedings
Pages	144-153
Number of pages	10
DOIs	https://doi.org/10.1109/SEW.2007.87
State	Published - 2007
Event	31st Annual IEEE Software Engineering Workshop, SEW-31 2007 - Columbia, MD, United States Duration: Mar 6 2007 → Mar 8 2007

Publication series

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

Other

Other	31st Annual IEEE Software Engineering Workshop, SEW-31 2007
Country/Territory	United States
City	Columbia, MD
Period	3/6/07 → 3/8/07

All Science Journal Classification (ASJC) codes

Software

Keywords

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

Access to Document

10.1109/SEW.2007.87

Cite this

@inproceedings{2ddba3dca6f94ef5acace911c47305e4,

title = "A refinement-based framework for computing loop behavior",

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.",

keywords = "Computing loop behavior, Function extraction, Loop functions, Loop invariants, Refinement calculus, Relational calculus",

author = "Ali Mili",

year = "2007",

doi = "10.1109/SEW.2007.87",

language = "English (US)",

isbn = "0769528627",

series = "Proceedings - International Conference on Software Engineering",

pages = "144--153",

booktitle = "31st Annual IEEE Software Engineering Workshop, SEW-31 2007 - Proceedings",

note = "31st Annual IEEE Software Engineering Workshop, SEW-31 2007 ; Conference date: 06-03-2007 Through 08-03-2007",

}

Mili, A 2007, A refinement-based framework for computing loop behavior. in 31st Annual IEEE Software Engineering Workshop, SEW-31 2007 - Proceedings., 4402773, Proceedings - International Conference on Software Engineering, pp. 144-153, 31st Annual IEEE Software Engineering Workshop, SEW-31 2007, Columbia, MD, United States, 3/6/07. https://doi.org/10.1109/SEW.2007.87

TY - GEN

T1 - A refinement-based framework for computing loop behavior

AU - Mili, Ali

PY - 2007

Y1 - 2007

N2 - 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.

AB - 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.

KW - Computing loop behavior

KW - Function extraction

KW - Loop functions

KW - Loop invariants

KW - Refinement calculus

KW - Relational calculus

UR - http://www.scopus.com/inward/record.url?scp=47749156806&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=47749156806&partnerID=8YFLogxK

U2 - 10.1109/SEW.2007.87

DO - 10.1109/SEW.2007.87

M3 - Conference contribution

AN - SCOPUS:47749156806

SN - 0769528627

SN - 9780769528625

T3 - Proceedings - International Conference on Software Engineering

SP - 144

EP - 153

BT - 31st Annual IEEE Software Engineering Workshop, SEW-31 2007 - Proceedings

T2 - 31st Annual IEEE Software Engineering Workshop, SEW-31 2007

Y2 - 6 March 2007 through 8 March 2007

ER -

A refinement-based framework for computing loop behavior

Abstract

Publication series

Other

All Science Journal Classification (ASJC) codes

Keywords

Access to Document

Other files and links

Fingerprint

Cite this