NASA Logo, National Aeronautics and Space Administration

IKOS

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.

Publications

  • 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).

Software

Download IKOS

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

IKOS installation has been successfully tested on the following platforms:

  • Mac OS X Yosemite (Version 10.10.5)
  • Red Hat Linux 6.7 and 7.1
  • Debian 8

Contact

Contact us by sending an email to ikos@lists.nasa.gov

Current/Past Contributors

Maxime Arthaud
Guillaume Brat
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 - nasa.gov