Software — free catalog

Inference Kernel for Open Static (IKOS) Analyzers: A High-Performance Static Analysis Engine to Build Automated Code Analysis Tools for the Formal Verification of Critical Software Properties

A NASA software catalog entry available for reuse or request.

Find it in the NASA software catalog Open project or source

About this technology

Overview

IKOS is a kernel for the construction of open-static analyzers based on Patrick Cousot and Radhia Cousot's theory of abstract interpretation, which states that computations can be abstracted and reduced to a generalized set of objects and still exhibit the same critical properties of the parent program. By reducing the set of objects through abstraction, IKOS is scalable to large complex computer programs and presents a sound approach to verification of such programs.