You are here

Parametric Model Checking

Three Verics modules are aimed at parametric verification. Bounded Model Checking, a symbolic method based on encoding problems in propositional formulas and testing their SATisfiability, has been extended to deal with parametric properties. Input languages include:

  • 1-safe fragment of Elementary Net Systems (module PNTools)
  • 1-safe fragment of Time Petri Nets (module TPNTools)
  • UML State Machines (module UML2SAT)

The modules are now included in the main release, available for download

    Back to top