3 ms·
It's hard to cross check since you didn't mention what you consider are good answers, but the quick answer snippet on Kagi says: > The Yogar-CBMC and JCBMC sol
by Etheryte 2y ago
It's hard to cross check since you didn't mention what you consider are good answers, but the quick answer snippet on Kagi says:
> The Yogar-CBMC and JCBMC solvers are notable multi-threaded variants of the CBMC (C Bounded Model Checker) framework: ...
Followed by further details and references. The search results themselves look relevant and reasonable to me, but again, outside my area of expertise.
- rurban 2y agoBoth are bad answers
- Etheryte 2y agoOkay and why is that?
- rurban 2y agoI was asking for multi-threaded solvers supported by CBMC, not multi-threaded CBMC, which is 1% of the runtime of large models. I'm trying to find proofs for strstr implementations, like Morris-Pratt in C. JCBMC is for Java programs. Good answers would be Z3, yices2, CVC5, Kisssat. Bad answers would be CaDiCaL, minisat2 (the default), and all the other supported single threaded solvers for the dimacs and ipasir interface for the SAT problems (which are much simplier than SMT problems). Just unrolling the loops and comparing to a small brute force strstr leads to very large models, which would need to run in several minutes, compared to the typical 20s. I'm considering running it on one of my big work machines with a parallel solver. Out of the 220 strstr's I suspect several of them to be wrong. I know that they are wrong, but CBMC gives me counterexamples where they would break exactly, and why. Better than a fuzzer, which just guesses around.