@inbook(alur02,
 author       = {Rajeev Alur and Michael McDougall and Zijiang Yang},
 year         = {2002},
 title        = {Exploiting Behavioral Hierarchy for Efficient Model Checking},
 pages        = {338--342},
 series       = {Lecture Notes in Computer Science},
 publisher    = {Springer},
 doi          = {10.1007/3-540-45657-0_25},
)
@inproceedings(bartha2012verification,
 author       = {Tam\'as Bartha and Andr\'as V\"or\"os and Attila J\'ambor and D\'aniel Darvas},
 year         = {2012},
 title        = {Verification of an Industrial Safety Function Using Coloured {P}etri Nets and Model Checking},
 booktitle    = {Proceedings of the 14th International Conference on Modern Information Technology in the Innovation Processes of the Industrial Enterprises (MITIP 2012)},
 publisher    = {Hungarian Academy of Sciences, Computer and Automation Research Institute},
 pages        = {472--485},
)
@incollection(beyer13,
 author       = {Dirk Beyer and Stefan L\"{o}we},
 year         = {2013},
 title        = {Explicit-State Software Model Checking Based on {CEGAR} and Interpolation},
 booktitle    = {Fundamental Approaches to Software Engineering},
 series       = {Lecture Notes in Computer Science},
 volume       = {7793},
 publisher    = {Springer},
 pages        = {146--162},
 doi          = {10.1007/978-3-642-37057-1_11},
)
@article(purandar2004,
 author       = {Purandar Bhaduri and S. Ramesh},
 year         = {2004},
 title        = {Model Checking of Statechart Models: Survey and Research Directions},
 journal      = {CoRR},
 volume       = {cs.SE/0407038},
 url          = {http://arxiv.org/abs/cs.SE/0407038},
)
@incollection(biere99,
 author       = {Armin Biere and Alessandro Cimatti and Edmund Clarke and Yunshan Zhu},
 year         = {1999},
 title        = {Symbolic Model Checking without {BDD}s},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems},
 series       = {Lecture Notes in Computer Science},
 volume       = {1579},
 publisher    = {Springer},
 pages        = {193--207},
 doi          = {10.1007/3-540-49059-0_14},
)
@book(bradley,
 author       = {Aaron R Bradley and Zohar Manna},
 year         = {2007},
 title        = {The calculus of computation: Decision procedures with applications to verification},
 publisher    = {Springer},
 doi          = {10.1007/978-3-540-74113-8},
)
@article(chan1998,
 author       = {W. Chan and R. J. Anderson and P. Beame and S. Burns and F. Modugno and D. Notkin and J. D. Reese},
 year         = {1998},
 title        = {Model checking large software specifications},
 journal      = {IEEE Transactions on Software Engineering},
 volume       = {24},
 number       = {7},
 pages        = {498--520},
 doi          = {10.1109/32.708566},
)
@article(clarke03,
 author       = {Edmund M Clarke and Orna Grumberg and Somesh Jha and Yuan Lu and Helmut Veith},
 year         = {2003},
 title        = {Counterexample-guided abstraction refinement for symbolic model checking},
 journal      = {Journal of the ACM},
 volume       = {50},
 number       = {5},
 pages        = {752--794},
 doi          = {10.1145/876638.876643},
)
@article(clarke94,
 author       = {Edmund M Clarke and Orna Grumberg and David E Long},
 year         = {1994},
 title        = {Model checking and abstraction},
 journal      = {ACM Transactions on Programming Languages and Systems},
 volume       = {16},
 number       = {5},
 pages        = {1512--1542},
 doi          = {10.1145/186025.186051},
)
@book(clarke99,
 author       = {Edmund M Clarke and Orna Grumberg and Doron Peled},
 year         = {1999},
 title        = {Model checking},
 publisher    = {MIT Press},
)
@article(clarke04,
 author       = {Edmund M Clarke and Anubhav Gupta and Ofer Strichman},
 year         = {2004},
 title        = {{SAT}-based counterexample-guided abstraction refinement},
 journal      = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
 volume       = {23},
 number       = {7},
 pages        = {1113--1123},
 doi          = {10.1109/TCAD.2004.829807},
)
@incollection(graf97,
 author       = {Susanne Graf and Hassen Saidi},
 year         = {1997},
 title        = {Construction of abstract state graphs with {PVS}},
 booktitle    = {Computer Aided Verification},
 series       = {Lecture Notes in Computer Science},
 volume       = {1254},
 publisher    = {Springer},
 pages        = {72--83},
 doi          = {10.1007/3-540-63166-6_10},
)
@incollection(hajdu15,
 author       = {\'Akos Hajdu and Andr\'as V\"or\"os and Tam\'as Bartha},
 year         = {2015},
 title        = {New search strategies for the {P}etri net {CEGAR} approach},
 booktitle    = {Application and Theory of Petri Nets and Concurrency},
 series       = {Lecture Notes in Computer Science},
 volume       = {9115},
 publisher    = {Springer},
 pages        = {309--328},
 doi          = {10.1007/978-3-319-19488-2_16},
)
@article(helke2016,
 author       = {Steffen Helke and Florian Kamm{\"u}ller},
 year         = {2016},
 title        = {Verification of statecharts using data abstraction},
 journal      = {International Journal of Advanced Computer Science and Applications},
 volume       = {7},
 number       = {1},
 pages        = {571--583},
 doi          = {10.14569/IJACSA.2016.070179},
)
@article(latella1999,
 author       = {Diego Latella and Istvan Majzik and Mieke Massink},
 year         = {1999},
 title        = {Automatic Verification of a Behavioural Subset of UML Statechart Diagrams Using the SPIN Model-checker},
 journal      = {Formal Aspects of Computing},
 volume       = {11},
 number       = {6},
 pages        = {637--664},
 doi          = {10.1007/s001659970003},
)
@inproceedings(leucker15,
 author       = {Martin Leucker and Grigory Markin and Neuh\"au{\ss}er, MartinR.},
 year         = {2015},
 title        = {A New Refinement Strategy for {CEGAR}-Based Industrial Model Checking},
 booktitle    = {Hardware and Software: Verification and Testing},
 series       = {Lecture Notes in Computer Science},
 volume       = {9434},
 publisher    = {Springer},
 pages        = {155--170},
 doi          = {10.1007/978-3-319-26287-1_10},
)
@incollection(mcmillan05,
 author       = {K.L. McMillan},
 year         = {2005},
 title        = {Applications of {C}raig Interpolants in Model Checking},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems},
 series       = {Lecture Notes in Computer Science},
 volume       = {3440},
 publisher    = {Springer},
 pages        = {1--12},
 doi          = {10.1007/11494744_2},
)
@phdthesis(meller16,
 author       = {Yael Meller},
 year         = {2016},
 title        = {Model Checking Techniques for Behavioral UML Models},
 school       = {Israel Institute of Technology},
)
@incollection(meller2014,
 author       = {Yael Meller and Orna Grumberg and Karen Yorav},
 year         = {2014},
 title        = {Verifying Behavioral UML Systems via CEGAR},
 booktitle    = {Integrated Formal Methods},
 series       = {Lecture Notes in Computer Science},
 publisher    = {Springer},
 pages        = {139--154},
 doi          = {10.1007/978-3-319-10181-1_9},
)
@incollection(demoura08,
 author       = {Leonardo de Moura and Bj{\o}rner, Nikolaj},
 year         = {2008},
 title        = {{Z3}: An Efficient {SMT} Solver},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems},
 series       = {Lecture Notes in Computer Science},
 volume       = {4963},
 publisher    = {Springer},
 pages        = {337--340},
 doi          = {10.1007/978-3-540-78800-3_24},
)
@article(nemeth2009,
 author       = {Erzs{\'e}bet N{\'e}meth and Tam{\'a}s Bartha and Csaba Fazekas and Katalin M. Hangos},
 year         = {2009},
 title        = {Verification of a primary-to-secondary leaking safety procedure in a nuclear power plant using coloured {P}etri nets},
 journal      = {Reliability Engineering \& System Safety},
 volume       = {94},
 number       = {5},
 pages        = {942--953},
 doi          = {10.1016/j.ress.2008.10.012},
)