New foundations for separation logic

This thesis presents new foundations for separation logic, an important field within the formal sciences such as theoretical computer science. Around the turn of the millennium, separation logic was introduced by J.C. Reynolds with the goal to make reasoning, about the correctness of computer programs that work with so-called ‘pointers’, more efficient than earlier formal methods. Reynolds’ method and the other earlier methods are both extensions of the proof system introduced by C.A.R. Hoare for reasoning about the correctness of simple while-programs. The essence of Reynolds’ initial work, which was researched and put into practical use by many other scientists, consists of two extensions of the work initiated by Hoare: the first extension adds to first-order predicate logic two new propositional connectives (the so-called separating conjunction and separating implication); the second extension adds to Hoare’s program logic new proof rules for reasoning about (the primitive operations of) pointer programs. These primitive operations are used for reading memory (‘lookup’), writing memory (‘mutation’), reserving memory (‘allocation’), or freeing memory (‘deallocation’).

• View at Worldcat

Full Text ( Final Version , 1mb )