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.
| Identifer | oai:union.ndltd.org:cmu.edu/oai:repository.cmu.edu:dissertations-1155 |
| Date | 01 June 2012 |
| Creators | Krishnaswami, Neelakantan R. |
| Publisher | Research Showcase @ CMU |
| Source Sets | Carnegie Mellon University |
| Detected Language | English |
| Type | text |
| Format | application/pdf |
| Source | Dissertations |
Page generated in 0.0017 seconds