Map2Check
Map2Check copied to clipboard
hbgit
Map2Check: Finding Software Vulnerabilities
# Description Closes #45 - More info on the issue
**Is your feature request related to a problem? Please describe.** FuseBMC is trying to use map2check to create coverage for C programs. However, its targets consists in functions named GOAL_N...
# Description This adds an option to specify a nondet-generator. If the flag is not set then the combination will be used. Closes #43 ## Type of change - [X]...
**Is your feature request related to a problem? Please describe.** I'd like to run only KLEE or only libFuzzer (or any future generator) **Describe the solution you'd like** Add the...
**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 - [...
**Is your feature request related to a problem? Please describe.** Currently, we only have support for KLEE as a symbolic engine, the issue is that it contains a limitation for...
**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...