goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
173 stars 72 forks source link

Handle large programs context-insensitively with autotuner #899

Open jerhard opened 1 year ago

jerhard commented 1 year ago

For the analysis of large programs, the autotuner should set the analysis to be context-insensitive, following the heuristic that context-insensitive analyses tend to terminate more quickly.

michael-schwarz commented 1 year ago

Paraphrasing @jerhard from Zulip. Just enabling ana.av-comp.enabled slows down Goblint from ~1:30min to 25mins for the context insensitive setting on a larger benchmark. Thus, before we can do this, we would need to squeeze a lot of performance out of the witness generation.

I don't think that this is realistic for sv-comp this year.