Verifying Temporal Relational Models with Pardinus.

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.