search

ftsrg / gazer

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

Support SV-COMP ReachSafety-Heap with Theta #81

Open hajduakos opened 3 years ago

hajduakos commented 3 years ago

This might be a longer-term plan. First step would be to have some partial support where at least we can parse and don't give wrong results (or harnesses can filter them).

AdamZsofi commented 3 years ago

Not top priority right now, but I'll run some benchmarks for this later, as we didn't even try this category earlier.