シンボリック実行

特定の条件を満たしてくれる(プログラムの特定の分岐を実行する)入力を探索したりできる

SAT/SMTソルバーで実現してる