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 30 articles , 1 standard article )

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

1 2 next

  1. Čermák, Petr; Lomuscio, Alessio; Mogavero, Fabio; Murano, Aniello: Practical verification of multi-agent systems against Slk specifications (2018)
  2. Ezekiel, J.; Lomuscio, A.: Combining fault injection and model checking to verify fault tolerance, recoverability, and diagnosability in multi-agent systems (2017)
  3. Belardinelli, Francesco; Lomuscio, Alessio: A three-value abstraction technique for the verification of epistemic properties in multi-agent systems (2016)
  4. Kouvaros, Panagiotis; Lomuscio, Alessio: Parameterised verification for multi-agent systems (2016)
  5. Jamroga, Wojciech; Penczek, Wojciech: Specification and verification of multi-agent systems (2012)
  6. Gammie, Peter: Verified synthesis of knowledge-based programs in finite synchronous environments (2011)
  7. Huang, Xiaowei; Luo, Cheng; van der Meyden, Ron: Improved bounded model checking for a fair branching-time temporal epistemic logic (2011)
  8. Lomuscio, Alessio; Qu, Hongyang; Russo, Francesco: Automatic data-abstraction in model checking multi-agent systems (2011)
  9. Dechesne, Francien; Wang, Yanjing: To know or not to know: Epistemic approaches to security protocol verification (2010)
  10. Jongmans, Sung-Shik T. Q.; Hindriks, Koen V.; van Riemsdijk, M. Birna: Model checking agent programs by using the program interpreter (2010) ioport
  11. Knapik, Michał; Niewiadomski, Artur; Penczek, Wojciech; Półrola, Agata; Szreter, Maciej; Zbrzezny, Andrzej: Parametric model checking with VerICS (2010)
  12. Lomuscio, Alessio; Penczek, Wojciech; Qu, Hongyang: Partial order reductions for model checking temporal-epistemic logics over interleaved multi-agent systems (2010)
  13. Penczek, Wojciech; Pòłrola, Agata; Zbrzezny, Andrzej: SAT-based (parametric) reachability for a class of distributed time Petri nets (2010)
  14. Boureanu, Ioana; Cohen, Mika; Lomuscio, Alessio: Automatic verification of temporal-epistemic properties of cryptographic protocols (2009)
  15. Cohen, Mika; Dam, Mads; Lomuscio, Alessio; Qu, Hongyang: A data symmetry reduction technique for temporal-epistemic logic (2009)
  16. Kurkowski, Mirosław; Penczek, Wojciech: Timed automata based model checking of timed security protocols (2009)
  17. Rataj, Artur; Woźna, Bożena; Zbrzezny, Andrzej: A translator of Java programs to TADDs (2009)
  18. Bryans, Jeremy W.; Koutny, Maciej; Mazaré, Laurent; Ryan, Peter Y. A.: Opacity generalised to transition systems (2008) ioport
  19. Janowska, Agata; Janowski, Paweł; Wróblewski, Dobiesław: Translation of intermediate language to timed automata with discrete data (2008)
  20. 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)

1 2 next