Verifying Temporal Relational Models with Pardinus

• Tipo: Artigo em Livro de Atas de Conferência Internacional
• Data: 2023

Autores

Macedo, N (Autor) FEUP; Brunel, J (Autor) Outra; Chemouil, D (Autor) Outra; Cunha, A (Autor) Outra

Ata de Conferência Internacional

Título: RIGOROUS STATE-BASED METHODS, ABZ 2023

Páginas: 254-261

9th International Conference on Rigorous State-Based Methods (ABZ)

Nancy, FRANCE, MAY 30-JUN 02, 2023

Indexação

ISI Web of Knowledge - 0 Citações

Scopus

Outras Informações

ID Authenticus: P-00Y-FJW

DOI: 10.1007/978-3-031-33163-3_20

Abstract (EN): This short paper summarizes an article published in the Journal of Automated Reasoning [7]. It presents Pardinus, an extension of the popular Kodkod [12] 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 counterexamples) of a specification. It also supports a decomposed parallel analysis strategy that improves the efficiency of both analysis engines on commodity multi-core machines.

Idioma: Inglês

Tipo (Avaliação Docente): Científica

Nº de páginas: 8