Collate some model checkers for future C++ evaluation #1225
kunjsong01
started this conversation in
Ideas
Replies: 1 comment
-
@kunjsong01: you could try https://cppcheck.sourceforge.io/. |
Beta Was this translation helpful? Give feedback.
0 replies
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
Just a general discussion to jot down the idea so that we could have a non-issue ticket to track this task:
Our previous STVR'21 paper compared ESBMC++ to LLBMC, DIVINE and CBMC. CBMC is still being maintained, which is "downloadable", "buildable" and still functional.
As for LLBMC and DIVINE...
LLBMC:
Latest release dated back in 2013, and now not really downloadable:
DIVINE:
The last commit in the mirror repository on Github was about 2.5 years ago back in March 2021. The download links in https://divine.fi.muni.cz/get.html also stopped working - nothing happened after clicking them.
Had to download the latest release (Feb 2020, but now July 2023) from https://github.com/paradise-fi/divine/tags,
and build from source (which is also a pretty lengthy process).Edit: following the build instructions in #1225 (comment), the last time I tried to build it failed with the error:We might need to look for some more recent and still active model checkers for C++.
@feliperodri How did we get the LLBMC binary last time?
Beta Was this translation helpful? Give feedback.
All reactions