{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T02:47:37Z","timestamp":1742957257099,"version":"3.40.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319899626"},{"type":"electronic","value":"9783319899633"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89963-3_2","type":"book-chapter","created":{"date-parts":[[2018,4,13]],"date-time":"2018-04-13T14:53:00Z","timestamp":1523631180000},"page":"20-37","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Fine-Grained Complexity of Safety Verification"],"prefix":"10.1007","author":[{"given":"Peter","family":"Chini","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roland","family":"Meyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Prakash","family":"Saivasan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,4,14]]},"reference":[{"key":"2_CR1","unstructured":"Atig, M.F., Bouajjani, A., Kumar, K.N., Saivasan, P.: On bounded reachability analysis of shared memory systems. In: FSTTCS, LIPIcs, vol. 29, pp. 611\u2013623. Schloss Dagstuhl (2014)"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-00768-2_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"MF Atig","year":"2009","unstructured":"Atig, M.F., Bouajjani, A., Qadeer, S.: Context-bounded analysis for concurrent programs with dynamic creation of threads. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 107\u2013123. Springer, Heidelberg (2009). \n                      https:\/\/doi.org\/10.1007\/978-3-642-00768-2_11"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/978-3-540-85361-9_29","volume-title":"CONCUR 2008 - Concurrency Theory","author":"MF Atig","year":"2008","unstructured":"Atig, M.F., Bouajjani, A., Touili, T.: On the reachability analysis of acyclic networks of pushdown systems. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 356\u2013371. Springer, Heidelberg (2008). \n                      https:\/\/doi.org\/10.1007\/978-3-540-85361-9_29"},{"issue":"8","key":"2_CR4","first-page":"423","volume":"75","author":"HL Bodlaender","year":"2009","unstructured":"Bodlaender, H.L., Downey, R.G., Fellows, M.R., Hermelin, D.: On problems without polynomial kernels. JCSS 75(8), 423\u2013434 (2009)","journal-title":"JCSS"},{"issue":"1","key":"2_CR5","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1137\/120880240","volume":"28","author":"HL Bodlaender","year":"2014","unstructured":"Bodlaender, H.L., Jansen, B.M.P., Kratsch, S.: Kernelization lower bounds by cross-composition. SIDAM 28(1), 277\u2013305 (2014)","journal-title":"SIDAM"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-3-642-11269-0_6","volume-title":"Parameterized and Exact Computation","author":"C Calabro","year":"2009","unstructured":"Calabro, C., Impagliazzo, R., Paturi, R.: The complexity of satisfiability of small depth circuits. In: Chen, J., Fomin, F.V. (eds.) IWPEC 2009. LNCS, vol. 5917, pp. 75\u201385. Springer, Heidelberg (2009). \n                      https:\/\/doi.org\/10.1007\/978-3-642-11269-0_6"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Cantin, J.F., Lipasti, M.H., Smith, J.E.: The complexity of verifying memory coherence. In: SPAA, pp. 254\u2013255. ACM (2003)","DOI":"10.1145\/777412.777457"},{"key":"2_CR8","unstructured":"Chini, P., Kolberg, J., Krebs, A., Meyer, R., Saivasan, P.: On the complexity of bounded context switching. In: ESA, LIPIcs, vol. 87, pp. 27:1\u201327:15. Schloss Dagstuhl (2017)"},{"key":"2_CR9","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-89963-3_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Peter Chini","year":"2018","unstructured":"Chini, P., Meyer, R., Saivasan, P.: Fine-grained complexity of safety verification. CoRR, abs\/1802.05559 (2018)"},{"issue":"3","key":"2_CR10","first-page":"41:1","volume":"12","author":"M Cygan","year":"2016","unstructured":"Cygan, M., Dell, H., Lokshtanov, D., Marx, D., Nederlof, J., Okamoto, Y., Paturi, R., Saurabh, S., Wahlstr\u00f6m, M.: On problems as hard as CNF-SAT. ACM TALG 12(3), 41:1\u201341:24 (2016)","journal-title":"ACM TALG"},{"key":"2_CR11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21275-3","volume-title":"Parameterized Algorithms","author":"M Cygan","year":"2015","unstructured":"Cygan, M., Fomin, F.V., Kowalik, \u0141., Lokshtanov, D., Marx, D., Pilipczuk, M., Pilipczuk, M., Saurabh, S.: Parameterized Algorithms. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-21275-3"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"620","DOI":"10.1007\/3-540-45841-7_51","volume-title":"STACS 2002","author":"S Demri","year":"2002","unstructured":"Demri, S., Laroussinie, F., Schnoebelen, P.: A parametric analysis of the state explosion problem in model checking. In: Alt, H., Ferreira, A. (eds.) STACS 2002. LNCS, vol. 2285, pp. 620\u2013631. Springer, Heidelberg (2002). \n                      https:\/\/doi.org\/10.1007\/3-540-45841-7_51"},{"key":"2_CR13","series-title":"Texts in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-5559-1","volume-title":"Fundamentals of Parameterized Complexity","author":"RG Downey","year":"2013","unstructured":"Downey, R.G., Fellows, M.R.: Fundamentals of Parameterized Complexity. TCS. Springer, London (2013). \n                      https:\/\/doi.org\/10.1007\/978-1-4471-5559-1"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-319-21690-4_5","volume-title":"Computer Aided Verification","author":"A Durand-Gasselin","year":"2015","unstructured":"Durand-Gasselin, A., Esparza, J., Ganty, P., Majumdar, R.: Model checking parameterized asynchronous shared-memory systems. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 67\u201384. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-21690-4_5"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/978-3-662-49674-9_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Enea","year":"2016","unstructured":"Enea, C., Farzan, A.: On atomicity in presence of non-atomic writes. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 497\u2013514. Springer, Heidelberg (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-662-49674-9_29"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-642-39799-8_8","volume-title":"Computer Aided Verification","author":"J Esparza","year":"2013","unstructured":"Esparza, J., Ganty, P., Majumdar, R.: Parameterized verification of asynchronous shared-memory systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 124\u2013140. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-39799-8_8"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-642-00768-2_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Farzan","year":"2009","unstructured":"Farzan, A., Madhusudan, P.: The complexity of predicting atomicity violations. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 155\u2013169. Springer, Heidelberg (2009). \n                      https:\/\/doi.org\/10.1007\/978-3-642-00768-2_14"},{"issue":"4","key":"2_CR18","first-page":"747","volume":"81","author":"H Fernau","year":"2015","unstructured":"Fernau, H., Heggernes, P., Villanger, Y.: A multi-parameter analysis of hard problems on deterministic finite automata. JCSS 81(4), 747\u2013765 (2015)","journal-title":"JCSS"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-319-40946-7_8","volume-title":"Implementation and Application of Automata","author":"H Fernau","year":"2016","unstructured":"Fernau, H., Krebs, A.: Problems on finite automata and the exponential time hypothesis. In: Han, Y.-S., Salomaa, K. (eds.) CIAA 2016. LNCS, vol. 9705, pp. 89\u2013100. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-40946-7_8"},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/3-540-45927-8_19","volume-title":"Programming Languages and Systems","author":"C Flanagan","year":"2002","unstructured":"Flanagan, C., Freund, S.N., Qadeer, S.: Thread-modular verification for shared-memory programs. In: Le M\u00e9tayer, D. (ed.) ESOP 2002. LNCS, vol. 2305, pp. 262\u2013277. Springer, Heidelberg (2002). \n                      https:\/\/doi.org\/10.1007\/3-540-45927-8_19"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-44829-2_14","volume-title":"Model Checking Software","author":"C Flanagan","year":"2003","unstructured":"Flanagan, C., Qadeer, S.: Thread-modular model checking. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 213\u2013224. Springer, Heidelberg (2003). \n                      https:\/\/doi.org\/10.1007\/3-540-44829-2_14"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-319-63390-9_9","volume-title":"Computer Aided Verification","author":"M Fortin","year":"2017","unstructured":"Fortin, M., Muscholl, A., Walukiewicz, I.: Model-checking linear-time properties of parametrized asynchronous shared-memory pushdown systems. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 155\u2013175. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-63390-9_9"},{"issue":"1","key":"2_CR23","first-page":"91","volume":"77","author":"L Fortnow","year":"2011","unstructured":"Fortnow, L., Santhanam, R.: Infeasibility of instance compression and succinct PCPs for NP. JCSS 77(1), 91\u2013106 (2011)","journal-title":"JCSS"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Furbach, F., Meyer, R., Schneider, K., Senftleben, M.: Memory model-aware testing - a unified complexity analysis. In: ACSD, pp. 92\u2013101. IEEE (2014)","DOI":"10.1109\/ACSD.2014.27"},{"issue":"4","key":"2_CR25","doi-asserted-by":"publisher","first-page":"1208","DOI":"10.1137\/S0097539794279614","volume":"26","author":"PB Gibbons","year":"1997","unstructured":"Gibbons, P.B., Korach, E.: Testing shared memories. SIAM J. Comput. 26(4), 1208\u20131244 (1997)","journal-title":"SIAM J. Comput."},{"issue":"6","key":"2_CR26","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1145\/1273442.1250765","volume":"42","author":"Alexey Gotsman","year":"2007","unstructured":"Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Thread-modular shape analysis. In: PLDI, pp. 266\u2013277. ACM (2007)","journal-title":"ACM SIGPLAN Notices"},{"key":"2_CR27","unstructured":"Hague, M.: Parameterised pushdown systems with non-atomic writes. In: FSTTCS, LIPIcs, vol. 13, pp. 457\u2013468. Schloss Dagstuhl (2011)"},{"key":"2_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-642-31424-7_22","volume-title":"Computer Aided Verification","author":"M Hague","year":"2012","unstructured":"Hague, M., Lin, A.W.: Synchronisation- and reversal-bounded analysis of multithreaded programs with counters. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 260\u2013276. Springer, Heidelberg (2012). \n                      https:\/\/doi.org\/10.1007\/978-3-642-31424-7_22"},{"key":"2_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-319-66706-5_9","volume-title":"Static Analysis","author":"L Hol\u00edk","year":"2017","unstructured":"Hol\u00edk, L., Meyer, R., Vojnar, T., Wolff, S.: Effect summaries for thread-modular analysis. In: Ranzato, F. (ed.) SAS 2017. LNCS, vol. 10422, pp. 169\u2013191. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-66706-5_9"},{"issue":"2","key":"2_CR30","first-page":"367","volume":"62","author":"R Impagliazzo","year":"2001","unstructured":"Impagliazzo, R., Paturi, R.: On the complexity of k-SAT. JCSS 62(2), 367\u2013375 (2001)","journal-title":"JCSS"},{"key":"2_CR31","doi-asserted-by":"crossref","unstructured":"Kahlon, V.: Parameterization as abstraction: a tractable approach to the dataflow analysis of concurrent programs. In: LICS, pp. 181\u2013192. IEEE (2008)","DOI":"10.1109\/LICS.2008.37"},{"key":"2_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"629","DOI":"10.1007\/978-3-642-14295-6_54","volume-title":"Computer Aided Verification","author":"S La Torre","year":"2010","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: Model-checking parameterized concurrent programs using linear interfaces. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 629\u2013644. Springer, Heidelberg (2010). \n                      https:\/\/doi.org\/10.1007\/978-3-642-14295-6_54"},{"key":"2_CR33","doi-asserted-by":"publisher","first-page":"760","DOI":"10.1137\/1.9781611973082.60","volume-title":"Proceedings of the Twenty-Second Annual ACM-SIAM Symposium on Discrete Algorithms","author":"Daniel Lokshtanov","year":"2011","unstructured":"Lokshtanov, D., Marx, D., Saurabh, S.: Slightly superexponential parameterized problems. In: SODA, pp. 760\u2013776. SIAM (2011)"},{"key":"2_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-31980-1_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Qadeer","year":"2005","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93\u2013107. Springer, Heidelberg (2005). \n                      https:\/\/doi.org\/10.1007\/978-3-540-31980-1_7"},{"key":"2_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/3-540-44674-5_26","volume-title":"Implementation and Application of Automata","author":"H Todd Wareham","year":"2001","unstructured":"Todd Wareham, H.: The parameterized complexity of intersection and composition operations on sets of finite-state automata. In: Yu, S., P\u0103un, A. (eds.) CIAA 2000. LNCS, vol. 2088, pp. 302\u2013310. Springer, Heidelberg (2001). \n                      https:\/\/doi.org\/10.1007\/3-540-44674-5_26"},{"key":"2_CR36","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/0304-3975(83)90020-8","volume":"26","author":"CK Yap","year":"1983","unstructured":"Yap, C.K.: Some consequences of non-uniform conditions on uniform classes. TCS 26, 287\u2013300 (1983)","journal-title":"TCS"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89963-3_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,3]],"date-time":"2020-03-03T03:16:10Z","timestamp":1583205370000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89963-3_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319899626","9783319899633"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89963-3_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"14 April 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Thessaloniki","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 April 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 April 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/index.php\/2018\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}