符號執行的應用程序

符號執行的應用程序是什麼？做symbolic execution只生成path condition？我如何使用符號執行來驗證contract？符號執行的應用程序

2016-09-17 any

符號執行最着名的用法是測試輸入生成。例如，KLEE是一個使用符號執行爲C程序生成測試輸入的工具。

另一個應用程序將斷言檢查。如果通過契約來表示事前和事後條件，那麼是的，符號執行也可以用於該目的。

2016-09-20 15:29:40 afsafzal

非常感謝。符號執行是否僅在輔助約束求解器中生成測試輸入？您能否介紹一下如何使用符號執行來檢查前期和後期條件？ – any

據我所知，它在約束求解器的幫助下生成測試輸入。最簡單的想法：想象一下，你有一個前置和後置條件的功能。通過使用符號執行，您可以找到該函數所有可能路徑的路徑條件。如果「後條件和路徑條件」在所有路徑內均可滿足，則後條件成立。 – afsafzal

感謝您的善意幫助。如果「後置條件和路徑條件」可滿足或「前置條件和路徑條件」？ – any

回答