Article

Free access

Pragmatic techniques for program analysis and verification

Author:

Erhard PloederederAuthors Info & Claims

ICSE '79: Proceedings of the 4th international conference on Software engineering

Pages 63 - 72

Published: 17 September 1979 Publication History

Abstract

The Program Development System (PDS) is a collection of programming tools created as an extension of the ECL programming system²³. It contains components that assist the programmer in the definition and modular structuring of large programs at different levels of algorithmic abstraction. These components are supplemented by a program analysis package that produces an information pool to be used for such tasks as source-to-source optimization, semi-automated program documentation, fault detection and program verification.

This paper describes the core of the analyzing package, the Symbolic Evaluator. In its implementation we have incorporated pragmatic methods for handling data sharing patterns, and for characterizing and reasoning about the behaviour of loops and procedures.

The impact of these methods upon program verification techniques is briefly discussed.

References

[1]

Balzer, Robert and Neil Goldman, "Principles of good software specification and their implications for specification languages", USC/Information Sciences Institute, undated.

[2]

Bauer, F.L., "Programming as an evolutionary process", Proc. of the Second Conference on Software Engineering, San Francisco, 1976.

Digital Library

[3]

Bauer, F.L., "'Variables considered harmful' und andere Bemerkungen zur Programmierung", Technische Universitaet Muenchen, Report Nr. 7519, Munich, undated.

[4]

Boyer, R.S., B. Elspas, and K.N. Levitt, "SELECT - A formal system for testing and debugging programs by symbolic execution", Proc. of the Int. Conference on Reliable Software, Los Angeles, Calif., April 1975.

Digital Library

[5]

Cartwright, Robert, and Derek Oppen, "Unrestricted procedure calls in Hoare's logic", Proc. of the Fifth Annual ACM Symposium on Principles of Programming Languages, Tueson, January 1978.

Digital Library

[6]

Cheatham, T.E., Jr., and Judy A. Townley, "Symbolic evaluation of programs—A look at loop analysis", Proc. of the ACM Symposium on Symbolic and Algebraic Computation, August 1976.

Digital Library

[7]

Cheatham, T.E., Jr., and Deborah B. Washington, "Program loop analysis by solving first order recurrence relations", Center for Research in Computing Technology, Harvard University, TR-13-78, May 1978.

[8]

Cheatham, T.E., Jr., G.H. Holloway, and Judy A. Townley, "Symbolic evaluation and the analysis of programs", Center for Research in Computing Technology, Harvard University, TR-19-78, November 1978; to appear in IEEE Transactions on Software Engineering.

[9]

Cheatham, T.E., Jr., Glenn H. Holloway and Judy A. Townley, "A system for program refinement", Proc. of the Forth International Conference on Software Engineering, Munich, Germany, September 17-19, 1979.

Digital Library

[10]

Clarke, L., "A system to generate test data and symbolically execute programs", Dept. of Computer Science, University of Colorado, Boulder, Colo., Technical Report, CU-CS-060-75, February 1975.

[11]

Conrad, W.R., "Rewrite user's guide", Center for Research in Computing Technology, Harvard University, Memo, August 1976.

[12]

Dahl, O.J., E. Dijkstra, and C.A.R. Hoare, "Structured Programming", Academic Press, New York, 1972.

Digital Library

[13]

Dijkstra, E.W., "A Discipline of Programming", Prentice Hall, Englewood Cliffs, 1976.

Digital Library

[14]

Elspas, B., "The semiautomatic generation of inductive assertions for proving program correctness", Research Report, SRI, Menlo Park, California, July 1974.

[15]

Good, D.I., R.L. London, and W.W. Bledsoe, "An interactive program verification system", IEEE Transactions on Software Engineering, Vol. SE-1, No. 1, March 1975.

Digital Library

[16]

Guttag, J.V., E. Horowitz, and D.R. Musser, "Abstract data types and software validation", CACM, Vol. 21, No. 12, December 1978.

Digital Library

[17]

Hantler, S.L., and King, J.C., "An introduction to proving the correctness of programs", Computing Surveys, Vol. 8, No. 3, September 1976.

Digital Library

[18]

Horning, J.J., "A case study in language design: Euclid", International Summer School on Program Construction, Munich-Marktoberdorf Germany, July 26 - August 6, 1978.

Digital Library

[19]

Howden, W.E., "Symbolic testing and the DISSECT symbolic evaluation system", IEEE Transactions on Software Engineering, Vol. SE-3, No. 4, July 1977.

Digital Library

[20]

Igarashi, S., R.L. London, and D.C. Luckham, "Automatic program verification I: A logical basis and its implementation", Acta Informatica, Vol. 4, No. 2, 1975.

Digital Library

[21]

King, J.C., "Symbolic execution and program testing", CACM, Vol. 19, No. 7, July 1976.

Digital Library

[22]

Liskov, B. and S. Zilles, "Programming with abstract data types", Proc. of the ACM SIGPLAN Conference on Very High Level Languages, SIGPLAN Notices, Vol. 9, No. 4, April 1974

Digital Library

[23]

"ECL programmer's manual", Center for Research in Computing Technology, Harvard University, TR-23-74, December 1974.

[24]

Parnas, D.L., "A technique for software module specification with examples", CACM, Vol. 15, No. 5, May 1972.

Digital Library

[25]

Ploedereder, Erhard O.J., "Symbolic evaluation of user-defined procedures in EL1", Center for Research in Computing Technology, Harvard University, TR-01-79, February 1979.

[26]

Shaw, M., and Wulf, W.A., "Global variables considered harmful", SIGPLAN Notices, Vol. 8, No. 2, February 1973.

Digital Library

[27]

Suzuki, N., "Automatic verification of programs with complex data structures", Ph.D. thesis, STAN-CS-76-552, Computer Science Department, Stanford University, February 1976.

Digital Library

[28]

Townley, Judy A., "A symbolic interpreter for EL1", Center for Research in Computing Technology, Harvard University, Memo, November 1976.

[29]

Townley, Judy A., "An incremental approach to resolution-based theorem proving", Center for Research in Computing Technology, Harvard University, TR-15-78, August 1978.

[30]

Townley, Judy A., "Program analysis techniques for software reliability", Proc. of the ACM Workshop on Reliable Software, Bonn University, September 1978.

[31]

Townley, Judy A., "The analysis of pointers in programs", Center for Research in Computing Technology, Harvard University, Memo, in preparation.

[32]

Wirth, N., "Systematisches Programmieren", Teubner, Stuttgart, 1975.

[33]

Wirth, N., "Modula: A language for modular multiprogramming", Software—Practice and Engineering, 7, 1977.

[34]

Wulf, W.A., "ALPHARD: Toward a language to support structured programs", Computer Science Department, Carnegie-Mellon University, April 1974

Cited By

Ryder BWiedermann B(2012)Language design and analyzabilitySoftware—Practice & Experience10.1002/spe.113342:1(3-18)Online publication date: 1-Jan-2012
https://dl.acm.org/doi/10.1002/spe.1133
Cheatham TTownley JHolloway GBauer FStucki LLehman M(1979)A system for program refinementProceedings of the 4th international conference on Software engineering10.5555/800091.802922(53-62)Online publication date: 17-Sep-1979
https://dl.acm.org/doi/10.5555/800091.802922

Index Terms

Pragmatic techniques for program analysis and verification

Recommendations

Guidebook for Teachers for the Basic Preprimer Programme: To Accompany Skip Along and Open the Door
Temporal property verification as a program analysis task

We describe a reduction from temporal property verification to a program analysis problem. First we present a proof system that, unlike the standard formulation, is more amenable to reasoning about infinite-state systems: disjunction is treated by ...
Formal Verification for C Program

Iterative abstraction refinement has emerged in the last few years as the leading approach to software model checking. We present an approach for automatically verifying C programs against safety specifications based on finite state machine. The ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICSE '79: Proceedings of the 4th international conference on Software engineering

September 1979

466 pages

Sponsors

ACM: Association for Computing Machinery
GMD: German Natl Research Ctr for Information Tech. - Gesellschft
IEEE-CS: Computer Society
ERO: ERO

Publisher

IEEE Press

Publication History

Published: 17 September 1979

Check for updates

Qualifiers

Article

Acceptance Rates

Overall Acceptance Rate 276 of 1,856 submissions, 15%

Upcoming Conference

ICSE 2025

2025 IEEE/ACM 46th International Conference on Software Engineering

April 26 - May 3, 2025

Ottawa , ON , Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
313
Total Downloads

Downloads (Last 12 months)48
Downloads (Last 6 weeks)10

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ryder BWiedermann B(2012)Language design and analyzabilitySoftware—Practice & Experience10.1002/spe.113342:1(3-18)Online publication date: 1-Jan-2012
https://dl.acm.org/doi/10.1002/spe.1133
Cheatham TTownley JHolloway GBauer FStucki LLehman M(1979)A system for program refinementProceedings of the 4th international conference on Software engineering10.5555/800091.802922(53-62)Online publication date: 17-Sep-1979
https://dl.acm.org/doi/10.5555/800091.802922

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents