Verics is a model-checking tool developed at the Institute of Computer Science, Polish Academy of Sciences. It is aimed for verifying timed and multi-agent systems modeled by networks of communicating automata. Also high-level input languages are supported. Verics is composed of several indepentent modules. Concerning the verification, its major part constitute SAT-based model-checking algorithms. 

  • Here can be downloaded tools and benchmarks for BMC of LTLK over Interpreted Systems.
  • Here you can download the benchmarks for Bounded Model Checking of Distributed Time Petri Nets

Back to top