Verics

√erics: A Tool for Verifying Timed Automata and Estelle Specifications. The paper presents a new tool for automated verification of Timed Automata as well as protocols written in the specification language Estelle. The current version offers an automatic translation from Estelle specifications to timed automata, and two complementary methods of reachability analysis. The first one is based on Bounded Model Checking (BMC), while the second one is an on-the-fly verification on an abstract model of the system.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 6 articles )

Showing results 1 to 6 of 6.
Sorted by year (citations)

  1. Bouyer, Patricia; Fahrenberg, Uli; Larsen, Kim Guldstrand; Markey, Nicolas; Ouaknine, Joël; Worrell, James: Model checking real-time systems (2018)
  2. Jamroga, Wojciech; Penczek, Wojciech: Specification and verification of multi-agent systems (2012)
  3. Lomuscio, Alessio; Penczek, Wojciech: Symbolic model checking for temporal-epistemic logic (2012)
  4. Belardinelli, F.; Lomuscio, A.: Quantified epistemic logics for reasoning about knowledge in multi-agent systems (2009)
  5. Lomuscio, Alessio; Penczek, Wojciech; Qu, Hongyang: Towards partial order reduction for model checking temporal epistemic logic (2009)
  6. Dembiński, Piotr; Janowska, Agata; Janowski, Paweł; Penczek, Wojciech; Półrola, Agata; Szreter, Maciej; Wozna, Bozena; Zbrzezny, Andrzej: (\surd)erics: A tool for verifying timed automata and Estelle specifications (2003)