DocumentCode :
3031850
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
fYear :
2008
fDate :
15-19 Sept. 2008
Firstpage :
479
Lastpage :
480
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;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Automated Software Engineering, 2008. ASE 2008. 23rd IEEE/ACM International Conference on
Conference_Location :
L´Aquila
ISSN :
1938-4300
Print_ISBN :
978-1-4244-2187-9
Electronic_ISBN :
1938-4300
Type :
conf
DOI :
10.1109/ASE.2008.80
Filename :
4639373
Link To Document :
بازگشت