Verifying Temporal Relational Models with Pardinus

• Type: Article in International Conference Proceedings Book
• Date: 2023

Authors

Macedo, N (Author) FEUP; Brunel, J (Author) Other; Chemouil, D (Author) Other; Cunha, A (Author) Other

Conference proceedings International

Title: RIGOROUS STATE-BASED METHODS, ABZ 2023

Pages: 254-261

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

Nancy, FRANCE, MAY 30-JUN 02, 2023

Indexing

ISI Web of Knowledge - 0 Citations

Scopus

Other information

Authenticus ID: 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.

Language: English

Type (Professor's evaluation): Scientific

No. of pages: 8