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

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...

Full description

Bibliographic Details
Main Author: Krishnaswami, Neelakantan R.
Format: Others
Published: Research Showcase @ CMU 2012
Subjects:
Separation Logic
Design Patterns
Verification
Specification
Type Theory
Denotational Semantics
Program Logic
Program Correctness
Computer Sciences
Online Access:http://repository.cmu.edu/dissertations/164
http://repository.cmu.edu/cgi/viewcontent.cgi?article=1155&context=dissertations

Internet

http://repository.cmu.edu/dissertations/164
http://repository.cmu.edu/cgi/viewcontent.cgi?article=1155&context=dissertations

Similar Items