|
Size: 1162
Comment:
|
Size: 1155
Comment:
|
| Deletions are marked like this. | Additions are marked like this. |
| Line 5: | Line 5: |
| = Star wiki = | = Separation logic & local reasoning = |
| Line 7: | Line 7: |
| This is a wiki about [[SeparationLogic|separation logic]]. Separation logic is an extension of Hoare's logic oriented to reasoning about mutable data structures (or, programs with dynamically allocated pointers). It enables more compact proofs and specs of imperative programs than before because of its support for local reasoning, where specifications and proofs concentrate on the portion of memory used by a program component, and not the entire global state of the system. |
This is a wiki about [[SeparationLogic|separation logic]], an extension of Hoare's logic oriented to reasoning about mutable data structures (or, programs with dynamically allocated pointers). Separation logic supports ''local reasoning'', where specifications and proofs concentrate on the portion of memory used by a program component, and not the entire global state of the system. |
| Line 19: | Line 17: |
| * [[SLInProofAssistants|SL in proof assistants (Coq,HOL,etc.)]] | |
| Line 23: | Line 22: |
Separation logic & local reasoning
This is a wiki about separation logic, an extension of Hoare's logic oriented to reasoning about mutable data structures (or, programs with dynamically allocated pointers). Separation logic supports local reasoning, where specifications and proofs concentrate on the portion of memory used by a program component, and not the entire global state of the system.
Table of Contents
Concurrent program logics (CSL, RGSep, etc.)
Decidability results
Editing the wiki
To edit the wiki, you first have to create an account and contact Viktor Vafeiadis to grant you write permission. Then, login and click on the "Edit" link to modify a page.