Dat3M 2.0.6 is out!
·
3181 commits
to master
since this release
Dartagnan can now verify program written in C.
It uses SMACK (needs to be installed independently) as a backend to convert C programs to Boogie and it then performs the verification on the Boogie representation of the program.
We also improved the IR of programs to support more kind of expressions (including input non-determinism) and implemented loop unrolling of goto instructions.