Add support for concurrency programs, e.g., the category ConcurrencySafety.
One possible solution is to adopt Lazy-Cseq* (https://www.southampton.ac.uk/~gp1y10/cseq/) tool to generate the C code, then apply Map2Check tool with its features to improve de verification. Note that Lazy-Cseq generates nondet calls for KLEE.
*CSeq is a framework that facilitates the development of code-to-code translations for concurrent C programs with POSIX threads based on sequentialization.
Add support for concurrency programs, e.g., the category ConcurrencySafety.
One possible solution is to adopt Lazy-Cseq* (https://www.southampton.ac.uk/~gp1y10/cseq/) tool to generate the C code, then apply Map2Check tool with its features to improve de verification. Note that Lazy-Cseq generates nondet calls for KLEE.
*CSeq is a framework that facilitates the development of code-to-code translations for concurrent C programs with POSIX threads based on sequentialization.