Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/78595| Título: | Why3-do: The way of harmonious distributed system proofs |
| Autor(es): | Lourenço, Cláudio Belo Pinto, Jorge Sousa |
| Data: | Jan-2022 |
| Editora: | Springer International Publishing AG |
| Revista: | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
| Citação: | Lourenço, C.B., Pinto, J.S. (2022). Why3-do: The Way of Harmonious Distributed System Proofs. In: Sergey, I. (eds) Programming Languages and Systems. ESOP 2022. Lecture Notes in Computer Science, vol 13240. Springer, Cham. https://doi.org/10.1007/978-3-030-99336-8_5 |
| Resumo(s): | We study principles and models for reasoning inductively about properties of distributed systems, based on programmed atomic handlers equipped with contracts. We present the Why3-do library, leveraging a state of the art software verifier for reasoning about distributed systems based on our models. A number of examples involving invariants containing existential and nested quantifiers (including Dijsktra’s self-stabilizing systems) illustrate how the library promotes contract-based modular development, abstraction barriers, and automated proofs. |
| Tipo: | Artigo em ata de conferência |
| URI: | https://hdl.handle.net/1822/78595 |
| ISBN: | 9783030993351 |
| DOI: | 10.1007/978-3-030-99336-8_5 |
| ISSN: | 0302-9743 |
| Versão da editora: | https://link.springer.com/chapter/10.1007/978-3-030-99336-8_5 |
| Arbitragem científica: | yes |
| Acesso: | Acesso aberto |
| Aparece nas coleções: |
Ficheiros deste registo:
| Ficheiro | Descrição | Tamanho | Formato | |
|---|---|---|---|---|
| why3do-ESOP22.pdf | 414,74 kB | Adobe PDF | Ver/Abrir |
