{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T09:56:28Z","timestamp":1781258188507,"version":"3.54.1"},"publisher-location":"Cham","reference-count":80,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030002619","type":"print"},{"value":"9783030002626","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","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":[[2019]]},"DOI":"10.1007\/978-3-030-00262-6_5","type":"book-chapter","created":{"date-parts":[[2019,2,11]],"date-time":"2019-02-11T10:02:09Z","timestamp":1549879329000},"page":"193-222","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Formal Methods"],"prefix":"10.1007","author":[{"given":"Doron A.","family":"Peled","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,2,12]]},"reference":[{"key":"5_CR1","unstructured":"Aggarwal, S., Kurshan, R.P., Sabnani, K.K.: A calculus for protocol specification and validation. In: Protocol Specification, Testing, and Verification, pp. 19\u201334 (1983)"},{"issue":"3","key":"5_CR2","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B Alpern","year":"1987","unstructured":"Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117\u2013126 (1987)","journal-title":"Distrib. Comput."},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Dill, D.L.: Automata for modeling real-time systems. In: Proceedings of ICALP, pp. 322\u2013335 (1990)","DOI":"10.1007\/BFb0032042"},{"issue":"1","key":"5_CR4","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R Alur","year":"1995","unstructured":"Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138(1), 3\u201334 (1995)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"5_CR5","first-page":"70","volume":"17","author":"R Alur","year":"1996","unstructured":"Alur, R., Holzmann, G.J., Peled, D.A.: An analyzer for message sequence charts. Softw. Concepts Tools 17(2), 70\u201377 (1996)","journal-title":"Softw. Concepts Tools"},{"key":"5_CR6","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/BFb0055039","volume-title":"Automata, Languages and Programming","author":"Rajeev Alur","year":"1998","unstructured":"Alur, R., McMillan, K.L., Peled, D.A.: Deciding global partial-order properties. In: Proceedings of ICALP, pp. 41\u201352 (1998)"},{"issue":"4","key":"5_CR7","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1145\/357146.357150","volume":"3","author":"KR Apt","year":"1981","unstructured":"Apt, K.R.: Ten years of Hoare\u2019s logic: a survey - part 1. ACM Trans. Program. Lang. Syst. 3(4), 431\u2013483 (1981)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"6","key":"5_CR8","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"KR Apt","year":"1986","unstructured":"Apt, K.R., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307\u2013309 (1986)","journal-title":"Inf. Process. Lett."},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Ardeshir-Larijani, E., Gay, S.J., Nagarajan, R.: Automated verification of quantum protocols by equivalence checking. In: Proceedings of TACAS, pp. 500\u2013514 (2014)","DOI":"10.1007\/978-3-642-54862-8_42"},{"key":"5_CR10","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/3-540-63165-8_199","volume-title":"Automata, Languages and Programming","author":"Christel Baier","year":"1997","unstructured":"Baier, C., Clarke, E.M., Hartonas-Garmhausen, V., Kwiatkowska, M.Z., Ryan, M.: Symbolic model checking for probabilistic processes. In: Proceedings of ICALP, pp. 430\u2013440 (1997)"},{"issue":"3","key":"5_CR11","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/s10703-015-0222-7","volume":"46","author":"DA Basin","year":"2015","unstructured":"Basin, D.A., Klaedtke, F., Marinovic, S., Zalinescu, E.: Monitoring of temporal first-order properties with aggregations. Formal Methods Syst. Des. 46(3), 262\u2013285 (2015)","journal-title":"Formal Methods Syst. Des."},{"key":"5_CR12","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/BFb0020949","volume-title":"Hybrid Systems III","author":"Johan Bengtsson","year":"1996","unstructured":"Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: UPPAAL - a tool suite for automatic verification of real-time systems. In: Proceedings of Hybrid Systems, pp. 232\u2013243 (1995)"},{"key":"5_CR13","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BFb0028755","volume-title":"Computer Aided Verification","author":"S. Bensalem","year":"1998","unstructured":"Bensalem, S., Lakhnech, Y., Owre, S.: Computing abstractions of infinite state systems compositionally and automatically. In: Proceedings of CAV, pp. 319\u2013331 (1998)"},{"key":"5_CR14","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"CONCUR '97: Concurrency Theory","author":"Ahmed Bouajjani","year":"1997","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: application to model-checking. In: Proceedings of CONCUR, pp. 135\u2013150 (1997)"},{"key":"5_CR15","volume-title":"Computational Logic","author":"RS Boyer","year":"1979","unstructured":"Boyer, R.S., Moore, J.S.: Computational Logic. Academic, New York (1979)"},{"issue":"8","key":"5_CR16","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE 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":"5_CR17","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1002\/malq.19600060105","volume":"6","author":"JR B\u00fcchi","year":"1960","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. Z. Math. Logik Grundlag. Math 6, 66\u201392 (1960)","journal-title":"Z. Math. Logik Grundlag. Math"},{"key":"5_CR18","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. In: Proceedings of LICS, pp. 428\u2013439 (1990)"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of Programs, pp. 52\u201371 (1981)","DOI":"10.1007\/BFb0025774"},{"issue":"1","key":"5_CR20","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"EM Clarke","year":"2001","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods Syst. Des. 19(1), 7\u201334 (2001)","journal-title":"Formal Methods Syst. Des."},{"issue":"5","key":"5_CR21","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"EM 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)","journal-title":"J. ACM"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"Courcoubetis, C., Yannakakis, M.: Verifying temporal properties of finite-state probabilistic programs. In: Proceedings of FOCS, pp. 338\u2013345 (1988)","DOI":"10.1109\/SFCS.1988.21950"},{"key":"5_CR23","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C Courcoubetis","year":"1992","unstructured":"Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties. Formal Methods Syst. Des. 1, 275\u2013288 (1992)","journal-title":"Formal Methods Syst. Des."},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of POPL, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"de Moura, L.Me., Bjorner, N.: Z3, an efficient SMT solver. In: Proceedings of TACAS, pp. 337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"9","key":"5_CR26","doi-asserted-by":"publisher","first-page":"569","DOI":"10.1145\/365559.365617","volume":"8","author":"EW Dijkstra","year":"1965","unstructured":"Dijkstra, E.W.: Solution of a problem in concurrent programming control. Commun. ACM 8(9), 569 (1965)","journal-title":"Commun. ACM"},{"key":"5_CR27","unstructured":"Eisner, C., Fisman, D.: A Practical Introduction to PSL. Series on Integrated Circuits and Systems. Springer, Berlin (2006)"},{"key":"5_CR28","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/3-540-10003-2_69","volume-title":"Automata, Languages and Programming","author":"E. Allen Emerson","year":"1980","unstructured":"Emerson, E.A., Clarke, E.M.: Characterizing correctness properties of parallel programs using fixpoints. In: Proceedings of ICALP, pp. 169\u2013181 (1980)"},{"issue":"1","key":"5_CR29","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"EA 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"},{"key":"5_CR30","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Mathematical Aspects of Computer Science, pp. 19\u201332. American Mathematical Society, Providence (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"5_CR31","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4886-6","volume-title":"Fairness","author":"Nissim Francez","year":"1986","unstructured":"Francez, N.: Fairness, Texts and Monographs in Computer Science, pp. 1\u2013295. Springer, Berlin (1986)"},{"key":"5_CR32","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-0-387-34892-6_1","volume-title":"Protocol Specification, Testing and Verification XV","author":"R. Gerth","year":"1996","unstructured":"Gerth, R., Peled, D.A., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Proceedings of PSTV, pp. 3\u201318 (1995)"},{"key":"5_CR33","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Wolper, P.: A partial approach to model checking. In: Proceedings of LICS, pp. 406\u2013415 (1991)","DOI":"10.1109\/LICS.1991.151664"},{"issue":"6","key":"5_CR34","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1145\/1064978.1065036","volume":"40","author":"Patrice Godefroid","year":"2005","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Proceedings of PLDI, pp. 213\u2013223 (2005)","journal-title":"ACM SIGPLAN Notices"},{"issue":"1","key":"5_CR35","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/BF01700692","volume":"38","author":"K G\u00f6del","year":"1931","unstructured":"G\u00f6del, K.: \u00dcber formal unentscheidbare S\u00e4tze der Principia Mathematica und verwandter Systeme. Monatsh. Math. Phys. 38(1), 173\u2013198 (1931)","journal-title":"Monatsh. Math. Phys."},{"key":"5_CR36","volume-title":"Introduction to HOL","author":"MJC Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL. Cambridge University Press, Cambridge (1993)"},{"key":"5_CR37","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-540-31980-1_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Radu Grosu","year":"2005","unstructured":"Grosu, R., Smolka, S.A.: Monte Carlo model checking. In: Proceedings of TACAS, pp. 271\u2013286 (2005)"},{"key":"5_CR38","first-page":"135","volume":"2001","author":"K Havelund","year":"2001","unstructured":"Havelund, K., Rosu, G.: Monitoring programs using rewriting. In: Proceedings of Automated Software Engineering, November 2001, pp. 135\u2013143 (2001)","journal-title":"In: Proceedings of Automated Software Engineering, November"},{"key":"5_CR39","doi-asserted-by":"crossref","unstructured":"Havelund, K., Peled, D.A., Ulus, D.: First order temporal logic monitoring with BDDs. In: Proceedings of FMCAD, pp. 116\u2013123 (2017)","DOI":"10.23919\/FMCAD.2017.8102249"},{"issue":"10","key":"5_CR40","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR 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":"5_CR41","volume-title":"The SPIN Model Checker - Primer and Reference Manual","author":"GJ Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The SPIN Model Checker - Primer and Reference Manual. Addison-Wesley, Boston (2004)"},{"key":"5_CR42","first-page":"23","volume":"32","author":"GJ Holzmann","year":"1996","unstructured":"Holzmann, G.J., Peled, D.A., Yannakakis, M.: On nested depth first search. In: DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 32, pp. 23\u201331 (1996)","journal-title":"In: DIMACS Series in Discrete Mathematics and Theoretical Computer Science"},{"issue":"2","key":"5_CR43","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256\u2013290 (2002)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"issue":"4","key":"5_CR44","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/s10009-016-0418-1","volume":"19","author":"G Katz","year":"2017","unstructured":"Katz, G., Peled, D.A.: Synthesizing, correcting and improving code, using model checking-based genetic programming. Int. J. Softw. Tools Technol. Transfer 19(4), 449\u2013464 (2017)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"5_CR45","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1109\/32.588534","volume":"23","author":"M Kaufmann","year":"1997","unstructured":"Kaufmann, M., Moore, J.S.: An industrial strength theorem prover for a logic based on Common Lisp. IEEE Trans. Softw. Eng. 23, 203\u2013213 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"2","key":"5_CR46","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/s10703-017-0276-9","volume":"51","author":"B K\u00f6nighofer","year":"2017","unstructured":"K\u00f6nighofer, B., Alshiekh, M., Bloem, R., Humphrey, L., K\u00f6nighofer, R., Topcu, U., Wang, C.: Shield synthesis. Formal Methods Syst. Des. 51(2), 332\u2013361 (2017)","journal-title":"Formal Methods Syst. Des."},{"key":"5_CR47","unstructured":"Kroening, D., Strichman, O.: Decision Procedures - An Algorithmic Point of View. EATCS Series, pp. 1\u2013304. Springer, Berlin (2008)"},{"key":"5_CR48","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/3-540-48683-6_17","volume-title":"Computer Aided Verification","author":"Orna Kupferman","year":"1999","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. In: Proceedings of CAV, pp. 172\u2013183 (1999)"},{"key":"5_CR49","doi-asserted-by":"crossref","unstructured":"Lamport, L.: \u201cSometimes\u201d is sometimes \u201cnot never\u201d. In: Proceedings of POPL, pp. 175\u2013185 (1980)","DOI":"10.1145\/567446.567463"},{"key":"5_CR50","first-page":"152","volume-title":"Lecture Notes in Computer Science","author":"Kim Larsen","year":"2017","unstructured":"Larsen, K.G., Peled, D.A., Sedwards, S.: Memory-efficient tactics for randomized LTL model checking. In: Proceedings of VSTTE, pp. 152\u2013169 (2017)"},{"key":"5_CR51","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-16612-9_11","volume-title":"Runtime Verification","author":"Axel Legay","year":"2010","unstructured":"Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Proceedings of RV, pp. 122\u2013135 (2010)"},{"key":"5_CR52","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: How to cook a temporal proof system for your pet language. In: Proceedings of POPL, pp. 141\u2013154 (1983)","DOI":"10.1145\/567067.567082"},{"key":"5_CR53","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems, Specification. Springer, Berlin (1991)","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"5_CR54","doi-asserted-by":"crossref","unstructured":"Mazurkiewicz, A.W.: Trace theory. In: Proceedings of Advances in Petri Nets, pp. 279\u2013324 (1986)","DOI":"10.1007\/3-540-17906-2_30"},{"key":"5_CR55","volume-title":"Code Complete - A Practical Handbook of Software Construction","author":"S McConnel","year":"2004","unstructured":"McConnel, S.: Code Complete - A Practical Handbook of Software Construction, 2nd edn. Microsoft Press, Redmond (2004)","edition":"2"},{"key":"5_CR56","first-page":"1","volume-title":"Computer Aided Verification","author":"K. L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Proceedings of CAV, pp. 1\u201313 (2003)"},{"key":"5_CR57","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/10722167_25","volume-title":"Computer Aided Verification","author":"Kenneth L. McMillan","year":"2000","unstructured":"McMillan, K.L., Qadeer, S., Saxe, J.B.: Induction in compositional model checking. In: Proceedings of CAV, pp. 312\u2013327 (2000)"},{"key":"5_CR58","unstructured":"Meyers, G.J.: The Art of Software Testing. Wiley, Hoboken (1979). 1989, ISBN 978-0-13-115007-2, pp. I-XI, 1\u2013260"},{"key":"5_CR59","unstructured":"Milner, R.: Communication and Concurrency. PHI Series in Computer Science. Prentice Hall, Upper Saddle River (1989)"},{"key":"5_CR60","first-page":"1","volume-title":"Computer Science Logic","author":"Peter O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Proceedings of CSL, pp. 1\u201319 (2001)"},{"key":"5_CR61","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S Owicki","year":"1976","unstructured":"Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. Acta Informatic 6, 319\u2013340 (1976)","journal-title":"Acta Informatic"},{"key":"5_CR62","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction\u2014CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Proceedings of CADE, pp. 748\u2013752 (1992)"},{"key":"5_CR63","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/3-540-56922-7_34","volume-title":"Computer Aided Verification","author":"Doron Peled","year":"1993","unstructured":"Peled, D.A.: All from one, one for all, on model checking using representatives. In: Proceedings of CAV, pp. 409\u2013423 (1993)"},{"key":"5_CR64","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of FOCS, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"5_CR65","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of POPL, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"5_CR66","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: Proceedings of FOCS, pp. 746\u2013757 (1990)","DOI":"10.1109\/FSCS.1990.89597"},{"key":"5_CR67","first-page":"337","volume-title":"Lecture Notes in Computer Science","author":"J. P. Queille","year":"1982","unstructured":"Queille, J.-P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. Symposium on Programming, pp. 337\u2013351 (1982)"},{"key":"5_CR68","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of LICS, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"5_CR69","unstructured":"Ryan, P.Y.A., Schneider, S.A.: Modelling and Analysis of Security Protocols, pp. 1\u2013300. Addison-Wesley-Longman, Boston (2001)"},{"key":"5_CR70","doi-asserted-by":"crossref","unstructured":"Safra, S.: On the complexity of omega-automata. In: Proceedings of FOCS, pp. 319\u2013327 (1988)","DOI":"10.1109\/SFCS.1988.21948"},{"issue":"4","key":"5_CR71","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1145\/265924.265927","volume":"15","author":"S Savage","year":"1997","unstructured":"Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.: Eraser: a dynamic data race detector for multithreaded programs. ACM Trans. Comput. Syst. 15(4), 391\u2013411 (1997)","journal-title":"ACM Trans. Comput. Syst."},{"key":"5_CR72","doi-asserted-by":"crossref","unstructured":"Sen, K., Agha, G.: CUTE and jCUTE: concolic unit testing and explicit path model-checking tools. In: Proceedings of CAV, pp. 419\u2013423 (2006)","DOI":"10.1007\/11817963_38"},{"issue":"6","key":"5_CR73","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1145\/1064978.1065045","volume":"40","author":"Armando Solar-Lezama","year":"2005","unstructured":"Solar-Lezama, A., Rabbah, R.M., Bodik, R., Ebciogl, K.: Programming by sketching for bit-streaming programs. In: Proceedings of PLDI, pp. 281\u2013294 (2005)","journal-title":"ACM SIGPLAN Notices"},{"key":"5_CR74","first-page":"133","volume-title":"Formal Models and Semantics","author":"Wolfgang THOMAS","year":"1990","unstructured":"Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics (B), pp. 133\u2013192. MIT Press, Cambridge (1990)"},{"key":"5_CR75","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/3-540-53863-1_36","volume-title":"Advances in Petri Nets 1990","author":"Antti Valmari","year":"1991","unstructured":"Valmari, A.: Stubborn sets for reduced state space generation. In: Proceedings of Applications and Theory of Petri Nets, pp. 491\u2013515 (1989)"},{"key":"5_CR76","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (Preliminary Report). In: Proceedings of LICS, pp. 332\u2013344 (1986)"},{"key":"5_CR77","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/BFb0055048","volume-title":"Automata, Languages and Programming","author":"Igor Walukiewicz","year":"1998","unstructured":"Walukiewicz, I.: Difficult configurations - on the complexity of LTrL. In: Proceedings of ICALP, pp. 140\u2013151 (1998)"},{"key":"5_CR78","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/3-540-17906-2_31","volume-title":"Petri Nets: Applications and Relationships to Other Models of Concurrency","author":"Glynn Winskel","year":"1987","unstructured":"Winskel, G.: Event structures. In: Proceedings of Advances in Petri Nets, pp. 325\u2013392 (1986)"},{"key":"5_CR79","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-45657-0_17","volume-title":"Computer Aided Verification","author":"H\u00e5kan L. S. Younes","year":"2002","unstructured":"Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Proceedings of CAV, pp. 223\u2013235 (2002)"},{"issue":"1\u20132","key":"5_CR80","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/S0304-3975(98)00009-7","volume":"200","author":"W Zielonka","year":"1998","unstructured":"Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci. 200(1\u20132), 135\u2013183 (1998)","journal-title":"Theor. Comput. Sci."}],"container-title":["Handbook of Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-00262-6_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,16]],"date-time":"2019-11-16T11:55:13Z","timestamp":1573905313000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-00262-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030002619","9783030002626"],"references-count":80,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-00262-6_5","relation":{},"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"12 February 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}