A beginner guide to Iris, Coq and separation logic
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2021
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866929684189544448 |
|---|---|
| author | Dietrich, Elizabeth |
| author_facet | Dietrich, Elizabeth |
| contents | Creating safe concurrent algorithms is challenging and error-prone. For this reason, a formal verification framework is necessary especially when those concurrent algorithms are used in safety-critical systems. The goal of this guide is to provide resources for beginners to get started in their journey of formal verification using the powerful tool Iris. The difference between this guide and many others is that it provides (i) an in-depth explanation of examples and tactics, (ii) an explicit discussion of separation logic, and (iii) a thorough coverage of Iris and Coq. References to other guides and to papers are included throughout to provide readers with resources through which to continue their learning. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2105_12077 |
| institution | arXiv |
| publishDate | 2021 |
| record_format | arxiv |
| spellingShingle | A beginner guide to Iris, Coq and separation logic Dietrich, Elizabeth Logic in Computer Science Programming Languages Creating safe concurrent algorithms is challenging and error-prone. For this reason, a formal verification framework is necessary especially when those concurrent algorithms are used in safety-critical systems. The goal of this guide is to provide resources for beginners to get started in their journey of formal verification using the powerful tool Iris. The difference between this guide and many others is that it provides (i) an in-depth explanation of examples and tactics, (ii) an explicit discussion of separation logic, and (iii) a thorough coverage of Iris and Coq. References to other guides and to papers are included throughout to provide readers with resources through which to continue their learning. |
| title | A beginner guide to Iris, Coq and separation logic |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2105.12077 |