Verification of Asynchronous Programs

Asynchronous Programming is a paradigm that is often used in low-level system software, web programming, and user applications on mobile platforms. However, these programs are difficult for a programmer to write correctly. This means we need software tools for verification, which can automatically establish correctness of such programs or exhibit faulty executions. In a recent project on verification of asynchronous programs, we have found a new approach that permits the automatic verification of a large variety of asynchronous programs.