|
Size: 1162
Comment:
|
← Revision 18 as of 2013-04-18 12:27:53 ⇥
Size: 1439
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]]. | 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). The 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. The general context of the work is methods for reasoning about programs. This wiki does not provide background on the general issue, for which the reader can search on the web for such topics as logics of programs, Hoare logic, program verification, and so on. |
| Line 9: | Line 11: |
| 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. | |
| Line 14: | Line 16: |
| * [[EarlyDays|Prehistory and Early Days]] | |
| Line 19: | Line 22: |
| * [[SLInProofAssistants|SL in proof assistants (Coq,HOL,etc.)]] * [[SLInProgramAnalysis|Program Analysis based on SL]] |
|
| Line 22: | Line 27: |
| To edit the wiki, you first have to ''<<Action(newaccount,create an account)>>'' and contact [[http://www.mpi-sws.org/~viktor/|Viktor Vafeiadis]] to grant you write permission. Then, login and click on the "Edit" link to modify a page. |
To edit the wiki, you have to contact [[http://www.mpi-sws.org/~viktor/|Viktor Vafeiadis]] to get an account. Then, login and click on the "Edit" link to modify a page. |
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). The 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.
The general context of the work is methods for reasoning about programs. This wiki does not provide background on the general issue, for which the reader can search on the web for such topics as logics of programs, Hoare logic, program verification, and so on.
Table of Contents
Concurrent program logics (CSL, RGSep, etc.)
Decidability results
Editing the wiki
To edit the wiki, you have to contact Viktor Vafeiadis to get an account. Then, login and click on the "Edit" link to modify a page.