Using Isabelle to Help Verify Code That Uses Abstract Data Types

Verification of programs that use paper Data Types (ADTs) is an important piece of the grand challenge of verified software. It is the position that an interactive proof assistant, such as Isabelle, used in a fully automated mode, can be an effective, extensible proof engine for use in the modular verification of software. As technical justification for this position, the authors describe the modular verification of two implementations of an extension to a queue ADT. One implementation is recursive, while the other is iterative and relies on a stack ADT. The correctness of the implementations is proved by Isabelle automatically, using specification theories from the Resolve mathematical library imported into Isabelle.