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 buffer-overflow analyzer for C programs based on the LLVM front-end.

Publications

  • 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 & Documentation

Installation instructions


Download IKOS

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)

You can register your download using this form, all fields are required:
Full Name:
Street Address:
City:
State:
eMail Address:
First Gov logo
NASA Logo - nasa.gov