Pardinus: A Temporal Relational Model Finder

• Type: Article in International Scientific Journal
• Date: 2022

Authors

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

Journal

Title: Journal of Automated Reasoning

Vol. 66

Pages: 861-904

ISSN: 0168-7433

Publisher: Springer Nature

Indexing

ISI Web of Knowledge - 0 Citations

Scopus - 0 Citations

Other information

Authenticus ID: P-00X-4SJ

DOI: 10.1007/s10817-022-09642-2

Abstract (EN): 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.

Language: English

Type (Professor's evaluation): Scientific

No. of pages: 44