References

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

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org