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 :
بازگشت