Sciweavers

Share
PAAMS
2015
Springer

Selected Methods of Model Checking Using SAT and SMT-Solvers

3 years 3 months ago
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/). Categories and Subject Descriptors D.2.4 [Software/Program Verification]: Model checking Keywords Bounded model checking, SMT, SAT, Temporal Logic, PhD xtended abstract
Agnieszka M. Zbrzezny
Added 16 Apr 2016
Updated 16 Apr 2016
Type Journal
Year 2015
Where PAAMS
Authors Agnieszka M. Zbrzezny
Comments (0)
books