Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/89201| Título: | Pardinus: a temporal relational model finder |
| Autor(es): | Macedo, Nuno Brunel, Julien Chemouil, David Cunha, Alcino |
| Palavras-chave: | Model checking Model finding Relational logic Temporal logic |
| Data: | 2022 |
| Editora: | Springer |
| Revista: | Journal of Automated Reasoning |
| Citação: | Macedo, N., Brunel, J., Chemouil, D. et al. Pardinus: A Temporal Relational Model Finder. J Autom Reasoning 66, 861–904 (2022). https://doi.org/10.1007/s10817-022-09642-2nder. Journal of Automated Reasoning. Springer Science and Business Media LLC. http://doi.org/10.1007/s10817-022-09642-2 |
| Resumo(s): | This article presents Pardinus, an extension of the popular Kodkod relational model finder with linear temporal logic (including past operators), to simplify the analysis of dynamic systems. Pardinus includes a SAT-based bounded-model checking engine and an SMV-based complete model checking engine, both allowing iteration through the different instances (or counter-examples) of a specification. It also supports a decomposed parallel analysis strategy that improves the efficiency of both analysis engines on commodity multi-core machines. |
| Tipo: | Artigo |
| URI: | https://hdl.handle.net/1822/89201 |
| DOI: | 10.1007/s10817-022-09642-2 |
| ISSN: | 0168-7433 |
| Versão da editora: | https://link.springer.com/article/10.1007/s10817-022-09642-2 |
| Arbitragem científica: | yes |
| Acesso: | Acesso aberto |
| Aparece nas coleções: |
