PtYasm: Software Model Checking with Proof Templates

—We describe PTYASM, an enhanced version of the YASM software model checker which uses proof templates. These templates associate correctness arguments with common programming idioms, thus enabling efficient verification. We have used PTYASM to verify the safety of array accesses in programs derived from the Verisec suite. PTYASM is able to verify this property in the majority of testcases, while existing software model checkers fail to do so due to loop unrolling.

• Type: Conference
• Year: 2008
• Where: KBSE
• Authors: Thomas E. Hart, Kelvin Ku, Arie Gurfinkel, Marsha Chechik, David Lie
• Keywords: KBSE 2008, Software Engineering, Software Model Checkers, Templates Associate Correctness, YASM Software Model