A tool for statically checking C programs.