Write simple SVG converter to change font, colors, and shapes in SVG file.

One challenge the article omits is that of handling behavioral values such as first-class functions. This is addressed in the following papers:

• Higher-Order Symbolic Execution via Contracts. Sam Tobin-Hochstadt and David Van Horn.
  The ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'12), Tuscon, Arizona, October 2012. http://dl.acm.org/citation.cfm?id=2384655

• Soft Contract Verification. With Phuc C. Nguyen, Sam Tobin-Hochstadt, and David Van Horn.
  The ACM SIGPLAN International Conference on Functional Programming (ICFP'14), Gothenburg, Sweden, September 2014. http://dl.acm.org/citation.cfm?id=2628156

• Relatively Complete Counterexamples for Higher-Order Programs. Phuc C. Nguyen and David Van Horn. The 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'15), Portland, Oregon, June, 2015. https://dl.acm.org/citation.cfm?id=2737971

By @joeranweiler:

A suggestion: SAW, by @galois: saw.galois.com (disclosure: I'm a former employee)

See DyTa: Dynamic Symbolic Execution Guided with Static Verification Results.

Such as BCEL and ASM.

Create a comprehensive description of the diagram notation.

ConCrest (or just Crest https://www.burn.im/crest/)

• Farzan, Azadeh, et al. "Con2colic testing." Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering. ACM, 2013.

Cortex (https://github.com/nunomachado/cortex-tool)

• Machado, Nuno, Brandon Lucia, and Luís Rodrigues. "Production-guided concurrency debugging." Proceedings of the 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming. ACM, 2016.

Conc-iSE

• Guo, Shengjian, Markus Kusano, and Chao Wang. "Conc-iSE: Incremental symbolic execution of concurrent software." Automated Software Engineering (ASE), 2016 31st IEEE/ACM International Conference on. IEEE, 2016.

https://github.com/illera88/Ponce

"Provides users the ability to perform taint analysis and symbolic execution over binaries in an easy and intuitive fashion. With Ponce you are one click away from getting all the power from cutting edge symbolic execution. Entirely written in C/C++"

Main paper: Taint-based Directed Whitebox Fuzzing.

Mentioned by @SeanHeelan:

• Efficient State Merging in Symbolic Execution (QCE);
• make test-zesti: A Symbolic Execution Solution for Improving Regression Testing (ZESTI).

Some extend the honor of "first" to a symbolic execution program called EFFIGY (1976) . Others acknowledge a program called SELECT (1976).

Both would be great additions who also contain bibliographies with lots of references to earlier work in program verification (most notably the verification of avionics in the United States Air Force - a kind of proto-cyberwarfare fear that the Russians, known for their technical prowess, could "hack" airplanes).

It's unclear how you might combine more modern innovations like "VSIDS", but it would be fantastic to see such a thing as well.

Thanks for putting this together!!

See Simplify: A Theorem Prover for Program Checking.

Thanks to Vijay Ganesh.

At least, add winners:

• vampire,
• veiT,
• Redlog,
• SMTInterpol,
• CaDiCaL,
• MinkeyRink,
• COLIBRI,
• AProVE.

Some symbolic engines noted A Survey of Symbolic Execution Techniques paper are missing on diagram:

• Rubyx,
• Cloud9,
• SymDroid,
• FuzzBALL,
• Pathgrind,
• Kite,
• SymJS,
• CIVL,
• KeY,
• CATG,
• PySymEmu,
• Miasm.

Dynamic binary analysis tool Manticore.

• Avatar,
• FIE,
• SymDrive,
• RevNIC.

Thanks to @fatemender.

Suggested by @ntddk.

This is awesome! Some minor additions (as a disclaimer, I worked on all of these projects, but I feel they're worth mentioning nonetheless as the first is, to the best of my knowledge, the first AEG system of its kind, while the second two are the first reverse engineering/symex hybrid tools of their kind). I would make the chances myself but I'm fairly certain I would break everything ;)

Sep 2009: Thesis publication: "Automatic Generation of Control Flow Hijacking Exploits for Software Vulnerabilities" - Utilised symbolic execution to generate exploits. The implementation was titled AXGEN.
(Authors: S. Heelan, D. Kroening @ University of Oxford)

Dec 6th 2010: Immunity Debugger v1.8 released, embedding a symbolic execution engine into Immunity Debugger for use during reverse engineering (http://seclists.org/dailydave/2010/q4/23) (Authors: P. Sole, S. Heelan @ Immunity Inc.)

Dec 2nd 2013: ILLITHID (also by Immunity, DARPA funded), a standalone tool focused on finding software vulnerabilities combining compositional symbolic execution, function annotations and manual reverse engineering https://lists.immunityinc.com/pipermail/dailydave/2013-December/000539.html (Authors: S. Heelan, P. Sole, R. Huizer @ Immunity Inc)

See The BORG: Nanoprobing Binaries for Buffer Overreads.

Add string solvers:

• Z3str → Z3str2 → Z3str3,
• CVC4,
• Norn,
• S3 → S3P,
• Stranger → ABC,
• DPRLE,
• Rex,
• Hampi.

Kudzu, a symbolic execution framework for JavaScript (paper).

Add Generalized symbolic execution for model checking and testing.

Here are a few papers/tools that deal with floating-point numbers. I think their addition would be interesting!

• Lakhotia, Kiran, et al. "Flopsy-search-based floating point constraint solving for symbolic execution." IFIP International Conference on Testing Software and Systems. Springer Berlin Heidelberg, 2010.
• https://srg.doc.ic.ac.uk/projects/klee-cl/
• Barr, Earl T., et al. "Automatic detection of floating-point exceptions." ACM SIGPLAN Notices. Vol. 48. No. 1. ACM, 2013.

• Boolector,
• PicoSAT,
• UCLID,
• Yices.

• Qsym (paper),
• Symcc (paper, GitHub, site),
• SymQEMU (paper),
• Fuzzolic (site),
• Jigsaw (paper).

Thanks to Vijay Ganesh.

By Brian Mastenbrook‏ @bmastenbrook:

It's missing a really interesting tool/language, Rosette: https://emina.github.io/rosette/

Add missing author affiliations.

See GitHub page.