Nous résumons ici un article paru dans le Journal of Automated Reasoning. Celui-ci présente Pardinus, une extension du model finder relationnel Kodkod au moyen de la logique temporelle linéaire (avec opérateurs du passé). Pardinus inclut un moteur de bounded model-checking basé sur SAT ainsi qu'un moteur de model-checking commplet basé sur SMV, les deux permettant d'itérer sur les instances (ou contre-exemples) d'une spécification. Il offre aussi une stratégie d'analyse « décomposée » parallèle qui améliore l'efficacité des deux moteurs d'analyse.