Literature

Books:

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-automata and SPIN:

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.

Symbolic model-checking and 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.

Bounded model-checking:

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, F. Lerda, A Tool for Checking ANSI-C Programs. Proc. TACAS 2004, 2004.
D. Kroening, E. M. Clarke, K. Yorav, Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking. Proc. DAC 2003, 2003.

Abstraction:

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, technical report, Microsoft research, 2000.
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.

JML:

Timed automata:

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.

Probabilistic verification:

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.

Computer aided verification