Herbert
**KLEE-Float** Check out https://srg.doc.ic.ac.uk/projects/klee-float/ That is an extension project to the KLEE symbolic execution engine that supports reasoning about floating-point arithmetic. For more details see: Floating-Point Symbolic Execution: A Case...
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...
**New subcategories from SV-COMP not supported yet** Apply minor changes to support: - [ ] ReachSafety-ECA - [ ] ReachSafety-Floats - [ ] ReachSafety-ProductLines - [ ] ReachSafety-Sequentialized - [...
**Termination Analysis** Add support to verify the category Termination-MainControlFlow on SV-COMP that contains programs for which termination should be decided. I suggest you check out the follows paper: - T2:...
**Check KLEE output after the map2check verification** KLEE crashes and incorrect TRUE results for Map2Check mode (e.g., target generate prt error). I would like to suggest you check out the...
Check out this sample: https://raw.githubusercontent.com/sosy-lab/sv-benchmarks/master/c/ntdrivers-simplified/cdaudio_simpl1.cil-1.c I would suggest to you add a checker result when CrabLLVM was adopted in the verification.
**Verification tasks from SV-COMP** One possible solution for the incorrect true results is to adopt a redundant check. - Add program invariant result in ERROR - **libfuzzer out**: fuzzing was...
**Verification tasks from SV-COMP** - [ ] ../../sv-benchmarks/c/list-ext3-properties/dll_nullified-1.i >> You need to improve memory leak check, bug root new_head->data_2 = __VERIFIER_nondet_int() == len? 1 : 0; >> expected_verdict: false but...
**Adopt a code slicer** Aiming to improve the code exploration and avoiding states in the program unnecessary to prove a given property, you could adopt a code slicer. Checking out...
**Verification tasks in SV-COMP** - [ ] ../../sv-benchmarks/c/bitvector/byte_add-2.i >> Fix check for shift operation r3 > Not identified bug root, but we have modeling issues with shift operation