TL;DR
プログラム解析の手法の 1 つで、実際の値ではなくシンボルを使ってプログラムの動作をシミュレーションする。
なぜ必要か
具体的な値で実行すると、その値が通る実行パスしか確かめられない。シンボリック実行ではすべての実行パスを網羅的に調べられるので、バグや脆弱性、仕様違反を見つけられる。
仕組み
シンボルとは抽象的な値である。コードを実行するときに与えられる具体的な値を表す、プレースホルダの役割を持つ。
Wikipedia によると、シンボリック実行では条件分岐に出会うたびに実行が分かれ、パスごとに状態とパス条件（そのパスを通るための入力の制約）を持つ。パスの終わりで制約ソルバにパス条件を解かせると、そのパスを通る具体的な入力が得られる。この入力はバグを再現するテストケースに使える。この考え方は 1970 年代に研究され、1976 年の King の論文が広く知られている。
例
入力が 6 のときに失敗する C のプログラムでは、失敗する分岐のパス条件として λ × 2 == 12 が得られ、ソルバが 6 を見つける。32 ビット整数のオーバーフローを考えると、-2147483642 も見つかる。ツールには LLVM のビットコードを対象にする KLEE や、バイナリを対象にする angr などがある。
注意点
プログラムが大きくなると、実行できるパスの数は指数的に増える（パス爆発）。カーネルの呼び出しのように、ツールの外にある環境とのやりとりも扱いにくい。同じパスを通る入力が少ないプログラムでは、入力を 1 つずつ試すのと比べた利点が小さい。