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

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

1 2 next

  1. Belardinelli, Francesco; Condurache, Rodica; Dima, Cătălin; Jamroga, Wojciech; Knapik, Michal: Bisimulations for verifying strategic abilities with an application to the ThreeBallot voting protocol (2021)
  2. Belardinelli, Francesco; Demri, Stéphane: Strategic reasoning with a bounded number of resources: the quest for tractability (2021)
  3. Belardinelli, Francesco; Lomuscio, Alessio; Murano, Aniello; Rubin, Sasha: Verification of multi-agent systems with public actions against strategy logic (2020)
  4. Čermák, Petr; Lomuscio, Alessio; Mogavero, Fabio; Murano, Aniello: Practical verification of multi-agent systems against \textscSlkspecifications (2018)
  5. Ezekiel, J.; Lomuscio, A.: Combining fault injection and model checking to verify fault tolerance, recoverability, and diagnosability in multi-agent systems (2017)
  6. Belardinelli, Francesco; Lomuscio, Alessio: A three-value abstraction technique for the verification of epistemic properties in multi-agent systems (2016)
  7. Chen, Qingliang; Su, Kaile; Sattar, Abdul; Luo, Xiangyu; Chen, Aixiang: A first-order coalition logic for BDI-agents (2016)
  8. Kouvaros, Panagiotis; Lomuscio, Alessio: Parameterised verification for multi-agent systems (2016)
  9. van der Meyden, Ron; Patra, Manas K.: Undecidable cases of model checking probabilistic temporal-epistemic logic (extended abstract) (2016)
  10. Jamroga, Wojciech; Penczek, Wojciech: Specification and verification of multi-agent systems (2012)
  11. Gammie, Peter: Verified synthesis of knowledge-based programs in finite synchronous environments (2011)
  12. Huang, Xiaowei; Luo, Cheng; van der Meyden, Ron: Improved bounded model checking for a fair branching-time temporal epistemic logic (2011)
  13. Lomuscio, Alessio; Qu, Hongyang; Russo, Francesco: Automatic data-abstraction in model checking multi-agent systems (2011)
  14. Dechesne, Francien; Wang, Yanjing: To know or not to know: Epistemic approaches to security protocol verification (2010)
  15. Jongmans, Sung-Shik T. Q.; Hindriks, Koen V.; van Riemsdijk, M. Birna: Model checking agent programs by using the program interpreter (2010) ioport
  16. Knapik, Michał; Niewiadomski, Artur; Penczek, Wojciech; Półrola, Agata; Szreter, Maciej; Zbrzezny, Andrzej: Parametric model checking with VerICS (2010)
  17. Lomuscio, Alessio; Penczek, Wojciech; Qu, Hongyang: Partial order reductions for model checking temporal-epistemic logics over interleaved multi-agent systems (2010)
  18. Penczek, Wojciech; Pòłrola, Agata; Zbrzezny, Andrzej: SAT-based (parametric) reachability for a class of distributed time Petri nets (2010)
  19. Boureanu, Ioana; Cohen, Mika; Lomuscio, Alessio: Automatic verification of temporal-epistemic properties of cryptographic protocols (2009)
  20. Cohen, Mika; Dam, Mads; Lomuscio, Alessio; Qu, Hongyang: A data symmetry reduction technique for temporal-epistemic logic (2009)

1 2 next