{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,20]],"date-time":"2026-02-20T07:49:36Z","timestamp":1771573776499,"version":"3.50.1"},"publisher-location":"Cham","reference-count":87,"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_1","type":"book-chapter","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T08:05:28Z","timestamp":1526630728000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":42,"title":["Introduction to Model Checking"],"prefix":"10.1007","author":[{"given":"Edmund M.","family":"Clarke","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Helmut","family":"Veith","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,19]]},"reference":[{"issue":"4","key":"1_CR1","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1093\/comjnl\/bxp023","volume":"53","author":"B. Akbarpour","year":"2010","unstructured":"Akbarpour, B., Abdel-Hamid, A.T., Tahar, S., Harrison, J.: Verifying a synthesized implementation of IEEE-754 floating-point exponential function using HOL. Comput. J. 53(4), 465\u2013488 (2010)","journal-title":"Comput. J."},{"issue":"4","key":"1_CR2","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B. Alpern","year":"1985","unstructured":"Alpern, B., Schneider, F.B.: Defining liveness. Inf. Process. Lett. 21(4), 181\u2013185 (1985)","journal-title":"Inf. Process. Lett."},{"key":"1_CR3","volume-title":"Principles of Cyber-Physical Systems","author":"R. Alur","year":"2015","unstructured":"Alur, R.: Principles of Cyber-Physical Systems. MIT Press, Cambridge (2015)"},{"key":"1_CR4","first-page":"1","volume-title":"Proceedings, Formal Methods in Computer-Aided Design, FMCAD","author":"R. Alur","year":"2013","unstructured":"Alur, R., Bod\u00edk, R., Juniwal, G., Martin, M.M.K., Raghothaman, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: Jobstmann, B., Ray, S. (eds.) Proceedings, Formal Methods in Computer-Aided Design, FMCAD, Portland, OR, USA, October 20\u201323, 2013, pp.\u00a01\u20138. IEEE, Piscataway (2013)"},{"issue":"7","key":"1_CR5","doi-asserted-by":"publisher","first-page":"971","DOI":"10.1109\/5.871304","volume":"88","author":"R. Alur","year":"2000","unstructured":"Alur, R., Henzinger, T.A., Lafferriere, G., Pappas, G.J.: Discrete abstractions of hybrid systems. Proc. IEEE 88(7), 971\u2013984 (2000)","journal-title":"Proc. IEEE"},{"key":"1_CR6","volume-title":"Modern Compiler Implementation in C","author":"A.W. Appel","year":"1998","unstructured":"Appel, A.W.: Modern Compiler Implementation in C. Cambridge University Press, Cambridge (1998)"},{"key":"1_CR7","series-title":"Texts in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-745-5","volume-title":"Verification of Sequential and Concurrent Programs","author":"K.R. Apt","year":"2009","unstructured":"Apt, K.R., de Boer, F.S., Olderog, E.-R.: Verification of Sequential and Concurrent Programs. Texts in Computer Science. Springer, Heidelberg (2009)"},{"key":"1_CR8","volume-title":"Principles of Model Checking","author":"C. Baier","year":"2008","unstructured":"Baier, C., Katoen, J-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"1_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72912-9","volume-title":"Test and Analysis of Web Services","author":"L. Baresi","year":"2007","unstructured":"Baresi, L., Di Nitto, E.: Test and Analysis of Web Services. Springer, Heidelberg (2007)"},{"key":"1_CR10","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/3-540-63166-6_28","volume-title":"Proceedings, Computer Aided Verification, CAV","author":"I. Beer","year":"1997","unstructured":"Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in ACTL formulas. In: Grumberg, O. (ed.) Proceedings, Computer Aided Verification, CAV, Haifa, Israel, June 22\u201325, 1997. LNCS, vol.\u00a01254, pp.\u00a0279\u2013290. Springer, Heidelberg (1997)"},{"key":"1_CR11","volume-title":"Principles of the SPIN Model Checker","author":"M. Ben-Ari","year":"2008","unstructured":"Ben-Ari, M.: Principles of the SPIN Model Checker. Springer, Heidelberg (2008)"},{"key":"1_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-04558-9","volume-title":"Systems and Software Verification: Model-Checking Techniques and Tools","author":"B. B\u00e9rard","year":"2001","unstructured":"B\u00e9rard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P.: Systems and Software Verification: Model-Checking Techniques and Tools. Springer, Heidelberg (2001)"},{"key":"1_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004)"},{"key":"1_CR14","series-title":"LNCS","first-page":"S33","volume-title":"Proceedings, Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Bloem","year":"2015","unstructured":"Bloem, R., K\u00f6nighofer, B., K\u00f6nighofer, R., Wang, C.: Shield synthesis: runtime enforcement for reactive systems. In: Baier, C., Tinelli, C. (eds.) Proceedings, Tools and Algorithms for the Construction and Analysis of Systems, TACAS, London, UK, April 11\u201318, 2015. LNCS, vol.\u00a09035, pp.\u00a0S33\u2013S48. Springer, Heidelberg (2015)"},{"issue":"4","key":"1_CR15","doi-asserted-by":"publisher","first-page":"27:1","DOI":"10.1145\/2629686","volume":"15","author":"U. Boker","year":"2014","unstructured":"Boker, U., Chatterjee, K., Henzinger, T.A., Kupferman, O.: Temporal specifications with accumulative values. ACM Trans. Comput. Log. 15(4), 27:1\u201327:25 (2014)","journal-title":"ACM Trans. Comput. Log."},{"key":"1_CR16","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/978-3-319-23820-3_23","volume-title":"Proceedings, Runtime Verification, RV","author":"L. Bortolussi","year":"2015","unstructured":"Bortolussi, L., Milios, D., Sanguinetti, G.: Machine-learning methods in statistical model checking and system design. In: Proceedings, Runtime Verification, RV, Vienna, Austria, September 22\u201325, 2015. LNCS, vol.\u00a09333, pp.\u00a0323\u2013341. Springer, Heidelberg (2015)"},{"key":"1_CR17","first-page":"127","volume-title":"Proceedings, Networked Systems Design and Implementation, NSDI","author":"M. Canini","year":"2012","unstructured":"Canini, M., Venzano, D., Pere\u0161\u00edni, P., Kosti\u0107, D., Rexford, J.: A NICE way to test openflow applications. In: Gribble, S.D., Katabi, D. (eds.) Proceedings, Networked Systems Design and Implementation, NSDI, San Jose, CA, USA, April 25\u201327, 2012, pp.\u00a0127\u2013140. USENIX Association, Berkeley (2012)"},{"key":"1_CR18","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-68612-7","volume-title":"Introduction to Discrete-Event Systems","author":"C.G. Cassandras","year":"2008","unstructured":"Cassandras, C.G., Lafortune, S.: Introduction to Discrete-Event Systems, 2nd edn. Springer, Heidelberg (2008)","edition":"2"},{"key":"1_CR19","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/978-3-319-21668-3_11","volume-title":"Proceedings, Computer Aided Verification, CAV, Part II","author":"P. Cern\u00fd","year":"2015","unstructured":"Cern\u00fd, P., Clarke, E.M., Henzinger, T.A., Radhakrishna, A., Ryzhyk, L., Samanta, R., Tarrach, T.: From non-preemptive to preemptive scheduling using synchronization synthesis. In: Kroening, D., Pasareanu, C.S. (eds.) Proceedings, Computer Aided Verification, CAV, Part II, San Francisco, CA, USA, July 18\u201324, 2015. LNCS, vol.\u00a09207, pp.\u00a0180\u2013197. Springer, Heidelberg (2015)"},{"issue":"1","key":"1_CR20","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/j.tcs.2011.08.002","volume":"413","author":"P. Cern\u00fd","year":"2012","unstructured":"Cern\u00fd, P., Henzinger, T.A., Radhakrishna, A.: Simulation distances. Theor. Comput. Sci. 413(1), 21\u201335 (2012)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR21","first-page":"115","volume-title":"Proceedings, Principles of Programming Languages, POPL","author":"P. Cern\u00fd","year":"2013","unstructured":"Cern\u00fd, P., Henzinger, T.A., Radhakrishna, A.: Quantitative abstraction refinement. In: Giacobazzi, R., Cousot, R. (eds.) Proceedings, Principles of Programming Languages, POPL, Rome, Italy, January 23\u201325, 2013, pp.\u00a0115\u2013128. ACM, New York (2013)"},{"key":"1_CR22","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Proceedings, Logics of Programs","author":"E.M. Clarke","year":"1981","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Proceedings, Logics of Programs, Yorktown Heights, NY, USA, May 1981. LNCS, vol.\u00a0131, pp.\u00a052\u201371. Springer, Heidelberg (1981)"},{"issue":"11","key":"1_CR23","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1145\/1592761.1592781","volume":"52","author":"E.M. Clarke","year":"2009","unstructured":"Clarke, E.M., Emerson, E.A., Sifakis, J.: Model checking: algorithmic verification and debugging. Commun. ACM 52(11), 74\u201384 (2009)","journal-title":"Commun. ACM"},{"key":"1_CR24","first-page":"117","volume-title":"Proceedings, Principles of Programming Languages, POPL","author":"E.M. Clarke","year":"1983","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite state concurrent systems using temporal logic specifications: a practical approach. In: Wright, J.R., Landweber, L., Demers, A.J., Teitelbaum, T. (eds.) Proceedings, Principles of Programming Languages, POPL, Austin, TX, USA, January 1983, pp.\u00a0117\u2013126. ACM, New York (1983)"},{"key":"1_CR25","doi-asserted-by":"publisher","first-page":"539","DOI":"10.1007\/0-8176-4404-0_23","volume-title":"Handbook of Networked and Embedded Control Systems","author":"E.M. Clarke","year":"2005","unstructured":"Clarke, E.M., Fehnker, A., Jha, S.K., Veith, H.: Temporal-logic model checking. In: Hristu-Varsakelis, D., Levine, W.S. (eds.) Handbook of Networked and Embedded Control Systems, pp.\u00a0539\u2013558. Birkh\u00e4user, Basel (2005)"},{"key":"1_CR26","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"1_CR27","first-page":"19","volume-title":"Proceedings, Logic in Computer Science, LICS","author":"E.M. Clarke","year":"2002","unstructured":"Clarke, E.M., Jha, S., Lu, Y., Veith, H.: Tree-like counterexamples in model checking. In: Proceedings, Logic in Computer Science, LICS, Copenhagen, Denmark, July 22\u201325 July 2002, pp.\u00a019\u201329. IEEE, Piscataway (2002)"},{"key":"1_CR28","doi-asserted-by":"publisher","first-page":"1635","DOI":"10.1016\/B978-044450813-3\/50026-6","volume-title":"Handbook of Automated Reasoning","author":"E.M. Clarke","year":"2001","unstructured":"Clarke, E.M., Schlingloff, B.-H.: Model checking. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp.\u00a01635\u20131790. Elsevier\/MIT Press, Amsterdam\/Cambridge (2001)"},{"key":"1_CR29","first-page":"238","volume-title":"Principles of Programming Languages, POPL","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) Principles of Programming Languages, POPL, Los Angeles, CA, USA, January 1977, pp.\u00a0238\u2013252. ACM, New York (1977)"},{"issue":"1","key":"1_CR30","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1023\/A:1011227529550","volume":"19","author":"W. Damm","year":"2001","unstructured":"Damm, W., Harel, D.: LSCs: breathing life into message sequence charts. Form. Methods Syst. Des. 19(1), 45\u201380 (2001)","journal-title":"Form. Methods Syst. Des."},{"key":"1_CR31","first-page":"321","volume-title":"Proceedings, Programming Language Design and Implementation, PLDI","author":"A. Desai","year":"2013","unstructured":"Desai, A., Gupta, V., Jackson, E.K., Qadeer, S., Rajamani, S.K., Zufferey, D.: P: safe asynchronous event-driven programming. In: Boehm, H-J., Flanagan, C. (eds.) Proceedings, Programming Language Design and Implementation, PLDI, Seattle, WA, USA, June 16\u201319, 2013, pp.\u00a0321\u2013332. ACM, New York (2013)"},{"issue":"10","key":"1_CR32","doi-asserted-by":"publisher","first-page":"859","DOI":"10.1145\/355604.361591","volume":"15","author":"E.W. Dijkstra","year":"1972","unstructured":"Dijkstra, E.W.: The humble programmer. Commun. ACM 15(10), 859\u2013866 (1972)","journal-title":"Commun. ACM"},{"key":"1_CR33","first-page":"995","volume-title":"Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics","author":"E.A. Emerson","year":"1990","unstructured":"Emerson, E.A.: Temporal and modal logic. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pp.\u00a0995\u20131072. MIT Press, Cambridge (1990)"},{"issue":"1","key":"1_CR34","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"Emerson, E.A., Halpern, J.Y.: \u201cSometimes\u201d and \u201cnot never\u201d revisited: on branching versus linear-time temporal logic. J. ACM 33(1), 151\u2013178 (1986)","journal-title":"J. ACM"},{"issue":"10","key":"1_CR35","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1145\/2001269.2001289","volume":"54","author":"J. Fisher","year":"2011","unstructured":"Fisher, J., Harel, D., Henzinger, T.A.: Biology as reactivity. Commun. ACM 54(10), 72\u201382 (2011)","journal-title":"Commun. ACM"},{"key":"1_CR36","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume-title":"Proceedings, Mathematical Aspects of Computer Science: American Mathematical Society Symposia","author":"R.W. Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meaning to programs. In: Schwartz, J.T. (ed.) Proceedings, Mathematical Aspects of Computer Science: American Mathematical Society Symposia, Providence, RI, USA, vol.\u00a019, pp.\u00a019\u201331. AMS, Providence (1967)"},{"key":"1_CR37","first-page":"213","volume-title":"Proceedings, Programming Language Design and Implementation, PLDI","author":"P. Godefroid","year":"2005","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Sarkar, V., Hall, M.W. (eds.) Proceedings, Programming Language Design and Implementation, PLDI, Chicago, IL, USA, June 12\u201315, 2005, pp.\u00a0213\u2013223. ACM, New York (2005)"},{"key":"1_CR38","series-title":"LNCS","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69850-0","volume-title":"25 Years of Model Checking: History, Achievements, Perspectives","author":"O. Grumberg","year":"2008","unstructured":"Grumberg, O., Veith, H.: 25 Years of Model Checking: History, Achievements, Perspectives. LNCS, vol.\u00a05000. Springer, Heidelberg (2008)"},{"issue":"11","key":"1_CR39","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1145\/2736282","volume":"58","author":"S. Gulwani","year":"2015","unstructured":"Gulwani, S., Hern\u00e1ndez-Orallo, J., Kitzelmann, E., Muggleton, S.H., Schmid, U., Zorn, B.G.: Inductive Programming meets the real world. Commun. ACM 58(11), 90\u201399 (2015)","journal-title":"Commun. ACM"},{"key":"1_CR40","unstructured":"Hales, T.C., Adams, M., Bauer, G., Dang, D.T., Harrison, J., Hoang, T.L., Kaliszyk, C., Magron, V., McLaughlin, S., Nguyen, T.T., Nguyen, T.Q., Nipkow, T., Obua, S., Pleso, J., Rute, J., Solovyev, A., Ta, A.H.T., Tran, T.N., Trieu, D.T., Urban, J., Vu, K.K., Zumkeller, R.: A\u00a0formal proof of the Kepler conjecture. CoRR (2015). arXiv:1501.02155 [abs]"},{"issue":"3","key":"1_CR41","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231\u2013274 (1987)","journal-title":"Sci. Comput. Program."},{"key":"1_CR42","volume-title":"Come, Let\u2019s Play. Scenario-Based Programming Using LSCs and the Play-Engine","author":"D. Harel","year":"2003","unstructured":"Harel, D., Marelly, R.: Come, Let\u2019s Play. Scenario-Based Programming Using LSCs and the Play-Engine. Springer, Heidelberg (2003)"},{"issue":"4","key":"1_CR43","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/s00450-013-0251-7","volume":"28","author":"T.A. Henzinger","year":"2013","unstructured":"Henzinger, T.A.: Quantitative reactive modeling and verification. Comput. Sci. Res. Dev. 28(4), 331\u2013344 (2013)","journal-title":"Comput. Sci. Res. Dev."},{"key":"1_CR44","series-title":"LNCS","first-page":"273","volume-title":"Proceedings, Concurrency Theory, CONCUR","author":"T.A. Henzinger","year":"2013","unstructured":"Henzinger, T.A., Otop, J.: From model checking to model measuring. In: D\u2019Argenio, P.R., Melgratti, H.C. (eds.) Proceedings, Concurrency Theory, CONCUR, Buenos Aires, Argentina, August 27\u201330, 2013. LNCS, vol.\u00a08052, pp.\u00a0273\u2013287. Springer, Heidelberg (2013)"},{"issue":"10","key":"1_CR45","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 computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"1_CR46","volume-title":"Design and Validation of Computer Protocols","author":"G.J. Holzmann","year":"1995","unstructured":"Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice Hall, New York (1995)"},{"key":"1_CR47","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"G.J. Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2004)"},{"key":"1_CR48","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511619540","volume-title":"Model-Based Software Testing and Analysis with C#","author":"J. Jacky","year":"2007","unstructured":"Jacky, J., Veanes, M., Campbell, C., Schulte, W.: Model-Based Software Testing and Analysis with C#. Cambridge University Press, Cambridge (2007)"},{"key":"1_CR49","first-page":"170","volume-title":"Proceedings, Enterprise Distributed Object Computing, EDOC","author":"C.T. Karamanolis","year":"2000","unstructured":"Karamanolis, C.T., Giannakopoulou, D., Magee, J., Wheater, S.M.: Model checking of workflow schemas. In: Proceedings, Enterprise Distributed Object Computing, EDOC, Makuhari, Japan, September 25\u201328, 2000, pp.\u00a0170\u2013181. IEEE, Piscataway (2000)"},{"issue":"7","key":"1_CR50","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"J.C. King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"issue":"1","key":"1_CR51","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/2560537","volume":"32","author":"G. Klein","year":"2014","unstructured":"Klein, G., Andronick, J., Elphinstone, K., Murray, T.C., Sewell, T., Kolanski, R., Heiser, G.: Comprehensive formal verification of an OS micro-kernel. ACM Trans. Comput. Syst. 32(1), 2 (2014)","journal-title":"ACM Trans. Comput. Syst."},{"issue":"3","key":"1_CR52","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 the propositional \u03bc$\\mu$-calculus. Theor. Comput. Sci. 27(3), 333\u2013354 (1983)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"1_CR53","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/2964568","volume":"24","author":"S. Kripke","year":"1959","unstructured":"Kripke, S.: A completeness theorem in modal logic. J. Symb. Log. 24(1), 1\u201314 (1959)","journal-title":"J. Symb. Log."},{"key":"1_CR54","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03809-3","volume-title":"Introduction to Formal Hardware Verification","author":"T. Kropf","year":"1999","unstructured":"Kropf, T.: Introduction to Formal Hardware Verification. Springer, Heidelberg (1999)"},{"key":"1_CR55","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":"1_CR56","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"2","author":"L. Lamport","year":"1977","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 2, 125\u2013143 (1977)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"1_CR57","volume-title":"Introduction to Embedded Systems, A Cyber-physical Systems Approach","author":"E.A. Lee","year":"2015","unstructured":"Lee, E.A., Seshia, S.: Introduction to Embedded Systems, A Cyber-physical Systems Approach, 2nd edn. MIT Press, Cambridge (2015)","edition":"2"},{"key":"1_CR58","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-16612-9_11","volume-title":"Proceedings, Runtime Verification, RV","author":"A. Legay","year":"2010","unstructured":"Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G.J., Rosu, G., Sokolsky, O., Tillmann, N. (eds.) Proceedings, Runtime Verification, RV, St. Julian\u2019s, Malta, November 1\u20134, 2010. LNCS, vol.\u00a06418, pp.\u00a0122\u2013135. Springer, Heidelberg (2010)"},{"issue":"7","key":"1_CR59","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X. Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"1_CR60","volume-title":"Safeware: System Safety and Computers","author":"N.G. Leveson","year":"1995","unstructured":"Leveson, N.G.: Safeware: System Safety and Computers. Addison-Wesley, Reading (1995)"},{"key":"1_CR61","first-page":"97","volume-title":"Principles of Programming Languages, POPL","author":"O. Lichtenstein","year":"1985","unstructured":"Lichtenstein, O., Pnueli, A.: Checking that finite-state concurrent programs satisfy their linear specification. In: Van Deusen, M.S., Galil, Z., Reid, B.K. (eds.) Principles of Programming Languages, POPL, New Orleans, LA, USA, January 1985, pp.\u00a097\u2013107. ACM, New York (1985)"},{"key":"1_CR62","volume-title":"Introduction to Mathematical Theory of Computation","author":"Z. Manna","year":"1974","unstructured":"Manna, Z.: Introduction to Mathematical Theory of Computation. McGraw-Hill, New York (1974)"},{"key":"1_CR63","series-title":"LNCS","volume-title":"Time for Verification, Essays in Memory of Amir Pnueli","year":"2010","unstructured":"Manna, Z., Peled, D. (eds.): Time for Verification, Essays in Memory of Amir Pnueli. LNCS, vol.\u00a06200. Springer, Heidelberg (2010)"},{"key":"1_CR64","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1992)"},{"key":"1_CR65","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/BFb0025786","volume-title":"Proceedings, Logics of Programs","author":"Z. Manna","year":"1981","unstructured":"Manna, Z., Wolper, P.: Synthesis of communicating processes from temporal-logic specifications. In: Kozen, D. (ed.) Proceedings, Logics of Programs, Yorktown Heights, NY, USA, May 1981. LNCS, vol.\u00a0131, pp.\u00a0253\u2013281. Springer, Heidelberg (1981)"},{"key":"1_CR66","series-title":"Studies in Logic and the Foundations of Mathematics","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1016\/S0049-237X(08)72018-4","volume-title":"Computer Programming and Formal Systems","author":"J. McCarthy","year":"1963","unstructured":"McCarthy, J.: A basis for a mathematical theory of computation. In: Braffort, P., Hirschberg, D. (eds.) Computer Programming and Formal Systems. Studies in Logic and the Foundations of Mathematics, vol.\u00a035, pp.\u00a033\u201370. Elsevier, Amsterdam (1963)"},{"key":"1_CR67","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. Springer, Heidelberg (1993)"},{"key":"1_CR68","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F. Nielson","year":"1999","unstructured":"Nielson, F., Riis Nielson, H., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)"},{"key":"1_CR69","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002)"},{"key":"1_CR70","series-title":"LIPIcs","first-page":"209","volume-title":"Proceedings, Summit on Advances in Programming Languages, SNAPL","author":"A. Panda","year":"2015","unstructured":"Panda, A., Argyraki, K.J., Sagiv, M., Schapira, M., Shenker, S.: New directions for network verification. In: Ball, T., Bod\u00edk, R., Krishnamurthi, S., Lerner, B.S., Morrisett, G. (eds.) Proceedings, Summit on Advances in Programming Languages, SNAPL, Asilomar, CA, USA, May 3\u20136, 2015. LIPIcs, vol.\u00a032, pp.\u00a0209\u2013220. Schloss Dagstuhl, Wadern (2015)"},{"key":"1_CR71","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3540-6","volume-title":"Software Reliability Methods","author":"D.A. Peled","year":"2001","unstructured":"Peled, D.A.: Software Reliability Methods. Springer, Heidelberg (2001)"},{"key":"1_CR72","first-page":"46","volume-title":"Proceedings, Foundations of Computer Science, FOCS","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings, Foundations of Computer Science, FOCS, Providence, RI, USA, October 31\u2013November 1, 1977, pp.\u00a046\u201357. IEEE, Piscataway (1977)"},{"key":"1_CR73","first-page":"179","volume-title":"Proceedings, Principles of Programming Languages, POPL","author":"A. Pnueli","year":"1989","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings, Principles of Programming Languages, POPL, Austin, TX, USA, January 11\u201313, 1989, pp.\u00a0179\u2013190. ACM, New York (1989)"},{"key":"1_CR74","doi-asserted-by":"publisher","DOI":"10.1142\/p1004","volume-title":"Analysis of Biological Systems","author":"C. Priami","year":"2015","unstructured":"Priami, C., Morine, M.J.: Analysis of Biological Systems. Imperial College Press, London (2015)"},{"key":"1_CR75","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"Proceedings, International Symposium 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.) Proceedings, International Symposium on Programming, Torino, Italy, April 6\u20138, 1982. LNCS, vol.\u00a0137, pp.\u00a0337\u2013351. Springer, Heidelberg (1982)"},{"key":"1_CR76","doi-asserted-by":"publisher","DOI":"10.1090\/cbms\/013","volume-title":"Automata on Infinite Objects and Church\u2019s Problem","author":"M.O. Rabin","year":"1972","unstructured":"Rabin, M.O.: Automata on Infinite Objects and Church\u2019s Problem. AMS, Providence (1972)"},{"issue":"1","key":"1_CR77","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1109\/5.21072","volume":"77","author":"P.J.G. Ramadge","year":"1989","unstructured":"Ramadge, P.J.G., Wonham, W.M.: The control of discrete event systems. Proc. IEEE 77(1), 81\u201398 (1989)","journal-title":"Proc. IEEE"},{"key":"1_CR78","first-page":"761","volume-title":"Proceedings, Principles of Programming Languages, POPL","author":"V. Raychev","year":"2016","unstructured":"Raychev, V., Bielik, P., Vechev, M.T., Krause, A.: Learning programs from noisy data. In: Bod\u00edk, R., Majumdar, R. (eds.) Proceedings, Principles of Programming Languages, POPL, St. Petersburg, FL, USA, January 20\u201322, 2016, pp.\u00a0761\u2013774. ACM, New York (2016)"},{"key":"1_CR79","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1090\/S0002-9947-1953-0053041-6","volume":"74","author":"H.G. Rice","year":"1953","unstructured":"Rice, H.G.: Classes of recursively enumerable sets and their decision problems. Trans. Am. Math. Soc. 74, 358\u2013366 (1953)","journal-title":"Trans. Am. Math. Soc."},{"issue":"5\u20136","key":"1_CR80","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/s10009-012-0249-7","volume":"15","author":"A. Solar-Lezama","year":"2013","unstructured":"Solar-Lezama, A.: Program sketching. Softw. Tools Technol. Transf. 15(5\u20136), 475\u2013495 (2013)","journal-title":"Softw. Tools Technol. Transf."},{"key":"1_CR81","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-0224-5","volume-title":"Verification and Control of Hybrid Systems","author":"P. Tabuada","year":"2009","unstructured":"Tabuada, P.: Verification and Control of Hybrid Systems. Springer, Heidelberg (2009)"},{"key":"1_CR82","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1112\/plms\/s2-42.1.230","volume":"42","author":"A. Turing","year":"1937","unstructured":"Turing, A.: On computable numbers, with an application to the Entscheidungsproblem. Proc. Lond. Math. Soc. 42, 230\u2013265 (1937)","journal-title":"Proc. Lond. Math. Soc."},{"key":"1_CR83","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49851-4","volume-title":"Process Mining\u2014Data Science in Action","author":"W.M.P. Aalst van der","year":"2016","unstructured":"van der Aalst, W.M.P.: Process Mining\u2014Data Science in Action, 2nd edn. Springer, Heidelberg (2016)","edition":"2"},{"key":"1_CR84","first-page":"322","volume-title":"Proceedings, 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: Proceedings, Logic in Computer Science, LICS, Cambridge, MA, USA, June 16\u201318, 1986, pp.\u00a0322\u2013331. IEEE, Piscataway (1986)"},{"key":"1_CR85","series-title":"LNCS","volume-title":"The Seventeen Provers of the World","year":"2006","unstructured":"Wiedijk, F. (ed.): The Seventeen Provers of the World. LNCS, vol.\u00a03600. Springer, Heidelberg (2006)"},{"key":"1_CR86","first-page":"185","volume-title":"Proceedings, Foundations of Computer Science, FOCS","author":"P. Wolper","year":"1983","unstructured":"Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths. In: Proceedings, Foundations of Computer Science, FOCS, Tucson, AZ, USA, November 7\u20139, 1983, pp.\u00a0185\u2013194. IEEE, Piscataway (1983)"},{"issue":"12","key":"1_CR87","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1145\/2043174.2043197","volume":"54","author":"J. Yang","year":"2011","unstructured":"Yang, J., Hawblitzel, C.: Safe to the last instruction: automated verification of a type-safe operating system. Commun. ACM 54(12), 123\u2013131 (2011)","journal-title":"Commun. ACM"}],"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_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T08:05:47Z","timestamp":1526630747000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10575-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319105741","9783319105758"],"references-count":87,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10575-8_1","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}