NASA Logo, National Aeronautics and Space Administration


IKOS logo

IKOS: Inference Kernel for Open Static Analyzers

The objective of this project is to perform scalable, precise static analysis of C and C++ code for aviation.

To this end, we have developed a tool, IKOS, that relies on the theory of Abstract Interpretation for analyzing C and C++ code. IKOS is really a framework for static analysis based on abstract interpretation. It relies on the LLVM framework for its front-end and implements various analyses based on its own library of abstract interpretation components (forward iterators, abstract domains, ...).

Key Benefits

  • Offers a library of abstract interpretation components for quickly building analyzers
  • Includes analyzers for null pointer dereference, division by zero, uninitialized variables and arrays, and buffer under/overflow
  • Applies to C and C++ code, but is more efficient on embedded code implemented in C

Applications

Static code analysis of various aviation applications (e.g., flight controls for drones).

References

Updated October 2018


Latest News

October 2018: IKOS 2.0 released on GitHub.

Other information

IKOS website
IKOS downloads

Active Members

Maxime Arthaud
Guillaume Brat
Nija Shi

Past Members

Arnaud Hamon
Jorge Navas
Elodie-Jane Simms
Sarah Thompson
Arnaud Venet

Summer Interns

Thomas Bailleux
Clement Decoodt
Alexandre Wimmers

Related Projects

CodeHawk from KT
Astree from ENS

First Gov logo
NASA Logo - nasa.gov