Add witnesses to traces benchmarks - Githubissues

goblint / bench

The benchmark suite

4 stars 5 forks source link

Add witnesses to traces benchmarks #31

Closed sim642 closed 2 years ago

sim642 commented 2 years ago

This is currently on top of #30.

Instead of using the assert transformation, here the same configuration is used to generate YAML witnesses with invariants instead and all the configurations are used to validate those. The results are currently available here: https://goblint.cs.ut.ee/simmo-results/goblint-bench_result-traces-rel-yaml/. Notably:

This avoids the issues about invariants referring to globals that aren't yet declared.
More invariants than asserts are generated for some reason (seems like the assert transformation doesn't insert invariants after some locks for whatever reason).

Using https://github.com/goblint/analyzer/pull/768, we can reprove all invariants: https://goblint.cs.ut.ee/simmo-results/goblint-bench_result-traces-rel-yaml3-no-pthread/.

Using https://github.com/goblint/analyzer/pull/770#issuecomment-1173769649, we get a massive speedup: https://goblint.cs.ut.ee/simmo-results/goblint-bench_result-traces-rel-yaml9-shallow-sound/.

sim642 commented 2 years ago

Merging this quickly with copied index and script for getting everything together for the paper.