VerICS

Verics (VerICS) is our original tool for automated verification of Timed Automata and protocols written in a subset of the specification language Estelle, developed as a part of the research project Automated Verification of Time Dependent Systems held in the Institute of Computer Science of Polish Academy of Sciences (ICS PAS). As an input for Verics, an Estelle specification, a specification in our original intermediate language (IL), or Timed Automata in the Kronos-like format can be used. A specification can be translated to timed automata, which are passed to other Verics components. for examples of inputs see here For today, reachability analysis is available. For disproving safety properties, a new efficient method consisting in translating the reachability problem for Timed Automata to the satisfiability problem of propositional formulas (SAT-problem) is used. For proving correctness, an (on-the-fly) reachability analysis on an abstract model of the system is performed.


References in zbMATH (referenced in 25 articles , 1 standard article )

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

1 2 next

  1. Kouvaros, Panagiotis; Lomuscio, Alessio: Parameterised verification for multi-agent systems (2016)
  2. Huang, Xiaowei; Luo, Cheng; van der Meyden, Ron: Improved bounded model checking for a fair branching-time temporal epistemic logic (2011)
  3. Lomuscio, Alessio; Qu, Hongyang; Russo, Francesco: Automatic data-abstraction in model checking multi-agent systems (2011)
  4. Dechesne, Francien; Wang, Yanjing: To know or not to know: Epistemic approaches to security protocol verification (2010)
  5. Jongmans, Sung-Shik T.Q.; Hindriks, Koen V.; van Riemsdijk, M.Birna: Model checking agent programs by using the program interpreter (2010)
  6. Knapik, Michał; Niewiadomski, Artur; Penczek, Wojciech; Półrola, Agata; Szreter, Maciej; Zbrzezny, Andrzej: Parametric model checking with VerICS (2010)
  7. Lomuscio, Alessio; Penczek, Wojciech; Qu, Hongyang: Partial order reductions for model checking temporal-epistemic logics over interleaved multi-agent systems (2010)
  8. Penczek, Wojciech; Pòłrola, Agata; Zbrzezny, Andrzej: SAT-based (parametric) reachability for a class of distributed time Petri nets (2010)
  9. Boureanu, Ioana; Cohen, Mika; Lomuscio, Alessio: Automatic verification of temporal-epistemic properties of cryptographic protocols (2009)
  10. Cohen, Mika; Dam, Mads; Lomuscio, Alessio; Qu, Hongyang: A data symmetry reduction technique for temporal-epistemic logic (2009)
  11. Kurkowski, Mirosław; Penczek, Wojciech: Timed automata based model checking of timed security protocols (2009)
  12. Rataj, Artur; Woźna, Bożena; Zbrzezny, Andrzej: A translator of Java programs to TADDs (2009)
  13. Bryans, Jeremy W.; Koutny, Maciej; Mazaré, Laurent; Ryan, Peter Y.A.: Opacity generalised to transition systems (2008)
  14. Janowska, Agata; Janowski, Paweł; Wróblewski, Dobiesław: Translation of intermediate language to timed automata with discrete data (2008)
  15. Kacprzak, Magdalena; Nabiałek, Wojciech; Niewiadomski, Artur; Penczek, Wojciech; Półrola, Agata; Szreter, Maciej; Woźna, Bożena; Zbrzezny, Andrzej: VERICS 2007 -- a model checker for knowledgee and real-time (2008)
  16. Nabiałek, Wojciech; Janowska, Agata; Janowski, Paweł: Translation of timed Promela to timed automata with discrete data (2008)
  17. Penczek, Wojciech; Szreter, Maciej: SAT-based unbounded model checking of timed automata (2008)
  18. Zbrzezny, Andrzej; Woźna, Bożena: Towards verification of Java programs in VerICS (2008)
  19. Lomuscio, Alessio; Penczek, Wojciech; Woźna, Bożena: Bounded model checking for knowledge and real time (2007)
  20. Lomuscio, Alessio; Raimondi, Franco; Woźna, Bożena: Verification of the TESLA protocol in MCMAS-X (2007)

1 2 next