Our core technology is based on abstract interpretation, a mathematical theory developed by Cousot and Cousot for sound static static analysis. Although very powerful, the theory has been found difficult to put into practice, resulting in few practical tools available. Over the past fifteen years we have succeeded in creating an abstract interpretation engine that supports sound static analysis of programs of hundreds of thousands of lines of code.
Our CodeHawk abstract interpretation engine includes very efficient iterators, and several abstract domains, including
- strided intervals
- linear equalities
- symbolic sets
- value sets, and
The CodeHawk Abstract Interpretation Engine has its own internal language, called CHIF (CodeHawk Internal Form) that provides an expressive, general representation of programs. This design enables CodeHawk to accommodate a number of different front-ends from different input languages. We currently offer front-ends for C, Java byte code, and X86, and MIPS executables.
The CodeHawk Abstract Interpretation Engine is implemented in OCaml. Its source code is available on under MIT License, in the CodeHawk/CH/chlib directory.