Victoria University of Wellington
Program Verification with Separation Logic and Rely Guarantee.
Degree: 2017, Victoria University of Wellington
This thesis explores two kinds of program logics that have become important for modern program verification - separation logic, for reasoning about programs that use pointers to build mutable data structures, and rely guarantee reasoning, for reasoning about shared variable concurrent programs. We look more closely into the motivations for merging these two kinds of logics into a single formalism that exploits the benefits of both approaches - local, modular, and explicit reasoning about interference between threads in a shared memory concurrent program. We discuss in detail two such formalisms - RGSep and Local Rely Guarantee (LRG), in particular we analyse how each formalism models program state and treats the distinction between global state (shared by all threads) and local state (private to a given thread) and how each logic models actions performed by threads on shared state, and look into the proof rules specifically for reasoning about atomic blocks of code. We present full examples of proofs in each logic and discuss their differences. This thesis also illustrates how a weakest precondition semantics for separation logic can be used to carry out calculational proofs. We also note how in essence these proofs are data abstraction proofs showing that a data structure implements some abstract data type, and relate this idea to a classic data abstraction technique by Hoare. Finally, as part of the thesis we also present a survey of tools that are currently available for doing manual or semi-automated proofs as well as program analyses with separation logic and rely guarantee.
Advisors/Committee Members: Groves, Lindsay.
Subjects/Keywords: Logic; Program verification; Concurrency
to Zotero / EndNote / Reference
APA (6th Edition):
Tabilog, A. (2017). Program Verification with Separation Logic and Rely Guarantee. (Masters Thesis). Victoria University of Wellington. Retrieved from http://hdl.handle.net/10063/6271
Chicago Manual of Style (16th Edition):
Tabilog, Allan. “Program Verification with Separation Logic and Rely Guarantee.” 2017. Masters Thesis, Victoria University of Wellington. Accessed August 19, 2017.
MLA Handbook (7th Edition):
Tabilog, Allan. “Program Verification with Separation Logic and Rely Guarantee.” 2017. Web. 19 Aug 2017.
Tabilog A. Program Verification with Separation Logic and Rely Guarantee. [Internet] [Masters thesis]. Victoria University of Wellington; 2017. [cited 2017 Aug 19].
Available from: http://hdl.handle.net/10063/6271.
Council of Science Editors:
Tabilog A. Program Verification with Separation Logic and Rely Guarantee. [Masters Thesis]. Victoria University of Wellington; 2017. Available from: http://hdl.handle.net/10063/6271