Towards Concurrent Quantitative Separation Logic
Fuente:
arXiv
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2022
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866910624497270784 |
|---|---|
| author | Fesefeldt, Ira Katoen, Joost-Pieter Noll, Thomas |
| author_facet | Fesefeldt, Ira Katoen, Joost-Pieter Noll, Thomas |
| contents | In this paper, we develop a novel verification technique to reason about programs featuring concurrency, pointers and randomization. While the integration of concurrency and pointers is well studied, little is known about the combination of all three paradigms. To close this gap, we combine two kinds of separation logic -- Quantitative Separation Logic and Concurrent Separation Logic -- into a new separation logic that enables reasoning about lower bounds of the probability to realise a postcondition by executing such a program. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2207_02822 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | Towards Concurrent Quantitative Separation Logic Fesefeldt, Ira Katoen, Joost-Pieter Noll, Thomas Logic in Computer Science Programming Languages In this paper, we develop a novel verification technique to reason about programs featuring concurrency, pointers and randomization. While the integration of concurrency and pointers is well studied, little is known about the combination of all three paradigms. To close this gap, we combine two kinds of separation logic -- Quantitative Separation Logic and Concurrent Separation Logic -- into a new separation logic that enables reasoning about lower bounds of the probability to realise a postcondition by executing such a program. |
| title | Towards Concurrent Quantitative Separation Logic |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2207.02822 |