Verifying Higher-Order Imperative Programs with Higher-Order Separation Logic
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...
| Main Author: | |
|---|---|
| Format: | Others |
| Published: |
Research Showcase @ CMU
2012
|
| Subjects: | |
| Online Access: | http://repository.cmu.edu/dissertations/164 http://repository.cmu.edu/cgi/viewcontent.cgi?article=1155&context=dissertations |
| Summary: | 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. |
|---|