Literatura
Książki nt. model-checkingu:
- 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.
LTL, omega-automaty i SPIN:
- 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)
Symboliczna weryfikacja modelowa i SMV:
- 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.
Ograniczona weryfikacja modelowa:
- 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)
Automaty czasowe:
- 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.
Weryfikacja probabilistyczna:
- 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.