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.
- F. Nielson, H.R. Nielson, C. Hankin, Principles of Program Analysis, Springer, 2005.
- K. Apt, E.-R. Olderog, Verification of Sequential and Concurrent Programs. Springer, 1997.
- G. J. Holzmann, The SPIN Model Checker. Pearson Educational, 2003.
- M. Ben-Ari, Principles of the SPIN Model Checker. Springer, 2008.
- G.J. Holzmann, D.A. Peled, An Improvement in Formal Verification. Proc. FORTE 1994.
- G.J. Holzmann, D.A. Peled, M. Yannakakis, On nested depth-first search. Proc. of the 2nd Spin Workshop, pp. 23-32, 1996.
- P. Gastin, D. Oddoux, Fast LTL to Büchi Automata Translation. Proc. CAV'01, LNCS 2102, p. 53-65.
- S. Demri, Ph. Schnoebelen, The Complexity of Propositional Linear Temporal Logics in Simple Cases. Information and Computation 174(1), str. 84-103, 2002.
- 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.
- D. Kroening, E. M. Clarke, K. Yorav, Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking. Proc. DAC 2003, 2003.
- 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.
- T. Ball, S. K. Rajamani, Boolean Programs: A Model and Process for Software Analysis.
- P. Cousot, R. Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. Proc. POPL'77, str. 238—252, 1977.
- N. D. Jones, F. Nielson, Abstract Interpretation: a Semantics-Based Tool for Program Analysis. Handbook of Logic in Computer Science, tom 4, str. 527-636, 1995.
- Abstract Interpretation, strona WWW utrzymywana przez P. Cousot.
- V. D'Silva, D. Kroening, G. Weissenbacher, A Survey of Automated Techniques for Formal Software Verification. IEEE Trans. on CAD of Integrated Circuits and Systems 27(7):1165-1178, 2008.
- G. T. Leavens, Y. Cheon, Design by Contract with JML.
- P. Chalin, J. R. Kiniry, G. T. Leavens, E. Poll, Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2. FMCO 2005, 342-363.
- J. R. Kiniry, G. T. Leavens, E. Poll, A JML Tutorial: Modular Specification and Verification of Functional Behavior for Java. CAV 2007 Tutorial
- K. Rustan, M. Leino, G. Nelson, J.B. Saxe, ESC/Java User’s Manual.
- 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.