References

LCLint

[Evans94] David Evans. Using specifications to check source code. MIT/LCS/TR 628, Laboratory for Computer Science, MIT, June 1994.

SM Thesis. Describes research behind LCLint, focusing on how specifications can be exploited to do lightweight checking. Includes case studies using LCLint.

[EGHT94] David Evans, John Guttag, Jim Horning and Yang Meng Tan. LCLint: A tool for using specifications to check code. SIGSOFT Symposium on the Foundations of Software Engineering, December 1994.

Introduction to LCLint. Shows how LCLint is used to find errors in a sample program.

[Evans96] David Evans. Static Detection of Dynamic Memory Errors. In SIGPLAN Conference on Programming Language Design and Implementation (PLDI '96), Philadelphia, PA., May 1996.

Describes approach for exploiting annotations added to code to detect a wide class of errors. Focuses on checks described in Sections 5-7 of this guide.
[Evans00] David Evans. Annotation-Assisted Lightweight Static Checking. In The First International Workshop on Automated Program Analysis, Testing and Verification (ICSE 2000). Feb 25, 2000.
A short position paper describing the research agenda behind LCLint.

Larch

[GH93] Guttag, John V. and Horning, James J., with Stephen J. Garland, Kevin D. Jones, Andrés Modet, and Jeannette M. Wing, Larch: Languages and Tools for Formal Specification, Springer-Verlag, Texts and Monographs in Computer Science, 1993.

Overview of the Larch family of specification languages and related tools. Includes a chapter on LCL, the Larch C interface language, on which LCLint is based.

[Tan95] Tan, Yang Meng. Formal Specification Techniques for Engineering Modular C, Kluwer International Series in Software Engineering, Volume 1, Kluwer Academic Publishers, Boston, 1995.

Modified and updated version of MIT Ph. D. dissertation, previously published as MIT/LCS/TR-619, 1994. Includes presentation of the semantics of LCL and a case study using LCL.

C

[ANSI] American National Standard for Information Systems, Programming Language, C. ANSI X3.159-1989. (Believed to be identical to ISO/IEC 9899:1990).
Specification for C programming language. LCLint aims to be consistent with this document.
[Hat95] Hatton, Les. Safer C: Developing Software for High-integrity and Safety-critical Systems. McGraw-Hill International Series in Software Engineering, 1995.
A broad work on all aspects of developing safety-critical software, focusing on the C language. Provides good justification for the use of C in safety-critical systems, and the necessity of tool-supported programming standards. LCLint users will be interested to see how many of the errors listed as only being dynamically detectable can be detected statically by LCLint.
[KR88] Kernighan, Brian W. and Ritchie, Dennis M. The C Programming Language, second edition. Prentice Hall, New Jersey, 1988.
Standard reference for ANSI C. If you haven't heard of this one, you probably didn't get this far (unless you started at the back).
[vdL94] Van der Linden, Peter. Expert C Programming: Deep C Secrets. SunSoft Press, Prentice Hall, New Jersey, 1994.
Filled with useful information on the darker corners of C, as well as lots of industry anecdotes and humor. LCLint's reserved name checking is loosely based on the list of reserved names in this book.

Abstract Types

[LG86] Liskov, Barbara. and Guttag, John V. Abstraction and Specification in Program Development, MIT Press, Cambridge, MA, 1986.
Describes a programming methodology using abstract types and specified interfaces. Much of the methodology upon which LCLint is based comes from this book. Uses the CLU programming language.
Contents