Pardinus: a temporal relational model finder

DOI10.1007/S10817-022-09642-2MaRDI QIDQ2102939zbMATH OpenOpenAlexFDO

Authors Nuno Macedo, Julien Brunel, David Chemouil, Alcino Cunha

Publication date 12 December 2022

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-022-09642-2

zbMATH Keywords

model checkingtemporal logicrelational logicmodel finding

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Model checking of probabilistic and nondeterministic systems
• scientific article; zbMATH DE number 1956570
• scientific article; zbMATH DE number 1305046
• scientific article; zbMATH DE number 2196601
• Symbolic model checking: \(10^{20}\) states and beyond

Cites work

• scientific article; zbMATH DE number 1956570 (Why is no real title available?)
• An improved algorithm for decentralized extrema-finding in circular configurations of processes
• CompoSAT: specification-guided coverage for model finding
• Exploiting partial knowledge for efficient model analysis
• Exploring theories with a model-finding assistant
• Fundamental Approaches to Software Engineering
• Generating effective symmetry-breaking predicates for search problems
• Kodkod: A Relational Model Finder
• Reasoning with temporal logic on truncated paths.
• Relational constraint solving in SMT
• Temporal logics in computer science. Finite-state systems

Cited in

(1)

• Kodkod: A Relational Model Finder

Describes a project that uses

Uses Software

• MiniSat
• SPIN
• NuSMV
• Prover9
• Mace4
• ProB
• Kodkod
• nuXmv
• CompoSAT

This page was built for publication: Pardinus: a temporal relational model finder

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2102939)