|
 ABSTRACT
Many important classes of bugs result from invalid assumptions about the results of functions and the values of parameters and global variables. Using traditional methods, these bugs cannot be detected efficiently at compile-time, since detailed cross-procedural analyses would be required to determine the relevant assumptions. In this work, we introduce annotations to make certain assumptions explicit at interface points. An efficient static checking tool that exploits these annotations can detect a broad class of errors including misuses of null pointers, uses of dead storage, memory leaks, and dangerous aliasing. This technique has been used successfully to fix memory management problems in a large program.
REFERENCES
Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.
| |
1
|
|
| |
2
|
|
| |
3
|
David Evans. LCLint User's Guide, Version 2.0. February 1996. (http ://larch-www. lcs.mit.edu:8001/!arch/!clint/guideO
|
 |
4
|
David Evans , John Guttag , James Horning , Yang Meng Tan, LCLint: a tool for using specifications to check code, Proceedings of the 2nd ACM SIGSOFT symposium on Foundations of software engineering, p.87-96, December 06-09, 1994, New Orleans, Louisiana, United States
|
| |
5
|
|
| |
6
|
Laurie J. Hendren , Joseph Hummell , Alexandru Nicolau, Abstractions for recursive pointer data structures: improving the analysis and transformation of imperative programs, Proceedings of the ACM SIGPLAN 1992 conference on Programming language design and implementation, p.249-260, June 15-19, 1992, San Francisco, California, United States
|
| |
7
|
Posting in comp. os. linux, August 1994.
|
| |
8
|
Robert Strom and Nagui Halim. A new programming methodology for long-lived software systems. IBM-RC 9979, IBM T J. Watson Research Center, March 1983.
|
| |
9
|
Yang Meng Tan. Formal Specification Techniques for Promoting Software Modularity, Enhancing Software Documentation, and Testing Specifications, MIT/LCS/TR-619, MIT Laboratory for Computer Science, June 1994.
|
| |
10
|
Gray Watson. Debug Malloc Library, November 1994. (ftp ://ftp.letters.com/src/dmalloc/docs/dma!loc. ps)
|
| |
11
|
Benjamin Zorn and Paul Hilfinger. A memory allocation profiler for C and Lisp programs. (ffp'J/gatokoopor. dec.com:/pbu/mise/mprof-3.0.tar. Z)
|
CITED BY 69
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Michael D. Ernst , Jake Cockrell , William G. Griswold , David Notkin, Dynamically discovering likely program invariants to support program evolution, Proceedings of the 21st international conference on Software engineering, p.213-224, May 16-22, 1999, Los Angeles, California, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Darrell Reimer , Edith Schonberg , Kavitha Srinivas , Harini Srinivasan , Julian Dolby , Aaron Kershenbaum , Larry Koved, Validating structural properties of nested objects, Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 24-28, 2004, Vancouver, BC, CANADA
|
|
|
|
|
|
Darrell Reimer , Edith Schonberg , Kavitha Srinivas , Harini Srinivasan , Bowen Alpern , Robert D. Johnson , Aaron Kershenbaum , Larry Koved, SABER: smart analysis based error reduction, ACM SIGSOFT Software Engineering Notes, v.29 n.4, July 2004
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
John Penix , Willem Visser , Seungjoon Park , Corina Pasareanu , Eric Engstrom , Aaron Larson , Nicholas Weininger, Verifying Time Partitioning in the DEOS Scheduling Kernel, Formal Methods in System Design, v.26 n.2, p.103-135, March 2005
|
|
|
Jinlin Yang , David Evans , Deepali Bhardwaj , Thirumalesh Bhat , Manuvir Das, Perracotta: mining temporal API rules from imperfect traces, Proceeding of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China
|
|
|
|
|
|
|
|
|
|
|
|
Gary T. Leavens , Jean-Raymond Abrial , Don Batory , Michael Butler , Alessandro Coglio , Kathi Fisler , Eric Hehner , Cliff Jones , Dale Miller , Simon Peyton-Jones , Murali Sitaraman , Douglas R. Smith , Aaron Stump, Roadmap for enhanced languages and methods to aid verification, Proceedings of the 5th international conference on Generative programming and component engineering, October 22-26, 2006, Portland, Oregon, USA
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
David Hovemeyer , William Pugh, Finding more null pointer bugs, but not too many, Proceedings of the 7th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.9-14, June 13-14, 2007, San Diego, California, USA
|
|
|
|
|
|
|
|
|
|
|
|
Umesh Shankar , Kunal Talwar , Jeffrey S. Foster , David Wagner, Detecting format string vulnerabilities with type qaualifiers, Proceedings of the 10th conference on USENIX Security Symposium, p.16-16, August 13-17, 2001, Washington, D.C.
|
|
|
Trevor Jim , J. Greg Morrisett , Dan Grossman , Michael W. Hicks , James Cheney , Yanling Wang, Cyclone: A Safe Dialect of C, Proceedings of the General Track: 2002 USENIX Annual Technical Conference, p.275-288, June 10-15, 2002
|
|
|
|
|
|
|
|
|
Umesh Shankar , Kunal Talwar , Jeffrey S. Foster , David Wagner, Detecting format string vulnerabilities with type qualifiers, Proceedings of the 10th conference on USENIX Security Symposium, p.16-16, August 13-17, 2001, Washington, D.C.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Saurabh Sinha , Hina Shah , Carsten Görg , Shujuan Jiang , Mijung Kim , Mary Jean Harrold, Fault localization and repair for Java runtime exceptions, Proceedings of the eighteenth international symposium on Software testing and analysis, July 19-23, 2009, Chicago, IL, USA
|
|
|
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf
D.2