search

ftsrg / gazer

An LLVM-based formal verification frontend for C programs.
24 stars 5 forks source link

Support SV-COMP ReachSafety-Arrays with BMC #76

Open hajduakos opened 3 years ago

hajduakos commented 3 years ago

I don't know if it actually works or not, we should try first.

sallaigy commented 3 years ago

There does not seem to be any syntactical issues with programs in this category, but they make heavy use of large, constant-bounded loops, something that the BMC algorithm handles very poorly (as it needs to unroll all of these loops).