Literatura
- E.M. Clarke, O. Grumberg, D.A. Peled, Model Checking. MIT Press, 2002.
- B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, P. Schnoebelen, P. McKenzie, Systems and Software Verification. Springer, 2001.
- C. Baier, J.-P. Katoen , Principles of Model Checking. MIT Press, 2008.
- G. J. Holzmann, The SPIN Model Checker. Pearson Educational, 2003.
- G.J. Holzmann, D.A. Peled, An Improvement in Formal Verification. Proc. FORTE 1994. (PDF)
- G.J. Holzmann, D.A. Peled, M. Yannakakis, On nested depth-first search. Proc. of the 2nd Spin Workshop, pp. 23-32, 1996. (PDF)
- P. Gastin, D. Oddoux, Fast LTL to Büchi Automata Translation. Proc. CAV'01, LNCS 2102, p. 53-65. (PDF)
- S. Demri, Ph. Schnoebelen, The Complexity of Propositional Linear Temporal Logics in Simple Cases. Information and Computation 174(1), str. 84-103, 2002. (PDF)
- E. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith, Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752-794, 2003.
- E. Clarke, O. Grumberg, D. Long, Verification tools for finite-state concurrent systems. In: A Decade of concurrency--Reflections and Perspectives, LNCS 803, 1994.
- K.L.McMillan, Symbolic Model Checking. praca doktorska, 1992.
- R. E. Bryant, Symbolic boolean manipulation with ordered binary decision diagrams. ACM Computing Surveys 24(3):293-318, 1992.
- A. Biere, A. Cimatti, E.M. Clarke, O. Strichman, Y. Zhu, Bounded Model Checking. Advances in Computers 58, 2003.
- E. M. Clarke, A. Biere, R. Raimi, Y. Zhu, Bounded Model Checking Using Satisfiability Solving. Formal Methods in System Design 19(1): 7-34 (2001)
- R. Alur, D. L. Dill, A Theory of Timed Automata. Theoretical Computer Science 125:183-235, 1994.
- R. Alur, Timed Automata. Proc. CAV'99, LNCS 1633, 8-22, Springer, 1999.
- J. Bengtsson, W. Yi, Timed Automata: Semantics, Algorithms and Tools. Lecture Notes on Concurrency and Petri Nets, LNCS 3098, Springer-Verlag, 2004.
- M. Kwiatkowska, Model checking for probability and time: from theory to practice. Proc. LICS'03, pp. 351-360, 2003.
- D. Parker, Implementation of Symbolic Model Checking for Probabilistic Systems. Praca doktorska, Uniwersytet w Birmingham, 2002.
- A. Miner and D. Parker, Symbolic Representations and Analysis of Large Probabilistic Systems. Proc. Validation of Stochastic Systems: A Guide to Current Research, LNCS 2925, 2004.
- M. Fujita, P.C. McGeer, J.C.-Y. Yang, Multi-Terminal Binary Decision Diagrams: An Efficient Data Structure for Matrix Representation. Formal Methods in System Design 10:149-169, 1997.