![](https://csd.cmu.edu/sites/default/files/styles/full_width_focal_point/public/graduate.png.webp?itok=Wsy3nMEH)
Neelakantan R. Krishnaswami
Verifying Higher-Order Imperative Programs with Higher-Order Separation Logic
Degree Type:
Ph.D. in Computer Science
Advisor(s):
Stephen Brookes, John Reynolds
Graduated:
August
2012
Abstract:
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.
Thesis Committee:
Jonathan Aldrich (Co-chair)
John C. Reynolds (Co-chair)
Robert Harper
Lars Birkedal (IT University of Copenhagen)
Jeannette Wing, Head, Computer Science Department
Randy Bryant, Dean, School of Computer Science
Keywords: Separation Logic, Design Patterns, Verification, Specification, Type Theory, Denotational Semantics, Program Logic, Program Correctness
CMU-CS-12-127.pdf (916.39 KB) ( 216 pages)Copyright Notice