Computer Science Department
School of Computer Science, Carnegie Mellon University


Verifying Higher-Order Imperative Programs
with Higher-Order Separation Logic

Neelakantan R. Krishnaswami

June 2012

Ph.D. Thesis


Keywords: Separation Logic, Design Patterns, Verification, Specification, Type Theory, Denotational Semantics, Program Logic, Program Correctness

In this thesis I show is that it is possible to give modular correctness proofs of interesting higher-order imperative programs using higher-order separation logic.

To do this, I develop a model higher-order imperative programming language, and develop a program logic for it. I demonstrate the power of my program logic by verifying a series of examples. This includes both realistic patterns of higher-order imperative programming such as the subject-observer pattern, as well as examples demonstrating the use of higher-order logic to reason modularly about highly aliased data structures such as the union-find disjoint set algorithm.

216 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by