There is a new study where they study the precision of IKOS on Juliet: https://ieeexplore.ieee.org/abstract/document/11431352
This study details the specific coding patterns that cause false negatives—such as wide character usage and widening techniques in loops—providing insights for practitioners selecting the IKOS analysis tool and researchers improving static analysis precision.
This could be interesting for a BSc student to read and see if any of these things also apply to Goblint.
There is a new study where they study the precision of IKOS on Juliet: https://ieeexplore.ieee.org/abstract/document/11431352
This could be interesting for a BSc student to read and see if any of these things also apply to Goblint.