{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,30]],"date-time":"2026-05-30T04:53:48Z","timestamp":1780116828144,"version":"3.54.0"},"publisher-location":"Cham","reference-count":86,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319105741","type":"print"},{"value":"9783319105758","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-10575-8_23","type":"book-chapter","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T08:05:28Z","timestamp":1526630728000},"page":"763-793","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Transfer of Model Checking to Industrial Practice"],"prefix":"10.1007","author":[{"given":"Robert P.","family":"Kurshan","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,5,19]]},"reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"http:\/\/www.absint.de\/astree\/ accessed 20 Oct 2013","DOI":"10.1016\/S1361-3723(13)70084-8"},{"key":"23_CR2","unstructured":"Accellera Property Specification Language Reference Manual (version 1.01). http:\/\/www.eda.org\/vfv\/docs\/psl_lrm-1.01.pdf accessed 20 Oct 2013"},{"key":"23_CR3","unstructured":"Ahrens, F.: Why It\u2019s So Hard For Toyota To Find Out What\u2019s Wrong. The Washington Post p. G01 (2010). see http:\/\/www.washingtonpost.com\/wp-dyn\/content\/article\/2010\/03\/06\/AR2010030602448_pf.html accessed 20 Oct 2013"},{"issue":"6","key":"23_CR4","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1109\/TC.1978.1675141","volume":"C-27","author":"S.B. Akers","year":"1978","unstructured":"Akers, S.B.: Binary decision diagrams. IEEE Trans. Comput. C-27(6), 509\u2013516 (1978)","journal-title":"IEEE Trans. Comput."},{"key":"23_CR5","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-540-69850-0_6","volume-title":"25 Years of Model Checking","author":"R. Alur","year":"2008","unstructured":"Alur, R.: Model checking: from tools to theory. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol.\u00a05000, pp.\u00a089\u2013106. Springer, Heidelberg (2008)"},{"key":"23_CR6","series-title":"LNCS","first-page":"137","volume-title":"Proc. CAV\u201992","author":"R. Alur","year":"1993","unstructured":"Alur, R., Itai, A., Kurshan, R.P., Yannakakis, M.: Timing verification by successive approximation. In: von Bochmann, G., Probst, D. (eds.) Proc. CAV\u201992. LNCS, vol.\u00a0663, pp.\u00a0137\u2013150. Springer, Heidelberg (1993). Also Inf. Comput. 118(1), 142\u2013157 (1995)"},{"key":"23_CR7","unstructured":"http:\/\/www.astree.ens.fr\/ accessed 20 Oct 2013"},{"key":"23_CR8","first-page":"1","volume-title":"Symposium on Principles of Programming Languages (POPL)","author":"T. Ball","year":"2002","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: Launchbury, J., Mitchell, J.C. (eds.) Symposium on Principles of Programming Languages (POPL), pp.\u00a01\u20133. ACM, New York (2002)"},{"key":"23_CR9","unstructured":"Barr, M.: Unintended acceleration and other embedded software bugs (2011). http:\/\/embeddedgurus.com\/barr-code\/2011\/03\/unintended-acceleration-and-other-embedded-software-bugs\/ accessed 20 Oct 2013"},{"issue":"2","key":"23_CR10","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0167-6423(92)90005-V","volume":"19","author":"G. Berry","year":"1992","unstructured":"Berry, G., Gonthier, G.: The ESTEREL synchronous programming language: design, semantics, implementation. Sci. Comput. Program. 19(2), 87\u2013152 (1992)","journal-title":"Sci. Comput. Program."},{"key":"23_CR11","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/1646353.1646374","volume":"53","author":"A. Bessey","year":"2010","unstructured":"Bessey, A., Block, K., Chelf, B., Chou, A., Fulton, B., Hallem, S., Henri-Gros, C., Kamsky, A., McPeak, S., Engler, D.: A few billion lines of code later: using static analysis to find bugs in the real world. Commun. ACM 53, 66\u201375 (2010)","journal-title":"Commun. ACM"},{"key":"23_CR12","first-page":"317","volume-title":"Proc. 36th Design Automation Conference","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Proc. 36th Design Automation Conference, pp.\u00a0317\u2013320. IEEE, Piscataway (1999)"},{"key":"23_CR13","unstructured":"Blau, J.: AT&T\u2019s frame relay crash highlights vulnerable nature of data networks. Total Telcom (1998). http:\/\/www.totaltele.com\/view.aspx?C=0&ID=433385 accessed 20 Oct 2013"},{"key":"23_CR14","volume-title":"Automated Theorem Proving: After 25 Years","year":"1984","unstructured":"Bledsoe, W.W., Loveland, D.W. (eds.): Automated Theorem Proving: After 25 Years, vol.\u00a029. AMS, Providence (1984). Especially the paper \u201cProof-Checking, Theorem-Proving and Program Verification\u201d by R.S. Boyer and J.S. Moore, 119\u2013132"},{"key":"23_CR15","series-title":"LNCS","first-page":"70","volume-title":"Proc. VMCAI 2011","author":"A.R. Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) Proc. VMCAI 2011. LNCS, vol.\u00a06538, pp.\u00a070\u201387. Springer, Heidelberg (2011)"},{"key":"23_CR16","series-title":"LNCS","first-page":"24","volume-title":"Proc. CAV\u201910","author":"R. Brayton","year":"2010","unstructured":"Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Tonilli, T., Cook, B., Jackson, P. (eds.) Proc. CAV\u201910. LNCS, vol.\u00a06174, pp.\u00a024\u201340. Springer, Heidelberg (2010)"},{"issue":"11","key":"23_CR17","first-page":"1456","volume":"56","author":"R. Bryant","year":"2009","unstructured":"Bryant, R.: Computer-aided verification prize awarded. Not. Am. Math. Soc. 56(11), 1456\u20131457 (2009)","journal-title":"Not. Am. Math. Soc."},{"issue":"8","key":"23_CR18","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"23_CR19","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-1-4615-0292-0_1","volume-title":"The Best of ICCAD: 20 Years of Excellence in Computer-Aided Design","author":"R.E. Bryant","year":"2003","unstructured":"Bryant, R.E., Kukula, J.H.: Formal methods for functional verification. In: Kuehlmann, A. (ed.) The Best of ICCAD: 20 Years of Excellence in Computer-Aided Design, pp.\u00a03\u201316. Kluwer Academic, Norwell (2003)"},{"key":"23_CR20","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: Nagel, E., Suppes, P., Tarski, A. (eds.) Methodology and Philosophy of Science, Proc., 1960 Stanford Intern. Congr., pp.\u00a01\u201311. Stanford University Press, Stanford (1962)"},{"key":"23_CR21","first-page":"3","volume-title":"Summaries of Talks Presented at the Summer Institute for Symbolic Logic","author":"A. Church","year":"1957","unstructured":"Church, A.: Application of recursive arithmetics to the problem of circuit synthesis. In: Summaries of Talks Presented at the Summer Institute for Symbolic Logic, pp.\u00a03\u201350 (1957). Communications Research Division, Institute for Defense Analysis"},{"key":"23_CR22","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-69850-0_1","volume-title":"25 Years of Model Checking","author":"E.M. Clarke","year":"2008","unstructured":"Clarke, E.M.: The birth of model checking. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol.\u00a05000, pp.\u00a01\u201326. Springer, Heidelberg (2008)"},{"issue":"1","key":"23_CR23","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E.M. Clarke","year":"2001","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Form. Methods Syst. Des. 19(1), 7\u201334 (2001)","journal-title":"Form. Methods Syst. Des."},{"key":"23_CR24","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Proc. Logic of Programs Workshop","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons for branching time temporal logic. In: Kozen, D. (ed.) Proc. Logic of Programs Workshop. LNCS, vol.\u00a0131, pp.\u00a052\u201371. Springer, Heidelberg (1982)"},{"issue":"5","key":"23_CR25","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E.M. Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003). A preliminary version was published as \u201cCounterexample-Guided Abstraction Refinement\u201d. In: Emerson, E.A., Prasad, A. (eds.) Proc. CAV\u201900. LNCS, vol.\u00a01855, pp.\u00a0154\u2013169. Springer, Heidelberg (2000)","journal-title":"J. ACM"},{"key":"23_CR26","series-title":"LNCS","first-page":"168","volume-title":"Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004)","author":"E.M. Clarke","year":"2004","unstructured":"Clarke, E.M., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004). LNCS, vol.\u00a02988, pp.\u00a0168\u2013176. Springer, Heidelberg (2004)"},{"key":"23_CR27","unstructured":"NASA\u2019s metric confusion caused Mars orbiter loss (1999). http:\/\/www.cnn.com\/TECH\/space\/9909\/30\/mars.metric\/; see also http:\/\/www.thinkreliability.com\/CM-MarsCO.aspx; both accessed 20 Oct 2013"},{"key":"23_CR28","first-page":"129","volume":"20","author":"T. Coe","year":"1995","unstructured":"Coe, T.: Inside the Pentium FDIV bug. Dr. Dobb\u2019s J. 20, 129\u2013135 (1995)","journal-title":"Dr. Dobb\u2019s J."},{"key":"23_CR29","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-1-4020-8157-6_27","volume-title":"Building the Information Society","author":"P. Cousot","year":"2004","unstructured":"Cousot, P., Cousot, R.: Basic concepts of abstract interpretation. In: Jacquard, R. (ed.) Building the Information Society, pp.\u00a0359\u2013366. Kluwer Academic, Norwell (2004)"},{"key":"23_CR30","unstructured":"http:\/\/www.coverity.com\/products\/static-analysis.html accessed 20 Oct 2013"},{"key":"23_CR31","first-page":"522","volume-title":"IEEE International Conference on Computer Design: VLSI in Computers and Processors","author":"D.L. Dill","year":"1992","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.\u00a0522\u2013525. IEEE, Piscataway (1992)"},{"key":"23_CR32","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/j.entcs.2008.06.039","volume":"217","author":"P. Emanuelsson","year":"2008","unstructured":"Emanuelsson, P., Nilsson, U.: A comparative study of industrial static analysis tools. Electron. Notes Theor. Comput. Sci. 217, 5\u201321 (2008). doi:10.1016\/j.entcs.2008.06.039 accessed 20 Oct 2013","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"23_CR33","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-540-69850-0_2","volume-title":"25 Years of Model Checking","author":"E.A. Emerson","year":"2008","unstructured":"Emerson, E.A.: The beginning of model checking: a personal perspective. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol.\u00a05000, pp.\u00a027\u201345. Springer, Heidelberg (2008)"},{"key":"23_CR34","first-page":"267","volume-title":"Proc. LICS","author":"E.A. Emerson","year":"1986","unstructured":"Emerson, E.A., Lei, C.L.: Efficient model checking in fragments of the propositional \u03bc$\\mu$-calculus. In: Proc. LICS, pp.\u00a0267\u2013278. IEEE, Piscataway (1986)"},{"key":"23_CR35","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1016\/S1571-0661(05)80282-8","volume":"26","author":"J. Fiskio-Lasseter","year":"1999","unstructured":"Fiskio-Lasseter, J., Sabry, A.: Putting operational techniques to the test: a syntactic theory for behavioral Verilog. Electron. Notes Theor. Comput. Sci. 26, 34\u201351 (1999)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"23_CR36","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume-title":"Mathematical Aspects of Computer Science","author":"R.W. Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Mathematical Aspects of Computer Science, vol.\u00a019, pp.\u00a019\u201332 (1967)"},{"key":"23_CR37","unstructured":"Lucent\u2019s Bell introduces FormalCheck. Electronic News (1997)"},{"key":"23_CR38","unstructured":"Foster, H.: Prologue: the 2010 Wilson research group functional verification study (2011). http:\/\/blogs.mentor.com\/verificationhorizons\/blog\/2011\/03\/30\/prologue-the-2010-wilson-research-group-functional-verification-study\/ accessed 20 Oct 2013"},{"key":"23_CR39","volume-title":"Assertion Based Design","author":"H.D. Foster","year":"2004","unstructured":"Foster, H.D., Krolnik, A.C., Lacey, D.J.: Assertion Based Design, 2nd edn. Kluwer Academic, Norwell (2004)","edition":"2"},{"key":"23_CR40","volume-title":"Planning and Coding of the Problems for an Electronic Computing Instrument","author":"H.H. Goldstine","year":"1947","unstructured":"Goldstine, H.H., von Neumann, J.: Planning and Coding of the Problems for an Electronic Computing Instrument. Institute for Advanced Study, Princeton (1947)"},{"key":"23_CR41","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanised Logic of Computation","author":"M. Gordon","year":"1979","unstructured":"Gordon, M., Milner, R., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation. LNCS, vol.\u00a078 (1979)"},{"key":"23_CR42","unstructured":"http:\/\/www.grammatech.com\/products\/codesonar\/smashproof_analysis.html accessed 20 Oct 2013"},{"issue":"10","key":"23_CR43","first-page":"1318","volume":"57","author":"O. Grumberg","year":"2010","unstructured":"Grumberg, O.: McMillan receives CAV award. Not. Am. Math. Soc. 57(10), 1318 (2010)","journal-title":"Not. Am. Math. Soc."},{"key":"23_CR44","series-title":"LNCS","volume-title":"25 Years of Model Checking","year":"2008","unstructured":"Grumberg, O., Veith, H. (eds.): 25 Years of Model Checking. LNCS, vol.\u00a05000. Springer, Heidelberg (2008)"},{"issue":"11","key":"23_CR45","first-page":"1429","volume":"55","author":"A. Gupta","year":"2008","unstructured":"Gupta, A.: Alur and Dill receive computer-aided verification award. Not. Am. Math. Soc. 55(11), 1429 (2008)","journal-title":"Not. Am. Math. Soc."},{"issue":"10","key":"23_CR46","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"23_CR47","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/3-540-45426-8_13","volume-title":"Modelling, Analysis, and Design of Hybrid Systems","author":"R. Huuck","year":"2002","unstructured":"Huuck, R., Lukoschus, B., Frehse, G., Engell, S.: Compositional verification of continuous-discrete systems. In: Engell, S., Frehse, G., Schnieder, E. (eds.) Modelling, Analysis, and Design of Hybrid Systems. LNCS, vol.\u00a0279, pp.\u00a0225\u2013244. Springer, Heidelberg (2002)"},{"key":"23_CR48","unstructured":"Toyota shareholders in US sue over fallen stock price. JapanToday (2010). http:\/\/www.japantoday.com\/category\/business\/view\/toyota-shareholders-in-us-sue-over-fallen-stock-price accessed 06 Aug 2013"},{"key":"23_CR49","series-title":"LNCS","first-page":"39","volume-title":"Proc. CAV\u201905","author":"R. Jhala","year":"2005","unstructured":"Jhala, R., McMillan, K.L.: Interpolant-based transition relation approximation. In: Etessami, K., Rajamani, S. (eds.) Proc. CAV\u201905. LNCS, vol.\u00a03576, pp.\u00a039\u201351. Springer, Heidelberg (2005)"},{"issue":"1","key":"23_CR50","first-page":"185","volume":"98","author":"M. Kaufmann","year":"2004","unstructured":"Kaufmann, M., Moore, J.S.: Some key research problems in automated theorem proving for hardware and software verification. Rev. R. Acad. Cienc. Exactas F\u00eds. Nat., Ser. a Mat. 98(1), 185\u2013195 (2004)","journal-title":"Rev. R. Acad. Cienc. Exactas F\u00eds. Nat., Ser. a Mat."},{"key":"23_CR51","first-page":"108","volume-title":"Proc. FMCAD\u201909","author":"Z. Khasidashvili","year":"2009","unstructured":"Khasidashvili, Z., Gavrielov, G., Melham, T.: Assume-guarantee validation for STE properties within an SVA environment. In: Biere, A., Pixley, C. (eds.) Proc. FMCAD\u201909, pp.\u00a0108\u2013115. IEEE, Piscataway (2009)"},{"key":"23_CR52","unstructured":"http:\/\/docs.klocwork.com\/Insight-9.6\/Klocwork_Truepath accessed 15 Sep 2015"},{"key":"23_CR53","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen, D.: Results on propositional \u03bc$\\mu$-calculus. Theor. Comput. Sci. 27, 333\u2013354 (1983)","journal-title":"Theor. Comput. Sci."},{"key":"23_CR54","volume-title":"Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach","author":"R.P. Kurshan","year":"1994","unstructured":"Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1994)"},{"key":"23_CR55","first-page":"258","volume-title":"Proc. DAC\u201997","author":"R.P. Kurshan","year":"1997","unstructured":"Kurshan, R.P.: Formal verification in a commercial setting. In: Proc. DAC\u201997, vol.\u00a034, pp.\u00a0258\u2013262 (1997)"},{"issue":"5","key":"23_CR56","first-page":"534","volume":"47","author":"R.P. Kurshan","year":"2000","unstructured":"Kurshan, R.P.: Program verification. Not. Am. Math. Soc. 47(5), 534\u2013545 (2000)","journal-title":"Not. Am. Math. Soc."},{"key":"23_CR57","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/978-3-540-77966-7_2","volume-title":"Hardware and Software: Verification and Testing","author":"R.P. Kurshan","year":"2008","unstructured":"Kurshan, R.P.: Scaling commercial verification to larger systems. In: Yorav, K. (ed.) Hardware and Software: Verification and Testing. LNCS, vol.\u00a04899, pp.\u00a08\u201313. Springer, Heidelberg (2008)"},{"key":"23_CR58","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-540-69850-0_3","volume-title":"25 Years of Model Checking","author":"R.P. Kurshan","year":"2008","unstructured":"Kurshan, R.P.: Verification technology transfer. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol.\u00a05000, pp.\u00a046\u201364. Springer, Heidelberg (2008)"},{"key":"23_CR59","doi-asserted-by":"publisher","first-page":"985","DOI":"10.1002\/j.1538-7305.1959.tb01585.x","volume":"38","author":"C.Y. Lee","year":"1959","unstructured":"Lee, C.Y.: Representations of switching circuits by binary-decision programs. Bell Syst. Tech. J. 38, 985\u2013999 (1959)","journal-title":"Bell Syst. Tech. J."},{"issue":"7","key":"23_CR60","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1109\/MC.1993.274940","volume":"26","author":"N.G. Leveson","year":"1993","unstructured":"Leveson, N.G., Turner, C.S.: An investigation of the Therac-25 accidents. IEEE Comput. 26(7), 18\u201341 (1993)","journal-title":"IEEE Comput."},{"key":"23_CR61","unstructured":"Lions, J.L.: Ariane 5 flight 501 failure (1996). http:\/\/web.archive.org\/web\/20000815230639\/www.esrin.esa.it\/htdocs\/tidc\/Press\/Press96\/ariane5rep.html accessed 20 Oct 2013"},{"key":"23_CR62","unstructured":"Lohr, S.: AT&T data network fails and commerce takes a hit. The New York Times (1998). http:\/\/www.nytimes.com\/1998\/04\/15\/business\/at-t-data-network-fails-and-commerce-takes-a-hit.html accessed 20 Oct 2013"},{"key":"23_CR63","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic, Norwell (1993)"},{"key":"23_CR64","series-title":"LNCS","first-page":"1","volume-title":"Proc. CAV\u201903","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A. Jr., Somenzi, F. (eds.) Proc. CAV\u201903. LNCS, vol.\u00a02725, pp.\u00a01\u201313. Springer, Heidelberg (2003)"},{"key":"23_CR65","series-title":"LNCS","first-page":"2","volume-title":"Proc. TACAS\u201903","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L., Amla, N.: Automatic abstraction without counterexamples. In: Garavel, H., Hatcliff, J. (eds.) Proc. TACAS\u201903. LNCS, vol.\u00a02619, pp.\u00a02\u201317. Springer, Heidelberg (2003)"},{"key":"23_CR66","volume-title":"Introduction to VLSI Systems","author":"C. Mead","year":"1979","unstructured":"Mead, C., Conway, L.: Introduction to VLSI Systems. Addison-Wesley, Reading (1979)"},{"issue":"4","key":"23_CR67","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/BF01966091","volume":"6","author":"P. Naur","year":"1966","unstructured":"Naur, P.: Proof of algorithms by general snapshots. BIT 6(4), 310\u2013316 (1966)","journal-title":"BIT"},{"key":"23_CR68","unstructured":"http:\/\/www.parasoft.com\/jsp\/technologies\/code_analysis.jsp accessed 20 Oct 2013"},{"key":"23_CR69","first-page":"46","volume-title":"Proc. Eighteenth FOCS","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proc. Eighteenth FOCS, pp.\u00a046\u201357. IEEE, Piscataway (1977)"},{"key":"23_CR70","doi-asserted-by":"crossref","unstructured":"http:\/\/www.mathworks.com\/products\/polyspace\/ accessed 20 Oct 2013","DOI":"10.1002\/wilm.10267"},{"key":"23_CR71","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"Proc. Intl. Symp. on Programming","author":"J.P. Queille","year":"1982","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Proc. Intl. Symp. on Programming. LNCS, vol.\u00a0137, pp.\u00a0337\u2013351. Springer, Heidelberg (1982)"},{"key":"23_CR72","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 decision problems. IBM J. Res. Dev. 3, 114\u2013125 (1959)","journal-title":"IBM J. Res. Dev."},{"key":"23_CR73","doi-asserted-by":"publisher","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. J. ACM 12, 23\u201341 (1965)","journal-title":"J. ACM"},{"issue":"7","key":"23_CR74","doi-asserted-by":"publisher","first-page":"630","DOI":"10.1109\/TC.1982.1676060","volume":"31","author":"H. Rudin","year":"1982","unstructured":"Rudin, H., West, C.: A validation technique for tightly coupled protocols. IEEE Trans. Comput. 31(7), 630\u2013636 (1982)","journal-title":"IEEE Trans. Comput."},{"issue":"2","key":"23_CR75","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF01383966","volume":"6","author":"C.J.H. Seger","year":"1995","unstructured":"Seger, C.J.H., Bryant, R.E.: Formal verification by symbolic evaluation of partially-ordered trajectories. Form. Methods Syst. Des. 6(2), 147\u2013190 (1995)","journal-title":"Form. Methods Syst. Des."},{"key":"23_CR76","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1002\/j.1538-7305.1949.tb03624.x","volume":"28","author":"C.E. Shannon","year":"1949","unstructured":"Shannon, C.E.: The synthesis of two-terminal switching circuits. Bell Syst. Tech. J. 28, 59\u201398 (1949)","journal-title":"Bell Syst. Tech. J."},{"key":"23_CR77","unstructured":"Sterling, B.: PART ONE: crashing the system (1990). http:\/\/www.farcaster.com\/sterling\/part1.htm accessed 15 Sep 2015"},{"issue":"4","key":"23_CR78","first-page":"11","volume":"218","author":"P. Travis","year":"1990","unstructured":"Travis, P.: Why the AT&T network crashed. Telephony 218(4), 11 (1990). See also http:\/\/www.phworld.org\/history\/attcrash.htm and http:\/\/tech-insider.org\/data-security\/research\/1990\/0126.html, both accessed 15 Sep 2015","journal-title":"Telephony"},{"key":"23_CR79","doi-asserted-by":"crossref","unstructured":"Turing, A.: On computable numbers, with an application to the Entscheidungsproblem. Proc. Lond. Math. Soc. 42 (1936)","DOI":"10.2307\/2268810"},{"issue":"11","key":"23_CR80","first-page":"1597","volume":"58","author":"M. Vardi","year":"2011","unstructured":"Vardi, M.: Ball and Rajamani receive 2011 CAV award. Not. Am. Math. Soc. 58(11), 1597 (2011)","journal-title":"Not. Am. Math. Soc."},{"key":"23_CR81","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-540-69850-0_10","volume-title":"25 Years of Model Checking","author":"M.Y. Vardi","year":"2008","unstructured":"Vardi, M.Y.: From Church and Prior to PSL. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol.\u00a05000, pp.\u00a0150\u2013171. Springer, Heidelberg (2008)"},{"key":"23_CR82","first-page":"322","volume-title":"Proc. (1st) IEEE Symposium on Logic in Computer Science (LICS)","author":"M.Y. Vardi","year":"1986","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), pp.\u00a0322\u2013331 (1986)"},{"key":"23_CR83","unstructured":"Waxer, C.: The hidden cost of IT security. Network Security Journal (2006). http:\/\/www.networksecurityjournal.com\/features\/hidden-cost-of-IT-security-041607\/ accessed 20 Oct 2013"},{"key":"23_CR84","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1147\/rd.224.0393","volume":"22","author":"C. West","year":"1978","unstructured":"West, C.: Generalized technique for communication protocol validation. IBM J. Res. Dev. 22, 393\u2013404 (1978)","journal-title":"IBM J. Res. Dev."},{"key":"23_CR85","unstructured":"Whitehead, A.N., Russell, B.: Principia Mathematica. Cambridge University Press, Cambridge (1910\u20131913)"},{"key":"23_CR86","volume-title":"Constraint-Based Verification","author":"J. Yuan","year":"2006","unstructured":"Yuan, J., Pixley, C., Aziz, A.: Constraint-Based Verification. Springer, Heidelberg (2006)"}],"container-title":["Handbook of Model Checking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10575-8_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,2]],"date-time":"2020-11-02T04:15:08Z","timestamp":1604290508000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10575-8_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319105741","9783319105758"],"references-count":86,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10575-8_23","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}