Automatic verification for interactive graphical programs

Modern software applications come with interactive graphical displays. In the past, verification efforts for such programs have usually ignored the I/O aspects of programs and focused instead on their core functionality. This approach leaves open the question of how errors in the interactive part of the program can affect its overall functionality. In this paper we present an extension of Dracula (the ACL2 development environment for DrScheme) with a simple graphical framework. With Dracula we can automatically prove theorems about interactive graphical programs, guaranteeing their complete behavior. We have successfully verified theorems about a number of interactive programs with Dracula; we have also successfully used Dracula as a motivational tool to introduce students to the world of automated theorem proving.