Verifying Temporal Relational Models with Pardinus

Abstract

This short paper summarizes an article published in the Journal of Automated Reasoning [7]. It presents (\textsf{Pardinus}), an extension of the popular (\textsf{Kodkod}) [12] relational model finder with linear temporal logic (including past operators) to simplify the analysis of dynamic systems. (\textsf{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.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{MacedoBCC23,
  author       = {Nuno Macedo and
                  Julien Brunel and
                  David Chemouil and
                  Alcino Cunha},
  editor       = {Uwe Gl{\"{a}}sser and
                  Jos{\'{e}} Creissac Campos and
                  Dominique M{\'{e}}ry and
                  Philippe A. Palanque},
  title        = {Verifying Temporal Relational Models with Pardinus},
  booktitle    = {Rigorous State-Based Methods - 9th International Conference, {ABZ}
                  2023, Nancy, France, May 30 - June 2, 2023, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {14010},
  pages        = {254--261},
  publisher    = {Springer},
  year         = {2023},
  url          = {https://doi.org/10.1007/978-3-031-33163-3\_20},
  doi          = {10.1007/978-3-031-33163-3\_20},
  timestamp    = {Tue, 25 Jun 2024 21:03:18 +0200},
  biburl       = {https://dblp.org/rec/conf/zum/MacedoBCC23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}