Selected Methods of Model Checking Using SAT and SMT-solvers

The objectives of this research are to further investigate the foundations for novel SMT and SAT-based bounded model checking (BMC) algorithms for real-time and multiagent systems. A major part of the research will involve the development of SMT-based BMC methods for standard Kripke structures, extended Kripke structures, and for different kinds of interpreted systems for different kinds of temporal languages, each of which will be augmented to include the standard epistemic and deontic operators. The algorithms will be implemented into several modules of the model checker VerICS (http://verics.ipipan.waw.pl/).