Forward with separation logic

Abstract

The use of Hoare logic in combination with weakest preconditions and strongest postconditions is a standard tool for program verification, known as backward and forward reasoning. Separation logic, an extension of Hoare logic, finds countless applications in the areas of program verification, but the requirement of frame calculation when using it as an assertion language for specifications limits automation. In this thesis, we develop techniques to allow backward and forward reasoning for separation logic. While the former was known, it required the use of separating implication, an operator of separation often left unsupported. We provide the required support for separating implication, and demonstrate that it is an effective technique for backward reasoning in separation logic by applying it to a case study: the system initialiser proof for the microkernel seL4. We discovered separating coimplication, which, as the dual of separating conjunction and the adjoint of septraction, completes the set of separation logic operators. We demonstrate that it can be used for forward reasoning in separation logic, allowing the choice of forward or backward reasoning to be determined by what is suitable for the program and properties being proved, not the limitations of separation logic. Our technique for forward reasoning, in standard separation logic, is limited to the setting of partial correctness. As strongest postconditions do not exist in general in total correctness, we target general correctness, which unifies partial and total correctness. To support forward reasoning in this setting, separation logic needs to be equipped with a failure element. We present several ways on how to add such an element. We show that none of the obvious extensions preserve all the algebraic properties desired. We develop more complicated models, satisfying the desired properties, and discuss their use for forward reasoning. We implement our framework, including all of the above, in the interactive proof assistant Isabelle/HOL, and enable automation with several interactive proof tactics.