DocumentCode
1579646
Title
Automatically Proving Concurrent Programs Correct
Author
Cook, Byron
Author_Institution
Microsoft, Redmond
fYear
2007
Firstpage
269
Lastpage
272
Abstract
Summary form only given. This talk describes new advances that allow us to automatically prove both liveness properties and heap-shape properties of concurrent programs. The talk focuses on recent thread-modular extensions to the program termination prover TERMINATOR and shape analysis tool SLAyer and their application to Windows device drivers.
Keywords
concurrency control; multi-threading; program verification; Windows device driver; concurrent program; heap-shape property; liveness property; program termination prover TERMINATOR; shape analysis tool SLAyer; thread-modular extension; Information analysis; Shape; Software engineering;
fLanguage
English
Publisher
ieee
Conference_Titel
Software Engineering and Formal Methods, 2007. SEFM 2007. Fifth IEEE International Conference on
Conference_Location
London
Print_ISBN
978-0-7695-2884-7
Type
conf
DOI
10.1109/SEFM.2007.10
Filename
4343943
Link To Document