Automatically Verifying Concurrent Computer Programs 

Modern computer programs typically consist of threads of instructions that run on different processors, which improves processing speed. However, this “concurrency” makes it difficult to prove the correctness of such programs. While smaller programs can still be verified using the “model checking” strategy, this approach becomes impractical for larger ones. In such cases, the focus of verification should shift from proving correctness to ensuring freedom from errors.