Automated software analysis is the process of testing program source code against a set of conditions. These may be as simple as verifying the coding standards, or as complicated as new languages which are formally verifiable by a theorem solver.
Checker is able to find two small classes of errors, one is memory faults, the other, non-deterministic behaviour. Lacking interprocedural analysis, checker can not be applied to real-world software.
Checker: a Static Program Checker.
Undergraduate Thesis, Computer Science Dept., Ryerson University, June 2006.
@MastersThesis{Lewycky:Checker06,
author = {Nicholas Lewycky},
title = "{Checker: a Static Program Checker}",
school = "{Computer Science Dept., Ryerson University}",
year = {2006},
address = {Toronto, ON},
month = {June},
note = {{\em See {\tt http://wagon.no-ip.org/checker}.}}
}