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(ARC-16789-1)

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.