Title :
Verifying linked data structure implementations
Author :
Zee, Karen ; Kuncak, Viktor ; Rinard, Martin
Author_Institution :
MIT CSAIL, Cambridge, MA
Abstract :
The Jahob program verification system leverages state of the art automated theorem provers, shape analysis, and decision procedures to check that programs conform to their specifications. By combining a rich specification language with a diverse collection of verification technologies, Jahob makes it possible to verify complex properties of programs that manipulate linked data structures. We present our results using Jahob to achieve full functional verification of a collection of linked data structures.
Keywords :
data structures; program verification; Jahob program verification system; art automated theorem provers; data structure; program specifications; shape analysis; Concrete; Data structures; Diversity reception; Java; Shape; Software systems; Specification languages; Tree data structures; Tree graphs; Virtual machining;
Conference_Titel :
Parallel and Distributed Processing, 2008. IPDPS 2008. IEEE International Symposium on
Conference_Location :
Miami, FL
Print_ISBN :
978-1-4244-1693-6
Electronic_ISBN :
1530-2075
DOI :
10.1109/IPDPS.2008.4536430
