 |
To address the memory issues weve discussed, we evaluated IKOS, an open-source static analyzer developed by NASA specifically for certifying flight software in avionic systems. Its core strength lies in its foundation of Abstract Interpretation, a mathematical framework that guarantees soundness—meaning if a certain type of error exists, IKOS is mathematically designed to find it.
Architecturally, IKOS is built on the LLVM compiler infrastructure, allowing it to analyze standard C and C++ files as well as LLVM bitcode. Besides that, it uses dynamic inlining and interprocedural analysis, which allows the tool to track data not just within a single block of code, but across multiple functions, providing a more holistic view of the programs behavior. |
IEEE/ICACT20260385 Slide.08
[Big Slide]