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