Splint Related Links

This page collects some of the more interesting links related to Splint and static checking. This page is not updated, and preserved only for historical interest.

Connected Projects

Gasta - Guillaume Thouvenin's GCC AST Analysis Project is working on automatically producing Splint annotations.
Programming the Swarm
Information Survivability for Critical Infrastructure Protection
CS588: Cryptology

Related Research Projects

Alloy Analyzer

MIT's Software Design Group focuses on new kinds of tools: design checkers and error analyzers, among others. The Alloy Analyzer analyzes models written in Alloy.

Assertion Definition Language

Sun's ADL is a formal specification language for C programs. The ADLT tool can be used to automate testing using an ADL specification. They like to make unfounded claims about it being the first ever practical specification language.

AST Toolkit

Daniel Weise's group at Microsoft Research is working on toolkits for analyzing program parse trees. Their AST Toolkit supports some LCLint-derivative checks.

Berkeley Analysis Engine (BANE)

BANE is a toolkit for constructing program analyses such as dataflow and type inference systems developed by Alex Aiken.

Extended Static Checking

Project at DEC Systems Research Center using theorem proving technology to enable extensive static checking in Java and Modula-3.

Cyclone

Cyclone is a safe dialect of C developed by AT&T Labs Research and Greg Morrisett's group at Cornell University.

Open Source Quality Project

Berkeley's project on techniques and tools for assuring software qualify. Focuses on formal verification and theorem proving, model checking, and large-scale software analysis.

Program Analysis and Verification Group

Research group at Stanford University led by David Luckham.

SLAM Project

The Software Productivity Tools Research group at Microsoft Research investigates relationships between Software (Specifications), Languages, Analysis, and Model checking. Their goal is to be able to check that software satisfies critical behavioral properties of the interfaces it uses, and to aid software engineers in designing interfaces and software to ensure reliable and correct functioning.

Vault

Vault is a safe version of the C programming language developed by Microsoft Research's Software Productivity Tools research group. Because of the language restrictions and sophisticated analyses, Vault can enforce many of the properties Splint checks soundly and completely.

Commercial Static Analysis Tools

Some commercial tools have been developed that focus on static checking, some can be used to check for conformance to various standards.

Abraxas's CodeCheck

CenterLine's C++Expert does both compile-time and run-time checking. It incorporates checks based on Scott Meyer's "Effective C++" books.

Gimpel's PC-Lint

Cigital's ITS4 scans code for possible security flaws

Knowledge Software's Open Systems Protability Checker

McCabe & Associates offer a suite of tools and methodology that will assist software developers with software quality assurance, software testing, software reengineering and Year 2000 efforts.

Parasoft's Code Wizard is a source code analysis tool for C++, also based on Scott Meyer's books.

Intrinsa's Software Component Simulation uses simulation to detect software defects. (Note: Intrinsa was bought by Microsoft and seems to have no web presence remaining. The PREfix tool is widely used within Microsoft.)

PolySpace sells a C Verifier that uses abstract interpretation techniques to detect potential run-time errors (including array bounds errors).

Programming Research offers QA/C, a static checking tool including code metrics.

RATS - rough auditing tool for security

Scientific Toolworks produces tools that analyze Ada, C, C++ and FORTRAN source code to reverse engineer and automatically document programms.

Run-Time Checking Tools

Splint hopes to extend the scope of what is checked statically, but there are many types of errors that are still only detectable at run-time. Several commercial and research tools focus on detecting dynamic memory errors are run-time.

Valgrind is an open-source memory debugger for x86 GNU-Linux

CenterLine's C++Expert also does run-time memory checking. Scott Meyer's "Effective C++" books.

Great Circle is a glorified garbage collector.

Immunix StackGuard

Numega's Bounds Checker

Parasoft's Insure++

Rational Software's Purify

The National Physical Laboratory of the United Kingdom offers an ISO C validation service. It uses both static and dynamic checking.

Some other tools are listed at Ben Zorn's Debugging Tools for Dynamic Storage Allocation page

Formal Methods

Larch

MIT Larch Page
Jim Horning's Larch Page

Larch C++

A Larch Interface Language for C++ developed by Gary Leavens and others at Iowa State. Currently there is nothing equivalent to Splint for Larch/C++.

Software Verification mailing list
Formal Methods Page

Secure Programming

Building Secure Software - web site for John Viega and Gary McGraw's book.
Cigital
Common Vulnerabilities and Exposures
Linux Security
Secure Programming for Linux and Unix HOWTO by David A. Wheeler (a freely-available and detailed book on how to write secure programs)
SecurityFocus

Reverse Links

Links to some publications and web pages that reference Splint.

Books

Secure Coding: Principles and Practices, by Mark G. Graff and Kenneth R. van Wyk, O'Reilly, 2003.

David Hanson's book C Interfaces and Implementations advocates a design methodology based on interfaces and implementations very similar to that supported by Splint.

However, if more C programmers read, understood, and imitated this book, the world would be a better and safer place. --- From Richard O'Keefe's review

C Unleashed, by Richard Heathfield, Lawrence Kirby, Mike Lee, Mathew Watson, Ben Pfaff, Dann Corbit, Peter Seebach, Brett Fishburne, Scott Fluhrer, Ian Woods, Sam Hobbs, Ian Kelly

Includes a short section describing running Splint with +strict and +checks on a 3-line program.

Cryptography in C and C++, by Michael Welschenbach, David Kramer

FAQs

C Frequently Asked Questions (also published as a book by Addison-Wesley in 1995) Note the Splint information is out-of-date, but the C FAQ is no longer being updated.

LCLint is also mentioned in its evil twin, the comp.lang.c Infrequently Asked Questions file (unfortunately, the entry for LCLint hasn't been true since before Version 2.0, but I'm counting on them to come up with a more suitable entry in the next edition.)

Linux Frequently Asked Questions

Linux GCC FAQ

Catalog of Free Compilers and Interpreters

Shmoo Group's How to Write Secure Code

David Wheeler's Secure Programming for Linux and Unix HOWTO

Magazine Articles

The German Computer Magazine c't describes Splint in the article Fehlersuche in Java in its 4/2004 issue (full article not available on line, just links).

Linux Journal, The Code Analyser LCLint. By David Santo Orcero, May 2000.
    “Debugging code is never fun, but this tool makes it a bit easier.”

Linux Gazette, Static checking of C programs with LCLint. By Pramode C E and Gopakumar C E. Issue 51, March 2000.
    “LCLint is justifiably angry at such amateurish use of C, but he is gentle in his admonishments.”

The German computer magazine, Ix, includes LCLint in an article, Lint als C-Syntax-Prufer in the July 96 issue.

MATLAB Digest, Checking Code and Models in Production Environments, July 2003. Focuses on checking standard compliance.

Courses

These courses either use Splint (or used LCLint) in a programming lab, or include Splint technical papers. If you know of any other courses that should be listed here, please let me know.

Second Year programming lab at the Imperial College of Science, Technology and Medicine, University of London.
Steve Linton's lectures on Larch at University of St. Andrews, Scotland.
Daniel Jackson's Tractable Representations for Software Development course at Carnegie Mellon.
University of Cincinatti
University of Washington CSE 503 l2D5333 Programverifiering, kursuppl�ggning at the Royal Institute of Technology, Stockholm.
Programmeringsmetodik at Uppsala University in Sweden.
Databehandlingslaboratorium at the University of Oslo.
Richard O'Keefe's Systems Programming 1 course at RMIT University in Melbourne, Australia.

Web Sites

Lysator Programming in C (under Other Sources)
Association of C and C++ Users
Linux Links
Free On-Line Dictionary of Computing
US Department of Agriculture, Information Technology Center
R. Nassif's Programming Page
Modern Web Programming
Sterling Software Archives in programming tools
Ecole Nationale Supirieure de Techniques Avancies, in Unix Programming
Internet Goodies in unix programming
Herbert Dietze's collection of useful programming information

More Links

Search Google for links to lclint.cs.virginia.edu
Search Google for links to www.splint.org
Search Google for mentions of LCLint
Search Google for mentions of Splint

	Splint - Secure Programming Lint [email protected] Download - Documentation - Manual - Links Source - Linux - Publications - Talks Reporting Bugs    Sponsors - Credits