Title :
Automatically Proving Concurrent Programs Correct
Author_Institution :
Microsoft, Redmond
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;
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
DOI :
10.1109/SEFM.2007.10
