Author
|
Conference
|
Journal
|
Organization
|
Year
|
DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all domains
Limit my searches in the following domains
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(8)
Formal Method
Program Transformation
Proof of Correctness
Public Key Cryptography
Reverse Engineering
Software Engineering
Software Maintenance
Transform Coding
Related Publications
(1)
Correct Architecture Refinement
Subscribe
Academic
Publications
The Application of Correctness Preserving Transformations to Software Maintenance
Edit
The Application of Correctness Preserving Transformations to Software Maintenance
(
Citations: 4
)
BibTex
|
RIS
|
RefWorks
Download
J. Paul Gibson
,
Thomas F. Dowling
,
Brian A. Malloy
The size and complexity of hardware and soft- ware systems continues to grow, making the introduction of subtle errors a more likely possibility. A major goal of soft- ware engineering is to enable developers to construct sys- tems that operate reliably despite increased size and com- plexity. One approach to achieving this goal is through for- mal methods: mathematically based languages, techniques and tools for specifying and verifying complex software sys- tems. In this paper, we apply a theoretical tool that is sup- ported by many formal methods, the correctness preserving transformation (CPT), to a real
software engineering
prob- lem: the need for optimization during the maintenance of code. We present four program transformations and a model that forms a framework for proof of correctness. We prove the transformations correct and then apply them to a cryp- tography application implemented in CS+. Our experience shows that CPTs can facilitate generation of more efficient code while guaranteeing the preservation of original behav- ior. Keywords- Reverse engineering, formal methods,
public key
cryptography, correctness preserving transformation, code optimization.
Conference:
International Conference on Software Maintenance - ICSM
, pp. 108-117, 2000
DOI:
10.1109/ICSM.2000.883025
Cumulative
Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
(
computer.org
)
(
www.informatik.uni-trier.de
)
(
ieeexplore.ieee.org
)
(
www-public.int-evry.fr
)
(
ieeexplore.ieee.org
)
More »
Citation Context
(4)
...Nevertheless, approaches based on formal methods rely on formal proofs as evidence for transformation conformance [see, e.g., “correct architectural refinement” in Moriconi et al. (1995), and “correctness preserving transformations” in Bolognesi et al. (1995);
Gibson et al. (2000)
]...
João Paulo A. Almeida
,
et al.
Requirements traceability in model-driven development: Applying model ...
...Nevertheless, approaches based on formal methods rely on formal proofs as evidence for transformation conformance (see, e.g., “correct architectural refinement” in [20], and “correctness preserving transformations” in [9,
14
])...
João Paulo A. Almeida
,
et al.
Requirements Traceability and Transformation Conformance in Model-Driv...
...We refer to such a transformation as a correctness preserving transformation, or CPT [
16
]...
Edward B. Duffy
,
et al.
Applying the Decorator Pattern for Profiling Object-Oriented Software
...While this transformational approach parallels well-recognized software engineering strategies, it has the additional benet of providing a framework for formal verication[
4
]...
James F. Power
,
et al.
Exploiting metrics to facilitate grammar transformation into LALR form...
References
(19)
Algebraic Specification Techniques in Object Oriented Programming Environments
(
Citations: 42
)
Ruth Breu
Published in 1991.
On understanding types, data abstraction, and polymorphism
(
Citations: 1123
)
Luca Cardelli
,
Peter Wegner
Journal:
ACM Computing Surveys - CSUR
, vol. 17, no. 4, pp. 471-523, 1985
The calculi of lambda-conversion
(
Citations: 344
)
Alonzo Church
Published in 1985.
Formal methods: state of the art and future directions
(
Citations: 637
)
Edmund M. Clarke
,
Jeannette M. Wing
Journal:
ACM Computing Surveys - CSUR
, vol. 28, no. 4, pp. 626-643, 1996
Type theories and object-oriented programmimg
(
Citations: 69
)
Scott Danforth
,
Chris Tomlinson
Journal:
ACM Computing Surveys - CSUR
, vol. 20, no. 1, pp. 29-72, 1988
Order by:
Citations
(4)
Requirements traceability in model-driven development: Applying model and transformation conformance
(
Citations: 1
)
João Paulo A. Almeida
,
Maria-eugenia Iacob
,
Pascal Van Eck
Journal:
Information Systems Frontiers - ISF
, vol. 9, no. 4, pp. 327-342, 2007
Requirements Traceability and Transformation Conformance in Model-Driven Development
(
Citations: 6
)
João Paulo A. Almeida
,
Pascal Van Eck
,
Maria-eugenia Iacob
Conference:
Enterprise Distributed Object Computing Conference - EDOS
, pp. 355-366, 2006
Applying the Decorator Pattern for Profiling Object-Oriented Software
(
Citations: 3
)
Edward B. Duffy
,
J. Paul Gibson
,
Brian A. Malloy
Conference:
International Conference on Program Comprehension - ICPC
, pp. 84-93, 2003
Exploiting metrics to facilitate grammar transformation into LALR format
(
Citations: 4
)
James F. Power
,
Brian A. Malloy
Conference:
ACM Symposium on Applied Computing - SAC
, pp. 636-640, 2001