Proving Properties of Concurrent Programs

摘要

How do you prove the correctness of multi-threaded code? This question has been asked since at least the mid-sixties, and it has inspired researchers ever since. Many approaches have been tried, based on mathematical theories, the use of annotations, or the construction of abstractions. An ideal solution would be a tool that one can point at an arbitrary piece of concurrent code, and that can resolve correctness queries in real-time. We describe one possible method for achieving this capability with a logic model checker.