K.R. Apt, D.C. Kozen, Limits for automatic program verification, Inform. Process. Lett. 22 (1986) 307-309.
S. Bensalem, Y. Lakhnech, H. Saidi, Powerful Techniques for the Automatic Generation of Invariants, Lect. Notes in Comput. Sci., vol. 1102, Springer, Berlin, 1996, pp. 323-335.
W. Bibel, Deduction - Automated Logic, Academic Press, London, 1993.
N. Bjorner, A. Browne, Z. Manna, Automatic Generation of Invariants and Intermediate Assertions, Lect. Notes in Comput. Sci., vol. 976, Springer, Berlin, 1995, pp. 589-623.
R.E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Trans. Comput. C-35 (1986) 677-691.
J.R. Burch et al., Symbolic model checking: 1020 states and beyond, Proc. 5th. Symp. on Logic in Computer Science, 1990, pp. 428-439.
E. Clarke, Program invariants as fixed points, Proc. 18th IEEE Symp. on Foundations of Comput. Sci., 1977, pp. 18-29.
E. Clarke, E. Emerson, A. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Trans. Programm. Lang. Systems 8 (1986) 244-263.
K.M. Chandy, J. Misra, Parallel Program Design: A Foundation, Addison-Wesley, Reading, MA, 1988.
C.C. Chang, H.J. Keisler, Model Theory, North-Holland, Amsterdam, 1973.
P. Cousot, N. Halbwachs, Automatic discovery of linear restraints among variables of a program, Proc. 5th ACM Symp. on Principles of Programming Languages, 1978, pp. 84-96.
E.W. Dijkstra, A Discipline of Programming, Prentice-Hall, Englewood Cliffs, NJ, 1976.
M. Fitting, First-Order Logic and Automated Theorem Proving, Springer, Berlin, 1990.
D.M. Goldschlag, Mechanically verifying concurrent programs with the Boyer-Moore prover, IEEE Trans. Software Eng. 16 (1990) 1005-1023.
S. Graf, H. Saidi, Verifying Invariants using Theorem Proving, Lect. Notes in Comput. Sci., vol. 1102, Springer, Berlin, 1996, pp. 196-207.
E.P. Gribomont, A Programming Logic for Formal Concurrent Systems, Lect. Notes in Comput. Sci., vol. 458, Springer, Berlin, 1990, pp. 298-313.
E.P. Gribomont, Concurrency without toil: a systematic method for parallel program design, Sci. Comput. Programm. 21 (1993) 1-56.
E.P. Gribomont, D. Rossetto, CAVEAT: Technique and Tool for Computer Aided VErification And Transformation, Lect. Notes in Comput. Sci., vol. 939, Springer, Berlin, 1995, pp. 70-83.
B. Jonsson, L. Kempe, Verifying Safety Properties of a Class of Infinite-State Distributed Algorithms, Lect. Notes in Comput. Sci., vol. 939, Springer, Berlin, 1995, pp. 42-53.
R.P. Kurshan, L. Lamport, Verification of a Multiplier: 64 Bits and Beyond, Lect. Notes in Comput. Sci., vol. 697, Springer, Berlin, 1993, pp. 166-179.
L. Lamport, An assertional correctness proof of a distributed algorithm, Sci. Comput. Programm. 2 (1983) 175-206.
K. Larsen, B. Steffen, C. Weise, A Constraint Oriented Proof Methodology Based on Modal Transitions Systems, Lect. Notes in Comput. Sci., vol. 1019, Springer, Berlin, 1995, pp. 17-40.
K. Larsen, B. Steffen, C. Weise, Fisher's protocol revisited: a simple proof using modal constraints, in: Proc. 4th DIMACS Workshop on Verification and Control of Hybrid Systems, New Brunswick, New Jersey, 22-24 October 1995.
Z. Manna et al., STEP: the Stanford temporal prover (Draft), Report STAN-CS-TR-94-1518, Stanford University, June 1994.
J.S. Moore, Introduction to the OBDD algorithm for the ATP community, J. Automat. Reason. 12 (1994) 33-45.
G. Ricart, A.K. Agrawala, An optimal algorithm for mutual exclusion, Comm. ACM 24 (1981) 9-17 (corrigendum: Comm. ACM 24 (1981) 578).
D.M. Russinoff, A verification system for concurrent programs based on the Boyer-Moore prover, Formal Aspects Comput. 4 (1992) 597-611.
L. Wallen, Automated Deduction in Nonclassical Logics, MIT Press, Cambridge, MA, 1990.
P. Wolper, V. Lovinfosse, Verifying Properties of large Sets of Processes with Network Invariants, Lect. Notes in Comput. Sci., vol. 407, Springer, Berlin, 1990, pp. 68-80.
