Affiliations: Technical University of Bialystok, FCS, Wiejska 45a,
15-351 Bialystok, Poland | University of Podlasie, ICS, Sienkiewicza 51, 08-110
Siedlce, Poland | ICS PAS, Ordona 21, 01-237 Warsaw, Poland | University of Lodz, FMCS, Banacha 22, 90-238 Lodz,
Poland | ICS PAS, Ordona 21, 01-237 Warsaw, Poland | Jan Dlugosz University in Czestochowa, IMCS, Armii
Krajowej 13/15, 42-200 Czestochowa, Poland
Note: [] Address for correspondence: The VerICS Group, ICS PAS, Ordona
21, 01-237 Warsaw, Poland; verics@ipipan.waw.pl
Abstract: The papers presents the current stage of the development of VerICS -
a model checker for real-time and multi-agent systems. Depending on the type of
a system considered, it enables to test various classes of properties - from
reachability to temporal, epistemic and deontic formulas. The model checking
methods used to this aim include both SAT-based and enumerative ones. In the
paper we focus on new features of the verifier: SAT-based model checking for
multi-agent systems and several extensions and improvements to real-time
systems' verification.
