The birth of model checking. (English) Zbl 1142.68046
Grumberg, Orna (ed.) et al., 25 years of model checking. History, achievements, perspectives. Berlin: Springer (ISBN 978-3-540-69849-4/pbk). Lecture Notes in Computer Science 5000, 1-26 (2008).
E. M. Clarke is one of the founding fathers of model checking. When he together with A. Emerson presented their work “Design and synthesis of synchronization skeletons using branching time temporal logic” during the Workshop on Logic of Programs in Yorktown Heights, NY in May 1981 [Lect. Notes Comput. Sci. 131, 52–71 (1982; Zbl 0546.68014)], this marked the start of a new era in the verification of concurrent programs and systems.
In the present paper, Clarke gives a very personal, historic account of the origins and the development of this important area of computer science. He starts with a description of the state of the art of verification in the late 1970s and he discusses advantages and disadvantages of model checking compared to other verification methods, like, e.g., theorem proving or state exploration for communication protocols. In subsequent sections he deals with central prerequisites of model checking: Tarski’s fixed-point theorem, mu-calculus, branching-time temporal logic, etc. He traces his own research done around 1980, giving a detailed account of how the work of others influenced him. In a section called “My Eureka moment” he describes the circumstances under which he first “realized that the important problem for verification was not the synthesis problem but the problem of checking formulas on finite models.” (p. 13) In the remaining parts of the paper he deals with the subsequent developments in model checking, starting with an appreciation of the work of J. P. Queille and J. Sifakis [“Specification and verification of concurrent systems in CESAR”, Lect. Notes Comput. Sci. 137, 337–351 (1982; Zbl 0482.68028)], who independently developed ideas similar to those of Clarke and Emerson, and continuing with brief outlines on different model checkers, temporal logics, automata-theoretic techniques, process algebra, symbolic model checking and related themes. A final section lists “Big events since 1990 and future challenges”. Throughout the paper the author extensively refers to the literature, collected in a striking bibliography containing about 110 references. So this work is not only a very interesting historical paper but can also serve as a good starting point for readers that are new to the topic.
The paper is the leading article in a collection based on the invited talks at the symposium “25 years of model checking” that was part of the 18th International Conference on Computer Aided Verification (CAV), which in turn was part of the Federated Logic Conference (FLOC) 2006 in Seattle. The whole collection represents one of those rare highlights of the computer science literature that do not concentrate on the every-day business but take a pause looking at the same time at the past, present and future of one of the main research areas of computer science where it is actually a science. As an add-on, the collection contains also reprints of the papers of Clarke and Emerson and of Queille and Sifakis mentioned above.
For the entire collection see [Zbl 1139.68003].
In the present paper, Clarke gives a very personal, historic account of the origins and the development of this important area of computer science. He starts with a description of the state of the art of verification in the late 1970s and he discusses advantages and disadvantages of model checking compared to other verification methods, like, e.g., theorem proving or state exploration for communication protocols. In subsequent sections he deals with central prerequisites of model checking: Tarski’s fixed-point theorem, mu-calculus, branching-time temporal logic, etc. He traces his own research done around 1980, giving a detailed account of how the work of others influenced him. In a section called “My Eureka moment” he describes the circumstances under which he first “realized that the important problem for verification was not the synthesis problem but the problem of checking formulas on finite models.” (p. 13) In the remaining parts of the paper he deals with the subsequent developments in model checking, starting with an appreciation of the work of J. P. Queille and J. Sifakis [“Specification and verification of concurrent systems in CESAR”, Lect. Notes Comput. Sci. 137, 337–351 (1982; Zbl 0482.68028)], who independently developed ideas similar to those of Clarke and Emerson, and continuing with brief outlines on different model checkers, temporal logics, automata-theoretic techniques, process algebra, symbolic model checking and related themes. A final section lists “Big events since 1990 and future challenges”. Throughout the paper the author extensively refers to the literature, collected in a striking bibliography containing about 110 references. So this work is not only a very interesting historical paper but can also serve as a good starting point for readers that are new to the topic.
The paper is the leading article in a collection based on the invited talks at the symposium “25 years of model checking” that was part of the 18th International Conference on Computer Aided Verification (CAV), which in turn was part of the Federated Logic Conference (FLOC) 2006 in Seattle. The whole collection represents one of those rare highlights of the computer science literature that do not concentrate on the every-day business but take a pause looking at the same time at the past, present and future of one of the main research areas of computer science where it is actually a science. As an add-on, the collection contains also reprints of the papers of Clarke and Emerson and of Queille and Sifakis mentioned above.
For the entire collection see [Zbl 1139.68003].
Reviewer: Klaus D. Kiermeier (Berlin)
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B44 | Temporal logic |
| 03B70 | Logic in computer science |
| 68-03 | History of computer science |
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
Software:
NuSMVReferences:
| [1] | Alur, R., Courcourbetis, C., Dill, D.: Model-checking for real-time systems. In: Proceedings of the 5th Symp. on Logic in Computer Science, pp. 414-425 (1990) |
| [2] | Alur, R.; Henzinger, T. A., Reactive modules, Formal Methods in System Design: An International Journal, 15, 1, 7-48 (1999) · doi:10.1023/A:1008739929481 |
| [3] | Apt, K.; Kozen, D., Limits for automatic verification of finite-state systems, IPL, 15, 307-309 (1986) · doi:10.1016/0020-0190(86)90071-2 |
| [4] | Aggarwal, S., Kurshan, R.P., Sabnani, K.: A calculus for protocol specification and validation. In: Rudin, H., West, C.H. (eds.) Protocol Specification, Testing and Verification, pp. 19-34. North-Holland (1983) |
| [5] | Alur, R.; Madhusudan, P.; Nam, W.; Etessami, K.; Rajamani, S. K., Symbolic Compositional Verification by Learning Assumptions, Computer Aided Verification, 548-562 (2005), Heidelberg: Springer, Heidelberg · Zbl 1081.68601 |
| [6] | Angluin, D., Learning regular sets from queries and counterexamples, Information and Computation, 75, 2, 87-106 (1987) · Zbl 0636.68112 · doi:10.1016/0890-5401(87)90052-6 |
| [7] | Abrial, J.-R., Schuman, S.A., Meyer, B.: Specification language. In: McKeag, R.M., Macnaughten, A.M. (eds.) On the Construction of Programs, pp. 343-410. Cambridge University Press (1980) |
| [8] | Ben-Ari, M.; Manna, Z.; Pnueli, A., The temporal logic of branching time, Acta Informatica, 20, 207-226 (1983) · Zbl 0533.68036 · doi:10.1007/BF01257083 |
| [9] | Bensalem, S.; Bouajjani, A.; Loiseaux, C.; Sifakis, J.; Probst, D. K.; von Bochmann, G., Property preserving simulations, Computer Aided Verification, 260-273 (1992), Heidelberg: Springer, Heidelberg |
| [10] | Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded Model Checking. Advances in computers, vol. 58. Academic Press (2003) |
| [11] | Clarke, E.; Biere, A.; Cimatti, A.; Zhu, Y.; Cleaveland, W. R., Symbolic Model Checking without BDDs, Tools and Algorithms for the Construction of Analysis of Systems, 193-207 (1999), Heidelberg: Springer, Heidelberg |
| [12] | Browne, M.C., Clarke, E.M., Dill, D.: Checking the correctness of sequential circuits. In: Proceedings of the 1985 International Conference on Computer Design, Port Chester, New York, October 1985, pp. 545-548. IEEE (1985) |
| [13] | Browne, M. C.; Clarke, E. M.; Dill, D. L., Automatic circuit verification using temporal logic: Two new examples, Formal Aspects of VLSI Design (1986), North Holland: Elsevier Science Publishers, North Holland · Zbl 0613.94017 |
| [14] | Browne, M. C.; Clarke, E. M.; Dill, D. L.; Mishra, B., Automatic verification of sequential circuits using temporal logic, IEEE Transactions on Computers, C-35, 12, 1035-1044 (1986) · Zbl 0604.94011 · doi:10.1109/TC.1986.1676711 |
| [15] | Browne, M. C.; Clarke, E. M.; Grumberg, O., Characterizing finite Kripke structures in propositional temporal logic, Theoretical Computer Science, 59, 1-2, 115-131 (1988) · Zbl 0677.03011 · doi:10.1016/0304-3975(88)90098-9 |
| [16] | Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, J.: Symbolic model checking: 10^20 states and beyond. In: Proc. 5th Ann. Symp. on Logic in Comput. Sci., IEEE Comp. Soc. Press (June 1990) · Zbl 0753.68066 |
| [17] | Burch, J. R.; Clarke, E. M.; McMillan, K. L.; Dill, D. L.; Hwang, L. J., Symbolic model checking: 10^20 states and beyond, Information and Computation, 98, 2, 142-170 (1992) · Zbl 0753.68066 · doi:10.1016/0890-5401(92)90017-A |
| [18] | Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: International Conference on Concurrency Theory, pp. 135-150 (1997) · Zbl 1512.68135 |
| [19] | Bose, S., Fisher, A.: Verifying pipelined hardware using symbolic logic simulation. In: IEEE International Conference on Computer Design (October 1989) |
| [20] | Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs 36(5), 203-213 (June 2001) |
| [21] | Bochmann, G.V.: Hardware specification with temporal logic: An example. IEEE Transactions on Computers C-31(3) (March 1982) · Zbl 0477.94036 |
| [22] | Bartlett, K. A.; Scantlebury, R. A.; Wilkinson, P. T., A note on reliable full-duplex transmission over half-duplex links, Commun. ACM, 12, 5, 260-261 (1969) · doi:10.1145/362946.362970 |
| [23] | Burstall, R.M.: Program proving as hand simulation with a little induction. In: IFIP congress 1974, pp. 308-312. North Holland (1974) · Zbl 0299.68012 |
| [24] | Basu, S. K.; Yeh, R. T., Strong verification of programs, IEEE Trans. Software Eng., 1, 3, 339-346 (1975) |
| [25] | Coudert, O., Berthet, C., Madre, J.C.: Verification of synchronous sequential machines based on symbolic execution. In: Sifakis [Sif89], pp. 365-373. · Zbl 0786.68059 |
| [26] | Coudert, O., Berthet, C., Madre, J.C.: Verifying temporal properties of sequential machines without building their state diagrams. In: Kurshan, Clarke [KC90], pp. 23-32 · Zbl 0765.68119 |
| [27] | Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. 4th Ann. ACM Symp. on Principles of Prog. Lang., pp. 238-252 (January 1977) |
| [28] | Cimatti, A.; Clarke, E. M.; Giunchiglia, F.; Roveri, M., Nusmv: A new symbolic model checker, STTT, 2, 4, 410-425 (2000) · Zbl 1059.68582 |
| [29] | Chaki, S., Clarke, E., Sharygina, N., Sinha, N.: Dynamic component substitutability analysis. In: Proc. of Conf. on Formal Methods (2005) · Zbl 1120.68421 |
| [30] | Chaki, S., Clarke, E., Sinha, N., Thati, P.: Automated assume-guarantee reasoning for simulation conformance. In: Proc. of Computer-Aided Verification (2005) · Zbl 1081.68612 |
| [31] | Clarke, E. M.; Draghicescu, I. A.; de Bakker, J. W.; de Roever, W.-P.; Rozenberg, G., Expressibility results for linear time and branching time logics, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, 428-437 (1989), Heidelberg: Springer, Heidelberg · Zbl 0683.68030 · doi:10.1007/BFb0013029 |
| [32] | Clarke, E. M.; Emerson, E. A.; Kozen, D., Design and synthesis of synchronization skeletons using branching time temporal logic, Logics of Programs (1982), Heidelberg: Springer, Heidelberg · Zbl 0546.68014 · doi:10.1007/BFb0025774 |
| [33] | Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. In: Proc. 10th Ann. ACM Symp. on Principles of Prog. Lang. (January 1983) · Zbl 0591.68027 |
| [34] | Clarke, E. M.; Emerson, E. A.; Sistla, A. P., Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems, 8, 2, 244-263 (1986) · Zbl 0591.68027 · doi:10.1145/5397.5399 |
| [35] | Clarke, E.M., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. In: Courcoubetis [Cou93], pp.450-462 |
| [36] | Clarke, E.M., Grumberg, O., Browne, M.C.: Reasoning about networks with many identical finite-state processes. In: Proceedings of the Fifth Annual ACM Symposium on Principles of Distributed Computing, pp. 240-248. ACM (August 1986) · Zbl 0709.68610 |
| [37] | Clarke, E. M.; German, S. M.; Halpern, J. Y., Effective axiomatizations of Hoare logics, J. ACM, 30, 3, 612-636 (1983) · Zbl 0627.68010 · doi:10.1145/2402.322394 |
| [38] | Clarke, E.M., Grumberg, O., Hiraishi, H., Jha, S., Long, D.E., McMillan, K.L., Ness, L.A.: Verification of the Futurebus+ cache coherence protocol. In: Claesen [Cla93] |
| [39] | Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Computer Aided Verification (CAV), pp. 154-169 (2000) · Zbl 0974.68517 |
| [40] | Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. In: POPL, pp. 342-354 (1992) |
| [41] | Clarke, E. M.; Grumberg, O.; Long, D. E., Model checking and abstraction, ACM Transactions on Programming Languages and Systems, 16, 5, 1512-1542 (1994) · doi:10.1145/186025.186051 |
| [42] | Cobleigh, J.; Giannakopoulou, D.; Păsăreanu, C. S.; Garavel, H.; Hatcliff, J., Learning Assumptions for Compositional Verification, Tools and Algorithms for the Construction and Analysis of Systems, 331-346 (2003), Heidelberg: Springer, Heidelberg · Zbl 1031.68545 |
| [43] | Clarke, E.M., Liu, L.: Approximate algorithms for optimization of busy waiting in parallel programs (preliminary report). In: 20th Annual Symposium on Foundations of Computer Science, pp. 255-266. IEEE Computer Society (1979) |
| [44] | Clarke, E.M.: Program invariants as fixed points (preliminary reports). In: 18th Annual Symposium on Foundations of Computer Science, pp. 18-29. IEEE Computer Society (November 1977) · Zbl 0418.68001 |
| [45] | Clarke, E. M., Programming language constructs for which it is impossible to obtain good hoare-like axiom systems, Fourth ACM Symposium on Principles of Programming Languages, 10-20 (1977), New York: ACM Press, New York |
| [46] | Clarke, E. M., Proving the correctness of coroutines without history variables, ACM-SE 16: Proceedings of the 16th annual Southeast regional conference, 160-167 (1978), New York: ACM Press, New York · doi:10.1145/503643.503680 |
| [47] | Clarke, E., Program invariants as fixed points, Computing, 21, 4, 273-294 (1979) · Zbl 0399.68022 · doi:10.1007/BF02248730 |
| [48] | Clarke, E.M.: Synthesis of resource invariants for concurrent programs. In: POPL, pp. 211-221 (1979) |
| [49] | Clarke, E. M., Programming language constructs for which it is impossible to obtain good Hoare axiom systems, J. ACM, 26, 1, 129-147 (1979) · Zbl 0388.68008 · doi:10.1145/322108.322121 |
| [50] | Clarke, E., Proving correctness of coroutines without history variables, Acta Inf., 13, 169-188 (1980) · Zbl 0404.68016 |
| [51] | Clarke, E.M.: The characterization problem for hoare logics. In: Proc. of a discussion meeting of the Royal Society of London on Mathematical logic and programming languages, Upper Saddle River, NJ, USA, pp. 89-106. Prentice-Hall, Inc (1985) |
| [52] | Claesen, L. (ed.): Proc. 11th Int. Symp. on Comput. Hardware Description Lang. and their Applications. North-Holland (April 1993) |
| [53] | Cook, S. A., Soundness and completeness of an axiom system for program verification, SIAM Journal on Computing, 7, 1, 70-90 (1978) · Zbl 0374.68009 · doi:10.1137/0207005 |
| [54] | Courcoubetis, C., Computer Aided Verification (1993), Heidelberg: Springer, Heidelberg · Zbl 0825.00130 |
| [55] | de Bakker, J. W.; Meertens, L., On the completeness of the inductive assertion method, Journal of Computer and System Sciences, 11, 323-357 (1975) · Zbl 0353.68040 |
| [56] | Dill, D.L., Clarke, E.M.: Automatic verification of asynchronous circuits using temporal logic. IEE Proceedings, Part E 133(5) (1986) · Zbl 0604.94011 |
| [57] | Dill, D.L.: Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. In: ACM Distinguished Dissertations. MIT Press (1989) |
| [58] | Emerson, E. A.; Clarke, E. M.; de Bakker, J. W.; van Leeuwen, J., Characterizing correctness properties of parallel programs using fixpoints, Automata, Languages and Programming, 169-181 (1980), Heidelberg: Springer, Heidelberg · Zbl 0456.68016 |
| [59] | Eisner, C.; Fisman, D., A Practical Introduction to PSL (Series on Integrated Circuits and Systems) (2006), New York: Springer, New York |
| [60] | Emerson, E. A.; Halpern, J. Y., “Sometimes“ and “Not Never” revisited: On branching time versus linear time, Journal of the ACM, 33, 151-178 (1986) · Zbl 0629.68020 · doi:10.1145/4904.4999 |
| [61] | Emerson, E.A., Lei, C.-L.: Modalities for model checking: Branching time strikes back. In: Twelfth Symposium on Principles of Programming Languages, New Orleans, La, pp. 84-96 (January 1985) |
| [62] | Emerson, E.A., Sistla, A.P.: Symmetry and model checking. In: Courcoubetis [Cou93], pp. 463-478 |
| [63] | Grumberg, O.; Long, D. E., Model checking and modular verification, ACM Transactions on Programming Languages and Systems, 16, 843-872 (1994) · doi:10.1145/177492.177725 |
| [64] | Godefroid, P.: Using partial orders to improve automatic verification methods. In: Kurshan, Clarke [KC90] · Zbl 0786.68061 |
| [65] | Graf, S.; Saïdi, H.; Grumberg, O., Construction of abstract state graphs with PVS, Computer Aided Verification, 72-83 (1997), Heidelberg: Springer, Heidelberg |
| [66] | Har’El, Z., Kurshan, R.P.: The COSPAN user’s guide. Technical Report 11211-871009-21TM, AT&T Bell Labs (1987) |
| [67] | Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? In: Proceedings of the 27th Annual Symposium on Theory of Computing, pp. 373-382. ACM Press (1995) · Zbl 0978.68534 |
| [68] | Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall (1985) · Zbl 0637.68007 |
| [69] | Ip, C.W., Dill, D.L.: Better verification through symmetry. In: Claesen [Cla93] |
| [70] | Jones, C.B.: Specification and design of (parallel) programs. In: Proceedings of IFIP 1983, pp. 321-332. North-Holland (1983) |
| [71] | Kurshan, R.P., Clarke, E.M.: Proc. 1990 Workshop on Comput.-Aided Verification (June 1990) |
| [72] | Kildall, G.A.: A unified approach to global program optimization. In: POPL, pp. 194-206 (1973) · Zbl 0309.68020 |
| [73] | Kleene, S.C.: Introduction to Metamathematics, Wolters-Noordhoff, Groningen (1971) · Zbl 0047.00703 |
| [74] | Kurshan, R.P., McMillan, K.L.: A structural induction theorem for processes. In: Proc. 8th Ann. ACM Symp. on Principles of Distributed Computing, pp. 239-247. ACM Press (August 1989) |
| [75] | Kozen, D., Results on the propositional mu-calculus, Theoretical Computer Science, 27, 333-354 (1983) · Zbl 0553.03007 · doi:10.1016/0304-3975(82)90125-6 |
| [76] | Kröger, F., Lar: A logic of algorithmic reasoning, Acta Inf., 8, 243-266 (1977) · Zbl 0347.68016 |
| [77] | Kam, J. B.; Ullman, J. D., Monotone data flow analysis frameworks, Acta Inf., 7, 305-317 (1977) · Zbl 0375.68020 · doi:10.1007/BF00290339 |
| [78] | Kurshan, R.P.: Computer-aided verification of coordinating processes: the automata-theoretic approach. Princeton University Press (1994) · Zbl 0822.68116 |
| [79] | Lamport, L.: “Sometimes” is sometimes “Not Never”. In: Ann. ACM Symp. on Principles of Prog. Lang., pp. 174-185 (1980) |
| [80] | Liu, L., Clarke, E.: Optimization of busy waiting in conditional critical regions. In: 13th Hawaii International Conference on System Sciences (January 1980) |
| [81] | Long, D.E.: Model Checking, Abstraction, and Compositional Reasoning. PhD thesis, Carnegie Mellon Univ. (1993) |
| [82] | Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: Proc. 12th Ann. ACM Symp. on Principles of Prog. Lang., pp. 97-107 (January 1985) |
| [83] | Mead, C.; Conway, L., Introduction to VLSI Systems (1979), Boston: Addison-Wesley Longman Publishing Co., Inc., Boston |
| [84] | Misra, J.; Chandy, K. M., Proofs of networks of processes, IEEE Transactions on Software Engineering, SE-7, 4, 417-426 (1981) · Zbl 0468.68030 · doi:10.1109/TSE.1981.230844 |
| [85] | Mishra, B.; Clarke, E. M., Hierarchical verification of asynchronous circuits using temporal logic, Theoretical Computer Science, 38, 269-291 (1985) · Zbl 0584.94022 · doi:10.1016/0304-3975(85)90223-3 |
| [86] | Marrero, W., Clarke, E., Jha, S.: Model checking for security protocols (1997) |
| [87] | McMillan, K.L.: Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers (1993) · Zbl 0784.68004 |
| [88] | McMillan, K. L.; Grumberg, O., A compositional rule for hardware design refinement, Computer Aided Verification, 24-35 (1997), Heidelberg: Springer, Heidelberg |
| [89] | Milner, R.: An algebraic definition of simulation between programs. In: Proc. 2nd Int. Joint Conf. on Artificial Intelligence, pp. 481-489 (September 1971) |
| [90] | Malachi, Y., Owicki, S.S.: Temporal specifications of self-timed systems. In: Kung, H.T., Sproull, B., Steele, G. (eds.) VLSI Systems and Computations, Comp. Sci. Press (1981) |
| [91] | Owicki, S.; Gries, D., Verifying properties of parallel programs: an axiomatic approach, Commun. ACM, 19, 5, 279-285 (1976) · Zbl 0322.68010 · doi:10.1145/360051.360224 |
| [92] | Owicki, S.; Lamport, L., Proving liveness properties of concurrent programs, ACM Trans. Program. Lang. Syst., 4, 3, 455-495 (1982) · Zbl 0483.68013 · doi:10.1145/357172.357178 |
| [93] | Park, D.M.R.: Finiteness is mu-ineffable. Theory of Computation Report No. 3, Warwick (1974) |
| [94] | Park, D.; Deussen, P., Concurrency and automata on infinite sequences, Theoretical Computer Science, 167-183 (1981), Heidelberg: Springer, Heidelberg · Zbl 0457.68049 · doi:10.1007/BFb0017309 |
| [95] | Peled, D.; Dill, D. L., Combining partial order reductions with on-the-fly model-checking, Computer Aided Verification, 377-390 (1994), Heidelberg: Springer, Heidelberg |
| [96] | Pixley, C.: Introduction to a computational theory and implementation of sequential hardware equivalence. In: Kurshan, Clarke [KC90], pp. 54-64 · Zbl 0800.68557 |
| [97] | Pnueli, A.: The temporal semantics of concurrent programs. In: 18th Annual Symposium on Foundations of Computer Science (1977) · Zbl 0402.68009 |
| [98] | Pnueli, A.: In transition for global to modular temporal reasoning about programs. In: Apt, K.R. (ed.) Logics and Models of Concurrent Systems, NATO ASI series F, vol. 13. Springer (1984) · Zbl 0578.68014 |
| [99] | Quielle, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Proceedings of the 5th International Symposium on Programming, pp. 337-350 (1982) · Zbl 0482.68028 |
| [100] | Queille, J. P.; Sifakis, J., Fairness and related properties in transition systems - a temporal logic to deal with fairness, Acta Inf., 19, 195-220 (1982) · Zbl 0489.68024 |
| [101] | Roscoe, A.W.: Model-checking CSP. In: Roscoe, A.W. (ed.) A Classical Mind: Essays in Honour of C. A. R. Hoare, pp. 353-378. Prentice-Hall (1994) |
| [102] | Rivest, R. L.; Schapire, R. E., Inference of finite automata using homing sequences, Inf. Comp., 103, 2, 299-347 (1993) · Zbl 0786.68082 · doi:10.1006/inco.1993.1021 |
| [103] | Sistla, A. P.; Clarke, E. M., Complexity of propositional temporal logics, Journal of the ACM, 32, 3, 733-749 (1986) · Zbl 0632.68034 · doi:10.1145/3828.3837 |
| [104] | David, A.: Schmidt. Data flow analysis is model checking of abstract interpretations. In: POPL, pp. 38-48 (1998) |
| [105] | Sifakis, J., Automatic Verification Methods for Finite State Systems (1989), Heidelberg: Springer, Heidelberg |
| [106] | Tarski, A., A lattice-theoretical fixpoint theorem and its applications, Pacific J. Math., 5, 285-309 (1955) · Zbl 0064.26004 |
| [107] | Taylor, R. N.; Osterweil, L. J., Anomaly detection in concurrent software by static data flow analysis, IEEE Trans. Software Eng., 6, 3, 265-278 (1980) · Zbl 0431.68029 · doi:10.1109/TSE.1980.234488 |
| [108] | Valmari, A.: A stubborn attack on the state explosion problem. In: Kurshan, Clarke [KC90] · Zbl 0786.68069 |
| [109] | Vitanyi, P.M.B.: Andrei nikolaevich kolmogorov. 1, 3-18 (1988) · Zbl 0643.01026 |
| [110] | Vardi, M. Y.; Wolper, P., An automata-theoretic approach to automatic program verification, Proc. 1st Ann. Symp. on Logic in Comput. Sci (1986), Los Alamitos: IEEE Computer Society Press, Los Alamitos |
| [111] | Wolper, P., Lovinfosse, V.: Verifying properties of large sets of processes with network invariants. In: Sifakis [Sif89] |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
