research-article

Software Specialization Via Symbolic Execution

Authors:

Alberto Coen-Porisini,

Flavio De Paoli,

Carlo Ghezzi,

Dino MandrioliAuthors Info & Claims

IEEE Transactions on Software Engineering, Volume 17, Issue 9

Pages 884 - 899

https://doi.org/10.1109/32.92907

Published: 01 September 1991 Publication History

Publisher Site

Abstract

A technique and an environment-supporting specialization of generalized software components are described. The technique is based on symbolic execution. It allows one to transform a generalized software component into a more specific and more efficient component. Specialization is proposed as a technique that improves software reuse. The idea is that a library of generalized components exists and the environment supports a designer in customizing a generalized component when the need arises for reusing it under more restricted conditions. It is also justified as a reengineering technique that helps optimize a program during maintenance. Specialization is supported by an interactive environment that provides several transformation tools: a symbolic executor/simplifier, an optimizer, and a loop refolder. The conceptual basis for these transformation techniques is described, examples of their application are given, and how they cooperate in a prototype environment for the Ada programming language is outlined.

References

[1]

{1} A.V. Aho, R. Sethi, and J.D. Ullman, Compilers: Principles, Techniques, and Tools. Reading, MA: Addison-Wesley, 1986.]]

Digital Library

Google Scholar

[2]

{2} H. Alblas, "One pass transformation of attributed program trees," Acta Inform., vol. 24, no. 3, pp. 299-352, 1987.]]

Digital Library

Google Scholar

[3]

{3} V. Ambriola, F. Giannotti, D. Pedreschi, and F. Turini, "Symbolic semantics and program reduction," IEEE Trans. Software Eng., vol. SE- 11, pp. 784-794, 1985.]]

Digital Library

Google Scholar

[4]

{4} L. A. Belady and M. M. Lehman, Program Evolution. New York: Academic, 1985.]]

Google Scholar

[5]

{5} T. J. Biggerstaff and A. J. Perlis, Software Reusability, vols. 1-2. New York: ACM Press, 1989.]]

Crossref

Google Scholar

[6]

{6} W. W. Bledsoe, "The Sup-Inf method in Presburger arithmetic," Dept. Mathematics, Univ. Texas, Tech. Rep., 1974.]]

Google Scholar

[7]

{7} A. Bossi, N. Cocco, and S. Dulli, "A method for specializing logic programs," ACM Trans. Programming Languages and Systems, vol. 12, no. 2, pp. 253-302, 1990.]]

Digital Library

Google Scholar

[8]

{8} L.A. Clarke and D. J. Richardson, "Symbolic evaluations methods-implementations and applications," in Computer Program Testing, B. Chandrasekaran and S. Radicchi, Eds. Amsterdam: North-Holland, 1981, pp. 65-102.]]

Google Scholar

[9]

{9} A. Coen-Porisini and F. DePaoli, "Array representation in symbolic execution," Politecnico di Milano, Dipartimento di Elettronica, Tech. Rep. 90.031, 1990, submitted for publication.]]

Google Scholar

[10]

{10} A. Coen-Porisini and F. DePaoli, "Symbad: a symbolic executor for sequential Ada programs," in Proc. Int. Conf. Safety Security and Reliability Related Computers for the 1990's-SAFECOMP '90 (London), 1990, pp. 105-111.]]

Crossref

Google Scholar

[11]

{11} A. Coen-Porisini and F. DePaoli, "SESADA: an environment supporting software specialization," to be presented at 3rd European Software Eng. Conf. (ESEC '91), Milano, 1991.]]

Digital Library

Google Scholar

[12]

{12} A. P. Ershov, "On the partial computation principle," Inform. Process. Lett., vol. 6, no. 2, pp. 38-45, 1977.]]

Crossref

Google Scholar

[13]

{13} A. P. Ershov, "Mixed computation: Potential applications and problems for study," Theoretical Computer Sci., vol. 18, pp. 41-67, 1982.]]

Crossref

Google Scholar

[14]

{14} S. Ghelfo and G. Levi, "A partial evaluator for metaprograms in a multiple theories logic language," Tech. Rep. ESPRIT-Project Epsilon, 1986.]]

Google Scholar

[15]

{15} S. Ghelfo, G. Levi, and G. Sardú, "Un valutatore parziale per metaprogrammi in un linguaggio logico con teorie multiple," in Atti del convegno GULP 1987, May 1987, pp. 13-24.]]

Google Scholar

[16]

{16} C. Ghezzi, D. Mandrioli, and A. Tecchio, "Program simplification via symbolic execution," Lecture Notes in Computer Science, no. 206, pp. 116-128, 1985.]]

Digital Library

Google Scholar

[17]

{17} R. Gordon, The Denotational Description of Programming Languages. New York: Springer-Verlag, 1975.]]

Digital Library

Google Scholar

[18]

{18} "Maintenance and reverse engineering and design recovery," IEEE Software, vol. 7, no. 1, 1990.]]

Digital Library

Google Scholar

[19]

{19} N. D. Jones, P. Sestoft, and H. Sonderaard, "An experiment in partial evaluation: the generation of a compiler generator," in Int. Conf. Rewriting Techniques and Applications. New York: Springer-Verlag, 1985.]]

Digital Library

Google Scholar

[20]

{20} R. Kemmerer and S. Eckmann, "UNISEX: a UNIX-based Symbolic Executor for Pascal," Software-Practice and Experience, vol. 15, no. 5, pp. 439-457, 1985.]]

Crossref

Google Scholar

[21]

{21} J. C. King, "Symbolic execution and program testing," Commun. ACM, vol. 19, no. 7, pp. 385-394, 1976.]]

Digital Library

Google Scholar

[22]

{22} D. L. Parnas, "On the criteria to be used in decomposing systems into modules," Commun. ACM, vol. 15, no. 12, pp. 1053-1058, 1972.]]

Digital Library

Google Scholar

[23]

{23} D.L. Parnas, "On the design and development of program families," IEEE Trans. Software Eng., vol. SE-2, no. 1, pp. 1-9, 1976.]]

Digital Library

Google Scholar

[24]

{24} D. L. Parnas, "Designing software for ease of extension and contraction," IEEE Trans. Software Eng., vol. SE-5, no. 2, pp. 128-137, 1979.]]

Digital Library

Google Scholar

[25]

{25} H. Partsch and R. Steinbruggen, "Program transformation systems," Computing Surveys, vol. 15, no. 3, pp. 199-236, 1983.]]

Digital Library

Google Scholar

[26]

{26} J. E. Stoy, Denorational Semantics: the Scott-Strachey approach to Programming Language Theory. Cambridge, MA: MIT Press, 1977.]]

Digital Library

Google Scholar

[27]

{27} V. F. Turchin, "The concept of a supercompiler," ACM Trans. Programming Languages and Systems, vol. 8, no. 3, pp. 292-325, 1986.]]

Digital Library

Google Scholar

[28]

{28} Reference Manual for the Ada Programming Language, US-DOD, ANSI/MIL-STD-1815 A., 1983.]]

Digital Library

Google Scholar

[29]

{29} M. Young and R.N. Taylor, "Rethinking the taxonomy of fault detection techniques," in Proc. 11th Int. Conf. Software Eng. Los Alamitos, CA: IEEE Computer Soc., 1989, pp. 53-62.]]

Digital Library

Google Scholar

Cited By

View all

Luinaud TLanglois JSavaria Y(2022)Symbolic Analysis for Data Plane Programs SpecializationACM Transactions on Architecture and Code Optimization10.1145/355772720:1(1-21)Online publication date: 17-Nov-2022
https://dl.acm.org/doi/10.1145/3557727
Kültürsay EEbcioğlu KKüçük GKandemir M(2016)Memory Partitioning in the LimitInternational Journal of Parallel Programming10.1007/s10766-015-0380-744:2(337-380)Online publication date: 1-Apr-2016
https://dl.acm.org/doi/10.1007/s10766-015-0380-7
Balasubramanian DPăsăreanu CWhalen MKarasi GLowry M(2012)Improving symbolic execution for statechart formalismsProceedings of the Workshop on Model-Driven Engineering, Verification and Validation10.1145/2427376.2427385(47-52)Online publication date: 1-Oct-2012
https://dl.acm.org/doi/10.1145/2427376.2427385
Show More Cited By

Index Terms

Software Specialization Via Symbolic Execution
1. Software and its engineering
  1. Software creation and management
    1. Software development techniques
      1. Reusability
  2. Software notations and tools
    1. Development frameworks and environments

Recommendations

Towards reengineering in reuse reengineering processes
ICSM '95: Proceedings of the International Conference on Software Maintenance

Reuse of existing software has been regarded in recent years as a feasible solution to software quality and productivity improvement problems. Various reference paradigms for setting up a reuse reengineering process have been proposed. With reference to ...
Supporting reuse and configuration for large scale software process models
ISPW '96: Proceedings of the 10th International Software Process Workshop

A software process is a set of activities that will be carried out over time to produce a software system. Research on the software process has been increasingly recognized. This position advocates the representation of a software development process ...
Automating Output Size and Reuse Metrics in a Repository-Based Computer-Aided Software Engineering (CASE) Environment

Measurement of software development productivity is needed in order to control software costs, but it is discouragingly labor-intensive and expensive. Computer-aided software engineering (CASE) technologies/spl minus/especially repository-based, ...

Reviews

Reviewer: Michael Marcotty

The authors make a contribution to software reusability through the use of program transformation tools. The idea is, given the specification and implementation for a software component or an entire program, to help restructure the implementation through a technique called specialization. When a software module with a particular functionality is needed, a library of reusable modules of generalized functionality is searched for a suitable module. In general, candidate modules will require some transformation. For example, their functionalities must be restricted in order to improve efficiency, that is, they must be specialized for a particular application. Suppose that the generalized module P is a function mapping its domain D P to its range R P and that the desired module M will have the same functionality as P but with a domain D M ?D P , then the aim of the specialization will be to transform P into a P ? that is more efficient than P . For example, if P contains the statement “if C then S 1 else S 2 ,<__?__Pub Caret>” and D M ?D P implies that C is always true, the statement may be transformed into S 1 . In this paper, the authors discuss specialization through symbolic execution. The paper describes the process of symbolic execution and simplification used for the specialization of a program; this process is defined formally using denotational semantics. Other specialization steps such as loop refolding and the application of conventional source-level optimization techniques are described. A complete specialization environment for Ada programs and a complete example are also presented. Finally, the authors assess the work and discuss further developments and applications, particularly in the area of object-oriented languages.

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image IEEE Transactions on Software Engineering

IEEE Transactions on Software Engineering Volume 17, Issue 9

September 1991

130 pages

ISSN:0098-5589

Editor:
Victor R. Basili
Univ. of Maryland, College Park

Issue’s Table of Contents

Publisher

IEEE Press

Publication History

Published: 01 September 1991

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 18 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Luinaud TLanglois JSavaria Y(2022)Symbolic Analysis for Data Plane Programs SpecializationACM Transactions on Architecture and Code Optimization10.1145/355772720:1(1-21)Online publication date: 17-Nov-2022
Kültürsay EEbcioğlu KKüçük GKandemir M(2016)Memory Partitioning in the LimitInternational Journal of Parallel Programming10.1007/s10766-015-0380-744:2(337-380)Online publication date: 1-Apr-2016
Balasubramanian DPăsăreanu CWhalen MKarasi GLowry M(2012)Improving symbolic execution for statechart formalismsProceedings of the Workshop on Model-Driven Engineering, Verification and Validation10.1145/2427376.2427385(47-52)Online publication date: 1-Oct-2012
Danicic SDaoudi MFox CHarman MHierons RHowroyd JOurabya LWard M(2005)ConSUSJournal of Systems and Software10.1016/j.jss.2004.03.03477:3(241-262)Online publication date: 1-Sep-2005
Fahringer TScholz B(2003)Advanced symbolic analysis for compilersundefinedOnline publication date: 1-Jan-2003
Jin YJin C(2002)Constraint-based partial evaluation for imperative languagesJournal of Computer Science and Technology10.1007/BF0294982617:1(64-72)Online publication date: 1-Jan-2002
Coen-Porisini ADenaro GGhezzi CPezzé M(2001)Using symbolic execution for verifying safety-critical systemsACM SIGSOFT Software Engineering Notes10.1145/503271.50323026:5(142-151)Online publication date: 1-Sep-2001
Coen-Porisini ADenaro GGhezzi CPezzé MTjoa AGruhn V(2001)Using symbolic execution for verifying safety-critical systemsProceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering10.1145/503209.503230(142-151)Online publication date: 10-Sep-2001
Buy UOrso APezze M(2000)Automated Testing of ClassesACM SIGSOFT Software Engineering Notes10.1145/347636.34887025:5(39-48)Online publication date: 1-Aug-2000
Buy UOrso APezze MRichardson D(2000)Automated Testing of ClassesProceedings of the 2000 ACM SIGSOFT international symposium on Software testing and analysis10.1145/347324.348870(39-48)Online publication date: 1-Aug-2000
Show More Cited By

Abstract

References

Cited By

Index Terms

Recommendations

Towards reengineering in reuse reengineering processes

Supporting reuse and configuration for large scale software process models

Automating Output Size and Reuse Metrics in a Repository-Based Computer-Aided Software Engineering (CASE) Environment

Reviews

Access critical reviews of Computing literature here

Comments

Information

Published In

Publisher

Publication History

Author Tags

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations