IKOS: Inference Kernel for Open Static Analyzers
IKOS is a C++ library designed to facilitate the development of sound static analyzers based on Abstract Interpretation. Specialization of a static analyzer for an application or family of applications is critical for achieving both precision and scalability. Developing such an analyzer is arduous and requires significant expertise in Abstract Interpretation.
IKOS provides a generic and efficient implementation of state-of-the-art Abstract Interpretation data structures and algorithms, such as control-flow graphs, fixpoint iterators, numerical abstract domains, etc. IKOS is independent of a particular programming language.
In order to build an effective static analyzer, one has to use IKOS building blocks in combination with a front-end for a particular language. As an illustration, we provide the implementation of a simple buffer-overflow analyzer for C programs based on the LLVM front-end.