This is the changelog file for the Map2Check Tool.
- using LibFuzzer to provide random data as input to C programs to quickly expose “shallow” bugs, i.e., those that do not require complex data input;
- implementing a new runtime library and instrumentation approach to monitor for crashes, failing built-in assertions and pointer safety;
- adopting Crab-LLVM to infer invariants;
- exploiting a sequential approach with LibFuzzer and KLEE to check safety properties in a novel way;
- adopting MetaSMT as a wrapper around various SMT solvers, for instance, Boolector and Yices, previously not supported by our tool; and
- fixed a couple of bugs.
- minor changes to SVCOMP 2018
- futher details https://link.springer.com/chapter/10.1007/978-3-319-89963-3_28
- we added witness true
- we improved nondet functions
- we added files to svcomp'18
- fixed a couple of bugs
- general improvements to track memory address
- we adopt Clang to parse C code
- we use LLVM as intermediary representation to code instrumentation
- we use KLEE for symbolic execution
- added dockerfile to build Map2Check
- fix bugs related to counter-example generation
- general improvements to track memory address
- minor improvements to the tool.
- futher details at https://link.springer.com/chapter/10.1007/978-3-662-49674-9_64
- first Map2Check public release.