article

Free access

Catching bugs in the web of program invariants

Authors:

Cormac Flanagan,

Shriram Krishnamurthi,

Stephanie Weirich,

Matthias FelleisenAuthors Info & Claims

ACM SIGPLAN Notices, Volume 31, Issue 5

Pages 23 - 32

https://doi.org/10.1145/249069.231387

Published: 01 May 1996 Publication History

Abstract

MrSpidey is a user-friendly, interactive static debugger for Scheme. A static debugger supplements the standard debugger by analyzing the program and pinpointing those program operations that may cause run-time errors such as dereferencing the null pointer or applying non-functions. The program analysis of MrSpidey computes value set descriptions for each term in the program and constructs a value flow graph connecting the set descriptions. Using the set descriptions, MrSpidey can identify and highlight potentially erroneous program operations, whose cause the programmer can then explore by selectively exposing portions of the value flow graph.

References

[1]

AIKEN, A., WIMMERS, E. L., AND LAKSHMAN, T. K. Soft typing with conditional types. In Proceedings of the A CM Sigplan Conference on Prin. ciples of Programming Languages (1994), pp. 163- 173.

Digital Library

[2]

BOUaDONCLE, F. Abstract debugging of higherorder imperative languages. In Proceedings of the A CM SIGPLAN '93 Conference on Programming Language Design and Implementation (June 1993), pp. 46-55.

Digital Library

[3]

CLINGER, W., AND REES, J. (Eos.). The revised4 report on the algorithmic language scheme. ACM Lisp Pointers 4, 3 (July 1991).

Digital Library

[4]

CooPER, K. D., HALL, M. W., HOOD, R., KENNEDY, K., MCKINLEY, K., MELLOR- CRUMMEY, J., TORCZON, L., AND WARREN, S. The Parascope parallel programming environment. Proceedings of the iEEE (February 1993), 244-263.

[5]

COUSOT, P., AND COUSOT, R. Abstract interpretation: A unified lattice model for static analyses of programs by construction or approximation of fixpoints. In Proceedings of the A CM Sigplan Conference on Principles of Programming Languages (1977), rp-238-252.

Digital Library

[6]

FLANAGAN, C., AND FELLEISEN, M. Set-based analysis for full Scheme and its use in soft-typing. Rice University Computer Science TR95-253.

[7]

FLANAGAN, C., AND FELLEISEN, M. The semantics of future and its use in program optimizations, in Proceedings of the A CM Sigplan Conference on Principles of Programming Languages (1995), PP. 2O9-22O.

Digital Library

[8]

FLATT, M. MrEd: An engine for portable graphical user interfaces. Rice University Computer Science TR-96-258, Rice University.

[9]

G~.cs~.G, F., AND STEINBY, M. Tree Automata. Akad~miai Kind6, Budapest, 1984.

[10]

HEINTZE, N. Set based analysis of arithmetic. Tech. Rep. CMU-CS-93-221, Carnegie Mellon University, December 1993.

Digital Library

[11]

Hr. INTZE, No Set-based analysis of ML programs. In Proceedings of the A CM Conference on Lisp and Functional Programming (1994), pp. 306-317.

Digital Library

[12]

HENGLEIN, F. Dynamic typing: syntax and proof theory. Science of Computer Programming 22 (1994), pp. 197-230.

Digital Library

[13]

HIRANANDANI, S., KENNEDY, K., TSENG, C.- W., AND WARREN, S. The D editor' A new interactive parallel programming tool. In Proceedings of $upercomputing (1994).

Digital Library

[14]

JAGANNATHAN, S., AND WEEKS, S. A unified treatment of flow analysis in higher-order languages. In ~~nd A CM Symposium on Principles of Programming Languages (1995), pp. 393-407.

Digital Library

[15]

JAGANNATUAN, S., AND WRIGUT, A. K. Effective flow analysis for avoiding run-time checks. In Proc. ~nd International Static Analysis Symposium, LNCS 983 (September 1995), Springer- Verlag, pp. 207-224. Preliminary version appears as part of Technical Report DAIMI-PB 493, arhus University, May 1995.

Digital Library

[16]

KENNEDY, K., MCKINLEY, K., AND TSENG, C.- W. Interactive parallel programming using the ParaScope Editor. IEEE Transactions on Parallel and Distributed Systems 2, 3 (July 1991).

Digital Library

[17]

KERNIGHAN, B. W., AND RITCHIE, D. M. The C Programming Language. Prentice-Hall, 1988.

Digital Library

[18]

KRISHNAMURTHI, S. Zodiac: A programming environment builder. Rice University Computer Science TR-96-259, Rice University.

[19]

MALMKJ/gR, K., HEINTZE, N., AND DANVY, O. ML partial evaluation using set-based analysis. Tech. Rep. CMU-CS-94-129, Carnegie Mellon University, 1994.

[20]

MILLER, B., KOSKI, D., LEE, C. P., MAGANTY, V., MURTHY, P., NATARAJAN, A., AND STEIDL, J. Fuzz revisited: A re-examination of the reliability of unix utilities and services. Computer Science Department, University of Wisconsin, 1995.

[21]

MiLNER, R., TOFTr, M., AND HARPER, R. The Definition of Standard ML. The MIT Praa~, Cambridge, Massachusetts and London, England, 1990.

Digital Library

[22]

PLOTKIN, G. D. Call-by-name, call-by-value, and the A-calculus. Theoretical Comput. Sci. 1 (1975), 125-159.

[23]

SHAO, Z., AND APPEL, A. Space-efficient closure representations, in Proceedings of the A CM Symposium on Lisp and Functional Programming (1994), pp. 150-161.

Digital Library

[24]

SHEI, B., AND GANNON, D. Sigmacs: A programmable programming environment. In Advances in Languages and Compilers for Parallel Computing. The MIT Press, August 1990.

[25]

SHIVERS, O. Control-flow Analysis of Higher- Order Languages, or Taming Lambda. PhD thesis, Carnegie-Mellon University, 1991.

Digital Library

[26]

STErANESCU, D., AND ZUOU, Y. An equational framework for the flow analysis of higher order functional programs, in Proceedings of the A CM Conference on Lisp and Functional Programming (1994), pp. 318-327.

Digital Library

[27]

WoLfE, M. J. :The Tiny loop restructuring research tool. In Proceedins of the 1991 International Conference on Parallel Processing (August 1991).

[28]

WRIGHT, A., AND CARTWRiGHT, Ro A practical soft type system for scheme. In Proceedings of the A CM Conference on Lisp and Functional Programming (1994), pp. 250-262.

Digital Library

Cited By

Seidel ESibghat HChaudhuri KWeimer WJhala R(2017)Learning to blame: localizing novice type errors with data-driven diagnosisProceedings of the ACM on Programming Languages10.1145/31388181:OOPSLA(1-27)Online publication date: 12-Oct-2017
https://dl.acm.org/doi/10.1145/3138818
Heinze TMøller AStrocco FIerusalimschy R(2016)Type safety analysis for DartProceedings of the 12th Symposium on Dynamic Languages10.1145/2989225.2989226(1-12)Online publication date: 1-Nov-2016
https://dl.acm.org/doi/10.1145/2989225.2989226
King DJha SMuthukumaran DJaeger TJha SSeshia S(2010)Automating security mediation placementProceedings of the 19th European conference on Programming Languages and Systems10.1007/978-3-642-11957-6_18(327-344)Online publication date: 20-Mar-2010
https://dl.acm.org/doi/10.1007/978-3-642-11957-6_18
Show More Cited By

Index Terms

Catching bugs in the web of program invariants
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Software defect analysis
        Software testing and debugging
  2. Software notations and tools
    1. Development frameworks and environments
    2. General programming languages
      1. Language features
2. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
    2. Program reasoning
      1. Invariants

Recommendations

Catching bugs in the web of program invariants
PLDI '96: Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation

MrSpidey is a user-friendly, interactive static debugger for Scheme. A static debugger supplements the standard debugger by analyzing the program and pinpointing those program operations that may cause run-time errors such as dereferencing the null ...
Symbolic heap abstraction with demand-driven axiomatization of memory invariants
OOPSLA '10

Many relational static analysis techniques for precise reasoning about heap contents perform an explicit case analysis of all possible heaps that can arise. We argue that such precise relational reasoning can be obtained in a more scalable and ...
Program decomposition for pointer aliasing: a step toward practical analyses

Pointer aliasing analysis is crucial to compile-time analyses for languages with general-purpose pointer usage (such as C), but many aliasing methods have proven quite costly. We present a technique that partitions the statements of a program to allow ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 31, Issue 5

May 1996

300 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/249069

Editor:
Richard L. Wexelblat

Issue’s Table of Contents

PLDI '96: Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation
May 1996
300 pages
ISBN:0897917952
DOI:10.1145/231379
Chairman:
Charles N. Fischer
Univ. of Wisconsin, Madison

Copyright © 1996 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 May 1996

Published in SIGPLAN Volume 31, Issue 5

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

65
Total Citations
View Citations
594
Total Downloads

Downloads (Last 12 months)124
Downloads (Last 6 weeks)27

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Seidel ESibghat HChaudhuri KWeimer WJhala R(2017)Learning to blame: localizing novice type errors with data-driven diagnosisProceedings of the ACM on Programming Languages10.1145/31388181:OOPSLA(1-27)Online publication date: 12-Oct-2017
https://dl.acm.org/doi/10.1145/3138818
Heinze TMøller AStrocco FIerusalimschy R(2016)Type safety analysis for DartProceedings of the 12th Symposium on Dynamic Languages10.1145/2989225.2989226(1-12)Online publication date: 1-Nov-2016
https://dl.acm.org/doi/10.1145/2989225.2989226
King DJha SMuthukumaran DJaeger TJha SSeshia S(2010)Automating security mediation placementProceedings of the 19th European conference on Programming Languages and Systems10.1007/978-3-642-11957-6_18(327-344)Online publication date: 20-Mar-2010
https://dl.acm.org/doi/10.1007/978-3-642-11957-6_18
Meunier PFindler RFelleisen M(2006)Modular set-based analysis from contractsACM SIGPLAN Notices10.1145/1111320.111105741:1(218-231)Online publication date: 11-Jan-2006
https://dl.acm.org/doi/10.1145/1111320.1111057
Meunier PFindler RFelleisen MMorrisett GJones S(2006)Modular set-based analysis from contractsConference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/1111037.1111057(218-231)Online publication date: 11-Jan-2006
https://dl.acm.org/doi/10.1145/1111037.1111057
Leino KMillstein TSaxe J(2005)Generating error traces from verification-condition counterexamplesScience of Computer Programming10.1016/j.scico.2004.05.01655:1-3(209-226)Online publication date: 1-Mar-2005
https://dl.acm.org/doi/10.1016/j.scico.2004.05.016
Gast H(2004)Explaining ML type errors by data flowsProceedings of the 16th international conference on Implementation and Application of Functional Languages10.1007/11431664_5(72-89)Online publication date: 8-Sep-2004
https://dl.acm.org/doi/10.1007/11431664_5
Fähndrich MLeino K(2003)Declaring and checking non-null types in an object-oriented languageACM SIGPLAN Notices10.1145/949343.94933238:11(302-312)Online publication date: 26-Oct-2003
https://dl.acm.org/doi/10.1145/949343.949332
Fähndrich MLeino KCrocker RSteele G(2003)Declaring and checking non-null types in an object-oriented languageProceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications10.1145/949305.949332(302-312)Online publication date: 26-Oct-2003
https://dl.acm.org/doi/10.1145/949305.949332
Lencevicius RLencevicius R(2000)ReferencesAdvanced Debugging Methods10.1007/978-1-4419-8774-7_9(145-160)Online publication date: 2000
https://doi.org/10.1007/978-1-4419-8774-7_9
Show More Cited By

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 Issue’s Table of Contents