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 analyzers for detecting buffer-overflow, division-by-zero, null pointers, and uninitialized variables and arrays for C and C++ (with limited capabilities) programs based on the LLVM front-end.
Guillaume Brat, Jorge Navas, Nija Shi and Arnaud Venet. IKOS: a Framework for Static Analysis based on Abstract Interpretation. In Proceedings of the International Conference on Software Engineering and Formal Methods (SEFM 2014), Grenoble, France (PDF).
Arnaud Venet. The Gauge Domain: Scalable Analysis of Linear Inequality Invariants. In Proceedings of Computer Aided Verification (CAV 2012), Berkeley, California, USA 2012. Lecture Notes in Computer Science, pages 139-154, volume 7358, Springer 2012 (PDF).
IKOS installation has been successfully tested on the following platforms:
Contact us by sending an email to firstname.lastname@example.org