SATABS is a verification tool for ANSI-C and C++ programs. It allows verifying array bounds (buffer overflows), pointer safety, exceptions and user-specified assertions. Furthermore, it can check ANSI-C and C++ for consistency with other languages, such as Verilog. SATABS computes an abstraction of the program in order to handle large amounts of code. SATABS home page