Towards algebraic separation logic
- We present an algebraic approach to separation logic. In particular, we give algebraic characterisations for different classes of separation logic assertions and prove abstract laws fully algebraically. The algebraic view does not only yield new insights on separation logic but also shortens proofs due to a pointfree representation and enables the use of automated theorem provers for verifying properties at a more abstract level.
Download full text files
Postprint
Statistics
Additional Services
| Author: | Han-Hing Dang, Peter Höfner, Bernhard MöllerGND |
|---|---|
| URN: | urn:nbn:de:bvb:384-opus4-689038 |
| Frontdoor URL | https://opus.bibliothek.uni-augsburg.de/opus4/68903 |
| ISBN: | 9783642046384OPAC |
| ISBN: | 9783642046391OPAC |
| ISSN: | 0302-9743OPAC |
| ISSN: | 1611-3349OPAC |
| Parent Title (English): | Lecture Notes in Computer Science |
| Publisher: | Springer |
| Place of publication: | Berlin |
| Type: | Article |
| Language: | English |
| Year of first Publication: | 2009 |
| Publishing Institution: | Universität Augsburg |
| Release Date: | 2020/01/20 |
| Volume: | 5827 |
| First Page: | 59 |
| Last Page: | 72 |
| DOI: | https://doi.org/10.1007/978-3-642-04639-1_5 |
| Institutes: | Fakultät für Angewandte Informatik |
| Fakultät für Angewandte Informatik / Institut für Informatik | |
| Fakultät für Angewandte Informatik / Institut für Informatik / Professur für Programmiermethodik und Multimediale Informationssysteme | |
| Dewey Decimal Classification: | 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik |
| Licence (German): |  Deutsches Urheberrecht |
