Literatura


Książki nt. model-checkingu, dowodzenia poprawności i analizy programów:
  • 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.

LTL, omega-automaty i SPIN:

Symboliczna weryfikacja modelowa i SMV:

Ograniczona weryfikacja modelowa:

Abstrakcja:

JML:

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: