Abdulla, P.A., Bouajjani, A., Jonsson, B., Nilsson, M., Handling global conditions in parametrized system verification (1999) Lecture Notes in Computer Science, 1633, pp. 134-145. , Computer Aided Verification Conference, Springer-Verlag, July
Apt, K.R., Kozen, D.C., Limits for automatic verification of finite-state concurrent systems (1986) Information Processing Letters, 22 (6), pp. 307-309. , May
Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L., Parameterized verification with automatically computed inductive assertions (2001) Lecture Notes in Computer Science, 2102, pp. 221-234. , Computer Aided Verification, Springer-Verlag, July
Baukus, K., Lakhnech, Y., Stahl, K., Verification of Parameterized Protocols (2001) Journal of Universal Computer Science, 7 (2), pp. 141-158. , Feb
Bernays, P., Schönfinkel, M., Zum Entscheidungsproblem der mathematischen Logik (1928) Math. Annalen, 99, pp. 342-372
Bjørner, N.S., Manna, Z., Sipma, H.B., Uribe, T.E., Deductive verification of real-time systems using STeP (2001) TCS: Theoretical Computer Science, 253
Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T., Regular model checking (2000) Lecture Notes in Computer Science, 1855, pp. 403-418. , Computer Aided Verification, Springer-Verlag, July
Dijkstra, E.W., (1976) A Discipline of Programming, , Prentice-Hall
Dreben, B., Goldfarb, W.D., (1979) The Decision Problem: Solvable Classes of Quantificational Formulas, , Addison-Wesley, Reading, Massachusetts
Emerson, E.A., Namjoshi, K.S., Automatic verification of parameterized synchronous systems (1996) Computer Aided Verification, 1102, pp. 87-98. , Springer-Verlag, July
Ebbinghaus, H.-D., Flum, J., Finite Model Theory (1995) Perspectives in Mathematical Logic, , Springer-Verlag, Berlin
Enderton, H.B., (1972) A Mathematical Introduction to Logic, , Academic Press, Inc., Orlando, Florida
Fitting, M., (1990) First-Order Logic and Automated Theorem Proving, , Springer-Verlag, Berlin
Fontaine, P., Gribomont, E.P., Using BDDs with combinations of theories (2002) Lecture Notes in Computer Science, 2514. , Logic for Programming, Artificial Intelligence, and Reasoning, Springer
Gallier, J., Narendran, P., Raatz, S., Snyder, W., Theorem proving using equational matings and rigid E-unification (1992) Journal of the ACM, 39 (2), pp. 377-429. , Apr
German, S.M., Sistla, A.P., Reasoning about systems with many processes (1992) Journal of the ACM, 39 (3), pp. 675-735. , July
Graf, S., Saïdi, H., Verifying invariants using theorem proving (1996) Lecture Notes in Computer Science, 1102, pp. 196-207. , Computer Aided Verification, Springer Verlag
Gribomont, E.P., Simplification of boolean verification conditions (2000) Theoretical Computer Science, 239 (1), pp. 165-185. , May
Halpern, J.Y., Presburger arithmetic with unary predicates is Π11 complete (1991) The Journal of Symbolic Logic, 56 (2), pp. 637-642. , June
Heitmeyer, C., Lynch, N.A., The generalized railroad crossing - A case study in formal verification of real-time systems (1994) Proceedings 15th IEEE Real-Time Systems Symposium, pp. 120-131. , San Juan, Puerto Rico, Dec
Jensen, H.E., Lynch, N.A., A proof of burns n-process mutual exclusion algorithm using abstraction (1998) Lecture Notes in Computer Science, 1384, pp. 409-423. , Tools and Algorithms for Construction and Analysis of Systems, Springer-Verlag, Mar
Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E., Symbolic model checking with rich assertional languages (1997) Lecture Notes in Computer Science, 1254, pp. 424-435. , Computer Aided Verification, Springer-Verlag
Kurshan, R.P., McMillan, K., A structural induction theorem for processes (1989) Principles of Distributed Computing, pp. 239-248. , ACM Press, Aug
Lynch, N., (1996) Distributed Algorithms, , Morgan Kaufmann, San Francisco, CS
Necula, G.C., (1998) Compiling with Proofs, , PhD thesis, Carnegie Mellon University, Oct. Available as Technical Report CMU-CS-98-154
Nelson, G., Oppen, D.C., Simplifications by cooperating decision procedures (1979) ACM Transactions on Programming Languages and Systems, 1 (2), pp. 245-257. , Oct
Pnueli, A., Ruah, S., Zuck, L.D., Automatic deductive verification with invisible invariants (2001) Lecture Notes in Computer Science, pp. 82-97. , Tools and Algorithms for the Construction and Analysis of Systems
Ramsey, F., On a Problem of Formal Logic (1930) Proceedings of the London Mathematical Society, 30, pp. 264-286
Shankar, N., Verification of Real-Time Systems Using PVS (1993) Lecture Notes in Computer Science, 697, pp. 280-291. , Computer Aided Verification, Springer-Verlag, June
Wolper, P., Lovinfosse, V., Verifying properties of large sets of processes with network invariants (1989) Lecture Notes in Computer Science, 407, pp. 68-80. , Automatic Verification Methods for Finite State Systems, Springer-Verlag, June
