Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007) London, England September 10-September 14 ISBN: 0-7695-2884-8
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SEFM.2007.10
This talk will describe new advances that allow us to automatically prove both liveness properties and heap-shape properties of concurrent programs. The talk will focus on recent thread-modular extensions to the program termination prover TERMINATOR and shape analysis tool SLAyer and their application to Windows device drivers.
Citation:
Byron Cook, "Automatically Proving Concurrent Programs Correct," sefm, pp.269-272, Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), 2007 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||