Java などの特定の言語で記述されたプログラムの堅牢性をテストするために、シンボリック実行を使用することを検討しています。シンボリック実行の基本概念を紹介するいくつかの論文を読みました。しかし、私はそれを開始する方法について明確ではありません。
たとえば、具体的な入力から制約条件を生成するにはどうすればよいですか? では、シンボリック実行の実装の基本についてアドバイスをくれる人はいますか? さらに、コンコリック実行(具体的+シンボリック)はどうですか?
Java などの特定の言語で記述されたプログラムの堅牢性をテストするために、シンボリック実行を使用することを検討しています。シンボリック実行の基本概念を紹介するいくつかの論文を読みました。しかし、私はそれを開始する方法について明確ではありません。
たとえば、具体的な入力から制約条件を生成するにはどうすればよいですか? では、シンボリック実行の実装の基本についてアドバイスをくれる人はいますか? さらに、コンコリック実行(具体的+シンボリック)はどうですか?
具体的な入力から制約条件を生成するにはどうすればよいですか?
シンボリックまたはコンコリック実行の使用
では、シンボリック実行の実装の基本についてアドバイスをくれる人はいますか?
私のアドバイスは Ziming Zhao と同じです。既存のシンボリック実行ツールを使用してください。独自に実装しようとしないでください。非常に難しく、時間がかかります。
最も人気のあるプロジェクトは次のとおりです (より完全なリストはこちら)。
Java: JPF + シンボリックパスファインダー、JCute .