Splint - Secure Programming Lint
|Download - Documentation - Manual - Links||Reporting Bugs - Mailing Lists Sponsors - Credits|
db: Employee Database Program
Splint ExamplesStarts 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 AnalysisDavid 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 ErrorsDavid Evans. In SIGPLAN Conference on Programming Language Design and Implementation (PLDI '96), Philadelphia, PA, May 1996.
LCLint: A Tool for Using Specifications to Check CodeDavid Evans, John Guttag, Jim Horning and Yang Meng Tan, SIGSOFT Symposium on the Foundations of Software Engineering, December 1994.
Using Specifications to Check Source CodeDavid Evans, MIT/LCS/TR-628, June 1994, SM Thesis.