Title :
PtYasm: Software Model Checking with Proof Templates
Author :
Hart, Thomas E. ; Ku, Kelvin ; Gurfinkel, Arie ; Chechik, Marsha ; Lie, David
Author_Institution :
Dept. of Comput. Sci., Univ. of Toronto, Toronto, ON
Abstract :
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.
Keywords :
formal specification; program control structures; program verification; PTYASM; Verisec suite; YASM software model checker; loop unrolling; program verification; programming idioms; proof templates; software model checking; Arithmetic; Computer science; Kelvin; Performance analysis; Safety; Sliding mode control; Software performance; Software testing; Software tools; System testing;
Conference_Titel :
Automated Software Engineering, 2008. ASE 2008. 23rd IEEE/ACM International Conference on
Conference_Location :
L´Aquila
Print_ISBN :
978-1-4244-2187-9
Electronic_ISBN :
1938-4300
DOI :
10.1109/ASE.2008.80