{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,11]],"date-time":"2026-07-11T03:30:20Z","timestamp":1783740620688,"version":"3.55.0"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319415277","type":"print"},{"value":"9783319415284","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"vor","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":[[2016]]},"DOI":"10.1007\/978-3-319-41528-4_15","type":"book-chapter","created":{"date-parts":[[2016,7,12]],"date-time":"2016-07-12T09:34:06Z","timestamp":1468316046000},"page":"271-291","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":26,"title":["Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations"],"prefix":"10.1007","author":[{"given":"Jakub","family":"Daniel","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alberto","family":"Griggio","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stefano","family":"Tonetta","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sergio","family":"Mover","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,7,13]]},"reference":[{"issue":"2","key":"15_CR1","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1016\/j.tcs.2005.11.026","volume":"354","author":"R Alur","year":"2006","unstructured":"Alur, R., Dang, T., Ivancic, F.: Counterexample-guided predicate abstraction of hybrid systems. Theor. Comput. Sci. 354(2), 250\u2013271 (2006)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"15_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11562436_1","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2005","author":"I Balaban","year":"2005","unstructured":"Balaban, I., Pnueli, A., Zuck, L.D.: Ranking abstraction as companion to predicate abstraction. In: Wang, F. (ed.) FORTE 2005. LNCS, vol. 3731, pp. 1\u201312. Springer, Heidelberg (2005)"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in BIP. In: SEFM, pp. 3\u201312. IEEE Computer Society (2006)","DOI":"10.1109\/SEFM.2006.27"},{"key":"15_CR5","doi-asserted-by":"crossref","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: Hybrid Systems, pp. 232\u2013243 (1995)"},{"issue":"2","key":"15_CR6","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1016\/S1571-0661(04)80410-9","volume":"66","author":"A Biere","year":"2002","unstructured":"Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. Electr. Notes Theor. Comput. Sci. 66(2), 160\u2013177 (2002)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-319-24953-7_25","volume-title":"Automated Technology for Verification and Analysis","author":"S Bliudze","year":"2015","unstructured":"Bliudze, S., Cimatti, A., Jaber, M., Mover, S., Roveri, M., Saab, W., Wang, Q.: Formal verification of infinite-state BIP models. In: Finkbeiner, B., et al. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 326\u2013343. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-24953-7_25"},{"issue":"3","key":"15_CR8","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/j.entcs.2005.02.061","volume":"138","author":"A Bouajjani","year":"2005","unstructured":"Bouajjani, A., Legay, A., Wolper, P.: Handling liveness properties in ($$\\omega $$-)regular model checking. Electr. Notes Theor. Comput. Sci. 138(3), 101\u2013115 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"15_CR9","doi-asserted-by":"publisher","first-page":"464","DOI":"10.1016\/j.scico.2014.06.003","volume":"98","author":"M Bozzano","year":"2015","unstructured":"Bozzano, M., Cimatti, A., Lisagor, O., Mattarei, C., Mover, S., Roveri, M., Tonetta, S.: Safety assessment of AltaRica models via symbolic model checking. Sci. Comput. Program. 98, 464\u2013483 (2015)","journal-title":"Sci. Comput. Program."},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011)"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-642-39799-8_28","volume-title":"Computer Aided Verification","author":"M Brockschmidt","year":"2013","unstructured":"Brockschmidt, M., Cook, B., Fuhs, C.: Better termination proving through cooperation. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 413\u2013429. Springer, Heidelberg (2013)"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"Computer Aided Verification","author":"R Cavada","year":"2014","unstructured":"Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334\u2013342. Springer, Heidelberg (2014)"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-642-22110-1_24","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2011","unstructured":"Cimatti, A., Griggio, A., Micheli, A., Narasamdya, I., Roveri, M.: Kratos \u2013 a software model checker for systemC. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 310\u2013316. Springer, Heidelberg (2011)"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-642-54862-8_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2014","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: IC3 modulo theories via implicit predicate abstraction. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 46\u201361. Springer, Heidelberg (2014)"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"424","DOI":"10.1007\/978-3-319-08867-9_28","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2014","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Verifying LTL properties of hybrid systems with K-Liveness. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 424\u2013440. Springer, Heidelberg (2014)"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/978-3-662-46681-0_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2015","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: HyComp: an SMT-based model checker for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 52\u201367. Springer, Heidelberg (2015)"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The mathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 93\u2013107. Springer, Heidelberg (2013)"},{"key":"15_CR18","unstructured":"Claessen, K., S\u00f6rensson, N.: A liveness checking algorithm that counts. In: FMCAD, pp. 52\u201359. IEEE (2012)"},{"issue":"5","key":"15_CR19","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":"15_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"384","DOI":"10.1007\/978-3-662-46681-0_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B Cook","year":"2015","unstructured":"Cook, B., Khlaaf, H., Piterman, N.: Fairness for infinite-state systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 384\u2013398. Springer, Heidelberg (2015)"},{"key":"15_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/978-3-319-21690-4_2","volume-title":"Computer Aided Verification","author":"B Cook","year":"2015","unstructured":"Cook, B., Khlaaf, H., Piterman, N.: On automation of CTL* verification for infinite-state systems. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 13\u201329. Springer, Heidelberg (2015)"},{"key":"15_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-642-22110-1_26","volume-title":"Computer Aided Verification","author":"B Cook","year":"2011","unstructured":"Cook, B., Koskinen, E., Vardi, M.: Temporal property verification as a program analysis task. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 333\u2013348. Springer, Heidelberg (2011)"},{"issue":"6","key":"15_CR23","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1145\/1133255.1134029","volume":"41","author":"Byron Cook","year":"2006","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI, pp. 415\u2013426 (2006)","journal-title":"ACM SIGPLAN Notices"},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-319-21690-4_4","volume-title":"Computer Aided Verification","author":"D Dietsch","year":"2015","unstructured":"Dietsch, D., Heizmann, M., Langenfeld, V., Podelski, A.: Fairness modulo theory: a new approach to LTL software model checking. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 49\u201366. Springer, Heidelberg (2015)"},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/10722167_20","volume-title":"Computer Aided Verification","author":"J Esparza","year":"2000","unstructured":"Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 232\u2013247. Springer, Heidelberg (2000)"},{"key":"15_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) Computer Aided Verification. LNCS, vol. 2102, pp. 53\u201365. Springer, Heidelberg (2001)"},{"key":"15_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-14203-1_3","volume-title":"Automated Reasoning","author":"S Ghilardi","year":"2010","unstructured":"Ghilardi, S., Ranise, S.: MCMT: a model checker modulo theories. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 22\u201329. Springer, Heidelberg (2010)"},{"key":"15_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"issue":"6","key":"15_CR29","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1145\/2345156.2254112","volume":"47","author":"Sergey Grebenshchikov","year":"2012","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI, pp. 405\u2013416. ACM (2012)","journal-title":"ACM SIGPLAN Notices"},{"key":"15_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/978-3-319-02444-8_26","volume-title":"Automated Technology for Verification and Analysis","author":"M Heizmann","year":"2013","unstructured":"Heizmann, M., Hoenicke, J., Leike, J., Podelski, A.: Linear ranking for linear lasso programs. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 365\u2013380. Springer, Heidelberg (2013)"},{"key":"15_CR31","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Jhala, R., Majumdar, R., McMillan, K.: Abstractions from proofs. In: POPL, pp. 232\u2013244 (2004)","DOI":"10.1145\/982962.964021"},{"key":"15_CR32","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Kopke, P., Puri, A., Varaiya, P.: What\u2019s decidable about hybrid automata? In: STOC, pp. 373\u2013382 (1995)","DOI":"10.1145\/225058.225162"},{"key":"15_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/11817963_39","volume-title":"Computer Aided Verification","author":"SK Lahiri","year":"2006","unstructured":"Lahiri, S.K., Nieuwenhuis, R., Oliveras, A.: SMT techniques for fast predicate abstraction. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 424\u2013437. Springer, Heidelberg (2006)"},{"key":"15_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"15_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1007\/978-3-540-27813-9_45","volume-title":"Computer Aided Verification","author":"L de Moura","year":"2004","unstructured":"de Moura, L., Owre, S., Rue\u00df, H., Rushby, J., Shankar, N., Sorea, M., Tiwari, A.: SAL 2. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 496\u2013500. Springer, Heidelberg (2004)"},{"key":"15_CR36","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Turbo-charging lemmas on demand with don\u2019t care reasoning. In: FMCAD, pp. 179\u2013186. IEEE (2014)","DOI":"10.1109\/FMCAD.2014.6987611"},{"key":"15_CR37","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"15_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239\u2013251. Springer, Heidelberg (2004)"},{"key":"15_CR39","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS, pp. 32\u201341. IEEE Computer Society (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"issue":"3","key":"15_CR40","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1145\/1232420.1232422","volume":"29","author":"Andreas Podelski","year":"2007","unstructured":"Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. ACM Trans. Program. Lang. Syst. 29(3) (2007)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"30","key":"15_CR41","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1112\/plms\/s2-30.1.264","volume":"3","author":"FP Ramsey","year":"1930","unstructured":"Ramsey, F.P.: On a problem in formal logic. Proc. Lond. Math. Soc. 3(30), 264\u2013286 (1930)","journal-title":"Proc. Lond. Math. Soc."},{"issue":"1","key":"15_CR42","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/j.entcs.2005.11.018","volume":"149","author":"V Schuppan","year":"2006","unstructured":"Schuppan, V., Biere, A.: Liveness checking as safety checking for infinite state spaces. Electron. Notes Theor. Comput. Sci. 149(1), 79\u201396 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"15_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"725","DOI":"10.1007\/978-3-642-31424-7_56","volume-title":"Computer Aided Verification","author":"A Tiwari","year":"2012","unstructured":"Tiwari, A.: HybridSAL relational abstracter. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 725\u2013731. Springer, Heidelberg (2012)"},{"key":"15_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-642-05089-3_7","volume-title":"FM 2009: Formal Methods","author":"S Tonetta","year":"2009","unstructured":"Tonetta, S.: Abstract model checking without computing the abstraction. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 89\u2013105. Springer, Heidelberg (2009)"},{"key":"15_CR45","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency","author":"Moshe Y. Vardi","year":"1996","unstructured":"Vardi, M.: An Automata-theoretic approach to linear temporal logic. In: Banff Higher Order Workshop, pp. 238\u2013266 (1995)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-41528-4_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,4]],"date-time":"2025-06-04T00:41:29Z","timestamp":1748997689000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41528-4_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319415277","9783319415284"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41528-4_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"13 July 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Toronto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}