Asynchronous programming is a general programming idiom where concurrent tasks are executed by a co-operative scheduler, and appear from low-level kernel or embedded systems code to smartphone and web programming environments. In its simplest form, the underlying programming system exposes an asynchronous procedure call construct, which allows the programmer to post a procedure for future execution in case a certain event occurs. When the corresponding event occurs, a scheduler picks the associated procedure and runs it to completion.

In this talk, I will describe algorithmic analysis techniques for asynchronous programs. On the one hand, I will talk about formal models for different styles of asynchronous programs and the decidability landscape. On the other, I will talk about our attempts to build model checking and program analysis tools for programs written in this style, both for verification and for systematic testing.