Sergey Vartanov

Add new tools

1

- [ ] Qsym ([paper](https://sangho2.github.io/papers/yun:qsym.pdf)), - [ ] Symcc ([paper](https://www.s3.eurecom.fr/docs/usenixsec20_symcc.pdf), [GitHub](https://github.com/eurecom-s3/symcc), [site](https://www.s3.eurecom.fr/tools/symbolic_execution/symcc.html)), - [ ] SymQEMU ([paper](https://www.ndss-symposium.org/wp-content/uploads/ndss2021_2B-2_24118_paper.pdf)), - [ ] Fuzzolic ([site](https://season-lab.github.io/fuzzolic/)), - [ ] Jigsaw ([paper](https://www.cs.ucr.edu/~csong/oakland22-jigsaw.pdf)).

Such as BCEL and ASM.

See [GitHub page](https://github.com/google/honggfuzz).

At least, add winners: - [ ] vampire, - [ ] veiT, - [ ] Redlog, - [ ] SMTInterpol, - [ ] CaDiCaL, - [ ] MinkeyRink, - [...

Add _Generalized symbolic execution for model checking and testing_.

See _DyTa: Dynamic Symbolic Execution Guided with Static Verification Results_.

See [_Simplify: A Theorem Prover for Program Checking_](http://dl.acm.org/citation.cfm?id=1066102). Thanks to Vijay Ganesh.

- [ ] Avatar, - [ ] FIE, - [ ] SymDrive, - [ ] RevNIC. Thanks to @fatemender.

Mentioned by @SeanHeelan: - [Efficient State Merging in Symbolic Execution](https://www.cs.rhul.ac.uk/home/kinder/papers/pldi12.pdf) (QCE); - [`make test-zesti`: A Symbolic Execution Solution for Improving Regression Testing](https://www.doc.ic.ac.uk/~cristic/papers/zesti-icse-12.pdf) (ZESTI).