|
Size: 1159
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: |
| = WikiName Wiki = | = Separation logic & local reasoning = |
| Line 7: | Line 7: |
| What is this wiki about? Interesting starting points: * RecentChanges: see where people are currently working * WikiSandBox: feel free to change this page and experiment with editing * FindPage: find some content, explore the wiki * HelpOnMoinWikiSyntax: quick access to wiki markup Here is an example how to use the Latex extension installed: <<latex(\usepackage{dsfont} % $$\mathds{C}$$)>> |
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 20: | Line 12: |
| == How to use this site == | |
| Line 22: | Line 13: |
| A Wiki is a collaborative site, anyone can contribute and share: * Edit any page by pressing '''<<GetText(Edit)>>''' at the top or the bottom of the page * Create a link to another page with joined capitalized words (like WikiSandBox) or with {{{[[words in brackets]]}}} * Search for page titles or text within pages using the search box at the top of any page * See HelpForBeginners to get you going, HelpContents for all help pages. |
=== Table of Contents === |
| Line 28: | Line 15: |
| To learn more about what a WikiWikiWeb is, read about MoinMoin:WhyWikiWorks and the MoinMoin:WikiNature. | * [[SeparationLogic|Basics of separation logic]] * [[EarlyDays|Prehistory and Early Days]] * [[Concurrency|Concurrent program logics]] (CSL, RGSep, etc.) * [[ContextLogic|Context logic]] * [[AbstractPredicates|Abstract predicates]] * [[Decidability]] results * [[ToolSupport|Verification tools based on SL]] * [[SLInProofAssistants|SL in proof assistants (Coq,HOL,etc.)]] * [[SLInProgramAnalysis|Program Analysis based on SL]] |
| Line 30: | Line 25: |
| This wiki is powered by [[http://moinmo.in/|MoinMoin]]. | === Editing the wiki === 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.