Lucas C. Cordeiro

New ESBMC release

5

Dear all, Shall we release a new version of ESBMC? ESBMC v6.11 or v7? The main feature of this release would be our new Jimple frontend for ESBMC. Additionally, the...

@rafaelsamenezes: could you please write short documentation about ESBMC-Jimple at https://ssvlab.github.io/esbmc/documentation.html? You can check how @kunjsong01 wrote such documentation for ESBMC-Solidity. In particular, you can check "Verification of Solidity Smart...

[WiP] Benchexec GitHub 152 (DO NOT MERGE)

1

This PR aims to eliminate further interleavings when the main thread has ended; it should fix #152.

[simplify_expr2] Simplify the addition operation

1

I have created this PR to evaluate the impact of each LLVM simplification in our regression suite. - **X + X to X

Signed-off-by: Lucas Cordeiro

This PR adds support for parallel SMT solving with the SMT solver Z3.

This commit fixes two issues with the CEX generation of Yices. First, if Yices does not return the truth value of a given Boolean variables, we return FALSE. If an...

added support for union dereference (EXPERIMENTAL & DO NOT MERGE)

1

This PR adds support for union dereference, but it is still experimental.

Print array elements inside a tuple (first attempt)

4

This PR aims to fetch array elements inside tuples in our counterexample. Closes #143