{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,23]],"date-time":"2025-09-23T12:39:33Z","timestamp":1758631173605},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540698494"},{"type":"electronic","value":"9783540698500"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-69850-0_3","type":"book-chapter","created":{"date-parts":[[2008,7,31]],"date-time":"2008-07-31T06:39:46Z","timestamp":1217486386000},"page":"46-64","source":"Crossref","is-referenced-by-count":11,"title":["Verification Technology Transfer"],"prefix":"10.1007","author":[{"given":"R. P.","family":"Kurshan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","first-page":"317","volume-title":"Proc. 36th Design Automation Conference","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Proc. 36th Design Automation Conference, pp. 317\u2013320. IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Berry, G., Gonthier, G.: The Esterel Synchronous Programming Language: Design, Semantics, Implementation. Science of Computer Programming, vol.\u00a019, pp. 87\u2013152 (1992)","DOI":"10.1016\/0167-6423(92)90005-V"},{"key":"#cr-split#-3_CR3.1","doi-asserted-by":"crossref","unstructured":"Bledsoe, W.W., Loveland, D.W. (eds.): Automated Theorem Proving: After 25 Years, Contemporary Math. 29, pp. 119???132. Amer. Math. Soc. (1984);","DOI":"10.1090\/conm\/029"},{"key":"#cr-split#-3_CR3.2","unstructured":"Especially the paper Proof-Checking, Theorem-Proving and Program Verification by R. S. Boyer and J. S. Moore"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The SLAM Project: Debugging System Software via Static Analysis. In: Symposium on Principles of Programming Languages (POPL), pp. 1\u20133. ACM (January 2002)","DOI":"10.1145\/503272.503274"},{"key":"3_CR5","first-page":"1","volume-title":"Methodology and Philosophy of Science, Proc., 1960 Stanford Intern. Congr.","author":"J.R. B\u00fcchi","year":"1962","unstructured":"B\u00fcchi, J.R.: On a Decision Method in Restricted Second-Order Arithmetic. In: Methodology and Philosophy of Science, Proc., 1960 Stanford Intern. Congr., pp. 1\u201311. Stanford Univ. Press, Stanford (1962)"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. In: Formal Methods in System Design, vol.\u00a019, Kluwer Academic Publishers (July 2001)","DOI":"10.1023\/A:1011276507260"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A.: Design and Synthesis of Synchronization Skeletons for Branching Time Temporal Logic. In: Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371 (1982)","DOI":"10.1007\/BFb0025774"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Computer Aided Verification, pp. 154\u2013169 (2000)","DOI":"10.1007\/10722167_15"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A Tool for Checking ANSI-C Programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"3_CR10","first-page":"129","volume":"20","author":"T. Coe","year":"1995","unstructured":"Coe, T.: Inside the Pentium FDIV Bug. Dr. Dobbs Journal\u00a020, 129\u2013135 (1995)","journal-title":"Dr. Dobbs Journal"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Dill, D.L., Drexler, A.J., Hu, A.J., Yang, C.H.: Protocol Verification as a Hardware Design Aid. In: IEEE International Conference on Computer Design: VLSI in Computers and Processors, pp. 522\u2013525. IEEE Computer Society (1992)","DOI":"10.1109\/ICCD.1992.276232"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Gordon, M., Milner, R., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation. LNCS, vol.\u00a078 (1979)","DOI":"10.1007\/3-540-09724-4"},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/3-540-61474-5_94","volume-title":"Computer Aided Verification","author":"R.H. Hardin","year":"1996","unstructured":"Hardin, R.H., Har\u2019El, Z., Kurshan, R.P.: COSPAN. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 423\u2013427. Springer, Heidelberg (1996)"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/11513988_6","volume-title":"Computer Aided Verification","author":"R. Jhala","year":"2005","unstructured":"Jhala, R., McMillan, K.L.: Interpolant-based transition relation approximation. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 39\u201351. Springer, Heidelberg (2005)"},{"issue":"1","key":"3_CR15","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1002\/j.1538-7305.1990.tb00102.x","volume":"69","author":"R.P. Kurshan","year":"1990","unstructured":"Kurshan, R.P., Har\u2019El, Z.: Software for analytical development of communication protocols. AT&T Tech. J.\u00a069(1), 45\u201359 (1990)","journal-title":"AT&T Tech. J."},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press (1994)","DOI":"10.1515\/9781400864041"},{"issue":"5","key":"3_CR17","first-page":"534","volume":"47","author":"R.P. Kurshan","year":"2000","unstructured":"Kurshan, R.P.: Program Verification. Notices of the AMS\u00a047(5), 534\u2013545 (2000)","journal-title":"Notices of the AMS"},{"key":"3_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/3-540-36577-X_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L., Amla, N.: Automatic Abstraction without Counterexamples. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol.\u00a02619, pp. 2\u201317. Springer, Heidelberg (2003)"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers (1993)","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Computer Aided Verification","author":"L. Kenneth","year":"2003","unstructured":"Kenneth, L., McMillan, K.L.: Interpolation and sat-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The Temporal Logic of Programs. In: Proc. of the Eighteenth Symposium on Foundations of Computer Science (FOCS), Providence, RI, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Queille, J.P., Sifakis, J.: Programming 1982. LNCS, vol.\u00a0137, pp. 337\u2013351 (1982)","DOI":"10.1007\/3-540-11494-7_22"},{"key":"3_CR23","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: Machine-Oriented Logic Based on the Resolution Principle. Journal of the Association for Computing Machinery\u00a012, 23\u201341 (1965)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"3_CR24","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1147\/rd.32.0114","volume":"3","author":"M.O. Rabin","year":"1959","unstructured":"Rabin, M.O., Scott, D.: Finite Automata and Their Decisions Problems. IBM J. Res. and Dev.\u00a03, 114\u2013125 (1959)","journal-title":"IBM J. Res. and Dev."},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Rudin, H., West, C.: A validation technique for tightly coupled protocols. Transactions on Computers (April 1982)","DOI":"10.1109\/TC.1982.1676060"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Turing, A.: On Computable Numbers, With an Application to the Entscheidungsproblem. In: Proceedings of the London Mathematical Society, vol.\u00a042 (1936)","DOI":"10.1112\/plms\/s2-42.1.230"},{"key":"3_CR27","unstructured":"Vardi, M.Y., Wolper, P.: An Automata-Theoretic Approach to Automatic Program Verification. In: Proc (1st) IEEE Symposium on Logic in Computer Science (LICS), Boston, pp. 322\u2013331 (1986)"},{"key":"3_CR28","doi-asserted-by":"crossref","first-page":"393","DOI":"10.1147\/rd.224.0393","volume":"22","author":"C.H. West","year":"1978","unstructured":"West, C.H.: Generalized technique for communication protocol validation. IBM Journal of Res. and Devel.\u00a022, 393\u2013404 (1978)","journal-title":"IBM Journal of Res. and Devel."},{"key":"3_CR29","unstructured":"Alfred\u00a0North Whitehead and Bertrand Russell. Principia Mathematica, pp. 1910\u20131913. Cambridge University Press (1913)"}],"container-title":["Lecture Notes in Computer Science","25 Years of Model Checking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69850-0_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:10:13Z","timestamp":1620015013000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69850-0_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540698494","9783540698500"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69850-0_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}