Labelled sequent calculi and automated reasoning for assertions in separation logic
Separation logic (SL) is an extension of Hoare logic to reason about programs with mutable data structures. This thesis studies automated reasoning for the assertional language (i.e., formulae that represent pre- and post-conditions) of separation logic. We start from the core of separation logic called Boolean BI (BBI), then consider various propositional abstract separation logics (PASLs) as extensions of BBI. These logics are "abstract" because they are independent of any particular concrete...[Show more]
|Collections||Open Access Theses|
|b37881504_H?u_Zh?.pdf||492.53 MB||Adobe PDF|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.