{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,18]],"date-time":"2026-06-18T04:26:52Z","timestamp":1781756812075,"version":"3.54.5"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319088662","type":"print"},{"value":"9783319088679","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08867-9_40","type":"book-chapter","created":{"date-parts":[[2014,6,28]],"date-time":"2014-06-28T11:37:30Z","timestamp":1403955450000},"page":"603-619","source":"Crossref","is-referenced-by-count":45,"title":["An SMT-Based Approach to Coverability Analysis"],"prefix":"10.1007","author":[{"given":"Javier","family":"Esparza","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rusl\u00e1n","family":"Ledesma-Garza","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Philipp","family":"Meyer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Filip","family":"Niksic","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"40_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/978-3-642-28756-5_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Bouajjani","year":"2012","unstructured":"Bouajjani, A., Emmi, M.: Bounded phase analysis of message-passing programs. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 451\u2013465. Springer, Heidelberg (2012)"},{"key":"40_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"40_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/3-540-46002-0_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Delzanno","year":"2002","unstructured":"Delzanno, G., Raskin, J.-F., Van Begin, L.: Towards the automated verification of multithreaded java programs. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 173\u2013187. Springer, Heidelberg (2002)"},{"key":"40_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"454","DOI":"10.1007\/978-3-642-38856-9_24","volume-title":"Static Analysis","author":"E. D\u2019Osualdo","year":"2013","unstructured":"D\u2019Osualdo, E., Kochems, J., Ong, C.-H.L.: Automatic verification of Erlang-style concurrency. In: Logozzo, F., F\u00e4hndrich, M. (eds.) Static Analysis. LNCS, vol.\u00a07935, pp. 454\u2013476. Springer, Heidelberg (2013)"},{"issue":"2","key":"40_CR5","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1023\/A:1008743212620","volume":"16","author":"J. Esparza","year":"2000","unstructured":"Esparza, J., Melzer, S.: Verification of safety properties using integer programming: Beyond the state equation. Formal Methods in System Design\u00a016(2), 159\u2013189 (2000)","journal-title":"Formal Methods in System Design"},{"issue":"1","key":"40_CR6","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1145\/2160910.2160915","volume":"34","author":"P. Ganty","year":"2012","unstructured":"Ganty, P., Majumdar, R.: Algorithmic verification of asynchronous programs. ACM Trans. Program. Lang. Syst.\u00a034(1), 6 (2012)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3","key":"40_CR7","first-page":"275","volume":"88","author":"P. Ganty","year":"2008","unstructured":"Ganty, P., Raskin, J.-F., Van Begin, L.: From many places to few: Automatic abstraction refinement for Petri nets. Fundam. Inform.\u00a088(3), 275\u2013305 (2008)","journal-title":"Fundam. Inform."},{"issue":"1","key":"40_CR8","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1016\/j.jcss.2005.09.001","volume":"72","author":"G. Geeraerts","year":"2006","unstructured":"Geeraerts, G., Raskin, J.-F., Begin, L.V.: Expand, enlarge and check: New algorithms for the coverability problem of WSTS. J. Comput. Syst. Sci.\u00a072(1), 180\u2013203 (2006)","journal-title":"J. Comput. Syst. Sci."},{"issue":"3","key":"40_CR9","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"S.M. German","year":"1992","unstructured":"German, S.M., Sistla, A.P.: Reasoning about systems with many processes. Journal of the ACM (JACM)\u00a039(3), 675\u2013735 (1992)","journal-title":"Journal of the ACM (JACM)"},{"key":"40_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1007\/978-3-642-14295-6_55","volume-title":"Computer Aided Verification","author":"A. Kaiser","year":"2010","unstructured":"Kaiser, A., Kroening, D., Wahl, T.: Dynamic cutoff detection in parameterized concurrent programs. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 645\u2013659. Springer, Heidelberg (2010)"},{"key":"40_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/978-3-642-32940-1_35","volume-title":"CONCUR 2012 \u2013 Concurrency Theory","author":"A. Kaiser","year":"2012","unstructured":"Kaiser, A., Kroening, D., Wahl, T.: Efficient coverability analysis by proof minimization. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol.\u00a07454, pp. 500\u2013515. Springer, Heidelberg (2012)"},{"issue":"2","key":"40_CR12","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/S0022-0000(69)80011-5","volume":"3","author":"R. Karp","year":"1969","unstructured":"Karp, R., Miller, R.: Parallel program schemata. J. Comput. Syst. Sci.\u00a03(2), 147\u2013195 (1969)","journal-title":"J. Comput. Syst. Sci."},{"key":"40_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-642-39799-8_10","volume-title":"Computer Aided Verification","author":"J. Kloos","year":"2013","unstructured":"Kloos, J., Majumdar, R., Niksic, F., Piskac, R.: Incremental, inductive coverability. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 158\u2013173. Springer, Heidelberg (2013)"},{"issue":"2","key":"40_CR14","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1145\/5383.5385","volume":"33","author":"L. Lamport","year":"1986","unstructured":"Lamport, L.: The mutual exclusion problem: Part II\u2014statement and solutions. J. ACM\u00a033(2), 327\u2013348 (1986)","journal-title":"J. ACM"},{"key":"40_CR15","doi-asserted-by":"crossref","unstructured":"Majumdar, R., Meyer, R., Wang, Z.: Static provenance verification for message passing programs. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol.\u00a07935, pp. 366\u2013387. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-38856-9_20"},{"issue":"4","key":"40_CR16","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1109\/5.24143","volume":"77","author":"T. Murata","year":"1989","unstructured":"Murata, T.: Petri nets: Properties, analysis and applications. Proceedings of the IEEE\u00a077(4), 541\u2013580 (1989)","journal-title":"Proceedings of the IEEE"},{"key":"40_CR17","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0304-3975(78)90036-1","volume":"6","author":"C. Rackoff","year":"1978","unstructured":"Rackoff, C.: The covering and boundedness problems for vector addition systems. Theor. Comput. Sci.\u00a06, 223\u2013231 (1978)","journal-title":"Theor. Comput. Sci."},{"key":"40_CR18","doi-asserted-by":"crossref","unstructured":"Reisig, W.: Understanding Petri Nets - Modeling Techniques, Analysis Methods, Case Studies. Springer (2013)","DOI":"10.1007\/978-3-642-33278-4"},{"key":"40_CR19","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. John Wiley & Sons Ltd. (1986)"},{"key":"40_CR20","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Tancau, L., Bod\u00edk, R., Seshia, S., Saraswat, V.: Combinatorial sketching for finite programs. In: ASPLOS, pp. 404\u2013415. ACM (2006)","DOI":"10.1145\/1168918.1168907"},{"key":"40_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-642-31131-4_12","volume-title":"Application and Theory of Petri Nets","author":"A. Valmari","year":"2012","unstructured":"Valmari, A., Hansen, H.: Old and new algorithms for minimal coverability sets. In: Haddad, S., Pomello, L. (eds.) PETRI NETS 2012. LNCS, vol.\u00a07347, pp. 208\u2013227. Springer, Heidelberg (2012)"},{"key":"40_CR22","doi-asserted-by":"crossref","unstructured":"Wimmel, H., Wolf, K.: Applying CEGAR to the Petri net state equation. Logical Methods in Computer Science\u00a08(3) (2012)","DOI":"10.2168\/LMCS-8(3:27)2012"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08867-9_40","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T05:16:12Z","timestamp":1558934172000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08867-9_40"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319088662","9783319088679"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08867-9_40","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}