ICACT20260385 Question.1
Questioner: hovhannes.movsisyan@rau.am 2026-02-09 오전 11:17:09 |
ICACT20260385 Answer.1
Answer by Auhor hripsime.hovhannisyan@rau.am 2026-02-09 오전 11:17:09
Chrome  Click!! |
| The experimental results on the Juliet test suite demonstrate that there are no false positives. Are there any false positives in real-world projects?
|
We verified two CVEs with IKOS: it successfully reported the bugs in the original commits, but once the fixes were applied, it reported nothing. This confirms we didnt encounter any false positives on these real-world cases |
ICACT20260385 Question.2
Questioner: arjunvirvashisht@gmail.com 2026-02-10 오전 3:47:49 |
ICACT20260385 Answer.2
Answer by Auhor hripsime.hovhannisyan@rau.am 2026-02-10 오전 3:47:49
Chrome Click!! |
| What specific version of the IKOS analyzer was used for these experiments? |
We used IKOS 3.5. |
ICACT20260385 Question.3
Questioner: hominpark@etri.re.kr 2026-02-10 오후 1:43:42 |
ICACT20260385 Answer.3
Answer by Auhor hripsime.hovhannisyan@rau.am 2026-02-10 오후 1:43:42
Chrome Click!! |
| Unlike its perfect precision on Juliet, doesnt IKOSs failure with STL containers and complex loops—core elements of modern C++—critically undermine its practical utility for certifying real-world avionics systems?
|
IKOS’s limitations with STL and complex loops create a significant coverage gap for modern C++, yet its utility in avionics remains high because safety-critical standards (like MISRA) often ban those exact features. Since avionics code typically avoids dynamic memory and complex templates, it stays within the "low-level" niche where IKOS provides the soundness and formal proof required for certification. |
ICACT20260385 Question.4
Questioner: kanampiumw@wssu.edu 2026-02-11 오전 4:05:21 |
ICACT20260385 Answer.4
Answer by Auhor hripsime.hovhannisyan@rau.am 2026-02-11 오전 4:05:21
Chrome Click!! |
| For future work would you consider the applicability of an AI-Based Framework with the aim of enhancing this scheme? |
While the primary goal of our current work is the rigorous evaluation and benchmarking of IKOS to understand its existing capabilities and limitations, we certainly consider an AI-based framework to be a promising direction for future enhancement. |
ICACT20260385 Question.5
Questioner: kanampiumw@wssu.edu 2026-02-11 오전 4:07:03 |
ICACT20260385 Answer.5
Answer by Auhor hripsime.hovhannisyan@rau.am 2026-02-11 오전 4:07:03
Chrome Click!! |
| Which section(s) of this work would you consider employing AI assistance to enhance your scheme? |
We would specifically consider employing AI assistance in the loop analysis section, particularly for the prediction of widening upper bounds. |
