NASA Logo, National Aeronautics and Space Administration


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 is now available on github:

Download IKOS 2.0 - October 2018

IKOS 2.0 installation has been successfully tested on the following platforms:

  • Archlinux
  • CentOS 6.10 and 7.5
  • Debian 8 and 9
  • Fedora 27 and 28
  • Mac OS X High Sierra (Version 10.13.6)
  • Red Hat Enterprise Linux 6.10 and 7.5
  • Ubuntu 14.04, 16.04 and 18.04

Download IKOS 1.3 - October 2017

IKOS 1.3 installation has been successfully tested on the following platforms:

  • Archlinux
  • CentOS 6.9 and 7.4
  • Debian 8 and 9
  • Fedora 26
  • Mac OS X Yosemite (Version 10.11.6)
  • Red Hat Enterprise Linux 6.9 and 7.4
  • Ubuntu 12.04, 14.04, 16.04 and 17.04

Download IKOS 1.2 - October 2016

  • ikos-1.2.tar.gz (installation notes and other documentation are packaged in the archive)

IKOS 1.2 installation has been successfully tested on the following platforms:

  • Archlinux
  • CentOS 6.8 and 7.2
  • Debian 8
  • Fedora 23 and 24
  • Mac OS X Yosemite (Version 10.10.5)
  • Red Hat Enterprise Linux 6.8 and 7.2
  • Ubuntu 12.04, 14.04 and 16.04


Contact us by sending an email to

Current/Past Contributors

Maxime Arthaud
Thomas Bailleux
Guillaume Brat
Clément Decoodt
Jorge Navas
Nija Shi
Sarah Thompson
Arnaud Venet
Alexandre Wimmers

This software is released under the terms and conditions of the NASA Open Source Agreement (NOSA) Version 1.3 or later.

IKOS NOSA Software Agreement (PDF)
IKOS NOSA Software Agreement (WORD)

First Gov logo
NASA Logo -