Splint - Secure Programming Lint
[email protected]
Download - Documentation - Manual - Links Reporting Bugs - Mailing Lists      Sponsors - Credits

Splint Examples

db: Employee Database Program
Starts with a fully specified, complete implementation. Uses LCLint to detect some bugs in the code, detect errors in the specifications, improve the specifications, and adopt and check conformance to a naming convention.
Splint's own source code, of course, is annotated and checked using Splint. [Download Code]

For more examples using Splint, see:

Improving Security Using Extensible Lightweight Static Analysis
David Evans and David Larochelle. In IEEE Software, Jan/Feb 2002. (PDF, 12 pages)

Statically Detecting Likely Buffer Overflow Vulnerabilities
David Larochelle and David Evans. In 2001 USENIX Security Symposium, Washington, D. C., August 13-17, 2001. (PDF, HTML, 13 pages)
Static Detection of Dynamic Memory Errors
David Evans. In SIGPLAN Conference on Programming Language Design and Implementation (PLDI '96), Philadelphia, PA, May 1996.

LCLint: A Tool for Using Specifications to Check Code

David Evans, John Guttag, Jim Horning and Yang Meng Tan, SIGSOFT Symposium on the Foundations of Software Engineering, December 1994.

Using Specifications to Check Source Code

David Evans, MIT/LCS/TR-628, June 1994, SM Thesis.
Splint - Secure Programming Lint [email protected]
Download - Documentation - Manual - Links
Source - Linux - Publications - Talks
Reporting Bugs    Sponsors - Credits