Many modern APIs contain interfaces in which methods have strict state based preconditions, while mainstream programming languages provide no facility to express these constraints in a concise,
human readable, machine verifiable form. Failure to detect violations of these preconditions can result in partial or catastrophic failure of a system, therefore programmers must take great care in understanding and verifying the usage of such APIs.

In this talk I discuss the broad goals and challenges of program verification, and the Hanoi language, which I devised to clearly, concisely describe typestate restrictions on Java APIs. The talk is high level and suitable for anyone with a background in computer science and software engineering.

I gave this talk at the 2010 SICSA PhD Conference at Edinburgh University, Scotland.