PV3 AdamMCverifies user-specified properties of Petri nets

Application domain/field

Type of tool

Model checker

Expected input

One of the following three options:
  1. Software-defined network (up to 82 switches) and a Flow-LTL formula
  2. Petri net with transits and a Flow-LTL formula
  3. Petri net and a LTL formula

Format:

Expected output

SAT or UNSAT If it is UNSAT, then a counterexample is visualized with DOT/Graphviz

Internals

Flow-LTL Petri nets

Links

Last commit date

15 May 2020

Related papers

https://doi.org/10.1007/978-3-030-53291-8_5

Last publication date

14 July 2020

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.