{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:10:44Z","timestamp":1760202644879,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642329395"},{"type":"electronic","value":"9783642329401"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-32940-1_35","type":"book-chapter","created":{"date-parts":[[2012,9,1]],"date-time":"2012-09-01T20:47:02Z","timestamp":1346532422000},"page":"500-515","source":"Crossref","is-referenced-by-count":18,"title":["Efficient Coverability Analysis by Proof Minimization"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Kaiser","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Wahl","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Abdulla, P.A.: Well (and better) quasi-ordered transition systems. Bulletin of Symbolic Logic\u00a016(4) (2010)","key":"35_CR1","DOI":"10.2178\/bsl\/1294171129"},{"unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Yih-Kuen, T.: General decidability theorems of infinite-state systems. In: Logic in Computer Science, LICS (1996)","key":"35_CR2"},{"doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Iyer, S.P., Nyl\u00e9n, A.: SAT-solving the coverability problem for Petri nets. Formal Methods in System Design, FMSD (2004)","key":"35_CR3","DOI":"10.1023\/B:FORM.0000004786.30007.f8"},{"doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.: The SLAM project: debugging system software via static analysis. In: Principles of Programming Languages, POPL (2002)","key":"35_CR4","DOI":"10.1145\/503272.503274"},{"unstructured":"Berthomieu, B., Vernadat, F.: The Tina tool, release 2.9.6, LAAS\/CNRS (November 2009), http:\/\/homepages.laas.fr\/bernard\/tina\/","key":"35_CR5"},{"doi-asserted-by":"crossref","unstructured":"Cardoza, E., Lipton, R.J., Meyer, A.R.: Exponential space complete problems for Petri nets and commutative semigroups: Preliminary report. In: STOC, pp. 50\u201354 (1976)","key":"35_CR6","DOI":"10.1145\/800113.803630"},{"key":"35_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1007\/978-3-540-31980-1_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2005","unstructured":"Clarke, E., Kroning, D., Sharygina, N., Yorav, K.: SATABS: SAT-Based Predicate Abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 570\u2013574. Springer, Heidelberg (2005)"},{"key":"35_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/3-540-44585-4_28","volume-title":"Computer Aided Verification","author":"G. Delzanno","year":"2001","unstructured":"Delzanno, G., Raskin, J.-F., Van Begin, L.: Attacking Symbolic State Explosion. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 298\u2013310. Springer, Heidelberg (2001)"},{"key":"35_CR9","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":"35_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/978-3-642-22110-1_28","volume-title":"Computer Aided Verification","author":"A. Donaldson","year":"2011","unstructured":"Donaldson, A., Kaiser, A., Kroening, D., Wahl, T.: Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 356\u2013371. Springer, Heidelberg (2011)"},{"doi-asserted-by":"crossref","unstructured":"Emerson, A., Namjoshi, K.K.: On model checking for non-deterministic infinite-state systems. In: Logic in Computer Science (LICS), pp. 70\u201380 (1998)","key":"35_CR11","DOI":"10.1109\/LICS.1998.705644"},{"unstructured":"Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: Logic in Computer Science, LICS (1999)","key":"35_CR12"},{"unstructured":"Esparza, J., Melzer, S.: Verification of safety properties using integer programming: Beyond the state equation. Formal Methods in System Design, FMSD (2000)","key":"35_CR13"},{"key":"35_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-02930-1_16","volume-title":"Automata, Languages and Programming","author":"A. Finkel","year":"2009","unstructured":"Finkel, A., Goubault-Larrecq, J.: Forward Analysis for WSTS, Part\u00a0II: Complete WSTS. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009. LNCS, vol.\u00a05556, pp. 188\u2013199. Springer, Heidelberg (2009)"},{"doi-asserted-by":"crossref","unstructured":"Finkel, A., Raskin, J.-F., Samuelides, M., Begin, L.V.: Monotonic extensions of Petri nets: Forward and backward search revisited. ENTCS (2002)","key":"35_CR15","DOI":"10.1016\/S1571-0661(04)80535-8"},{"doi-asserted-by":"crossref","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theoretical Computer Science, TCS (2001)","key":"35_CR16","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"35_CR17","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.\u00a02648, pp. 213\u2013224. Springer, Heidelberg (2003)"},{"unstructured":"Ganty, P., Meuter, C., Delzanno, G., Kalyon, G., Raskin, J.-F., Van Begin, L.: Symbolic data structure for sets of k-uples. Technical report, Universit\u00e9 Libre de Bruxelles (2007)","key":"35_CR18"},{"key":"35_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/11609773_4","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Ganty","year":"2005","unstructured":"Ganty, P., Raskin, J.-F., Van Begin, L.: A Complete Abstract Interpretation Framework for Coverability Properties of WSTS. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 49\u201364. Springer, Heidelberg (2005)"},{"key":"35_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-540-73094-1_10","volume-title":"Petri Nets and Other Models of Concurrency \u2013 ICATPN 2007","author":"P. Ganty","year":"2007","unstructured":"Ganty, P., Raskin, J.-F., Van Begin, L.: From Many Places to Few: Automatic Abstraction Refinement for Petri Nets. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol.\u00a04546, pp. 124\u2013143. Springer, Heidelberg (2007)"},{"doi-asserted-by":"crossref","unstructured":"Geeraerts, G., Raskin, J.-F., Begin, L.V.: Expand, enlarge and check: New algorithms for the coverability problem of WSTS. JCSS (2006)","key":"35_CR21","DOI":"10.1016\/j.jcss.2005.09.001"},{"key":"35_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-540-75596-8_9","volume-title":"Automated Technology for Verification and Analysis","author":"G. Geeraerts","year":"2007","unstructured":"Geeraerts, G., Raskin, J.-F., Van Begin, L.: On the Efficient Computation of the Minimal Coverability Set for Petri Nets. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol.\u00a04762, pp. 98\u2013113. Springer, Heidelberg (2007)"},{"doi-asserted-by":"crossref","unstructured":"German, S., Sistla, P.: Reasoning about systems with many processes. Journal of the ACM, JACM (1992)","key":"35_CR23","DOI":"10.1145\/146637.146681"},{"key":"35_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/978-3-642-22110-1_32","volume-title":"Computer Aided Verification","author":"A. Gupta","year":"2011","unstructured":"Gupta, A., Popeea, C., Rybalchenko, A.: Threader: A Constraint-Based Verifier for Multi-threaded Programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 412\u2013417. Springer, Heidelberg (2011)"},{"key":"35_CR25","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)"},{"issue":"2","key":"35_CR26","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/S0022-0000(69)80011-5","volume":"3","author":"R.M. Karp","year":"1969","unstructured":"Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci.\u00a03(2), 147\u2013195 (1969)","journal-title":"J. Comput. Syst. Sci."},{"doi-asserted-by":"crossref","unstructured":"Lu, S., Park, S., Seo, E., Zhou, Y.: Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In: Architectural Support for Programming Languages and Operating Systems, ASPLOS (2008)","key":"35_CR27","DOI":"10.1145\/1346281.1346323"},{"key":"35_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/11921240_13","volume-title":"Theoretical Aspects of Computing - ICTAC 2006","author":"A. Malkis","year":"2006","unstructured":"Malkis, A., Podelski, A., Rybalchenko, A.: Thread-Modular Verification Is Cartesian Abstract Interpretation. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol.\u00a04281, pp. 183\u2013197. Springer, Heidelberg (2006)"},{"key":"35_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-642-14295-6_19","volume-title":"Computer Aided Verification","author":"R. Meyer","year":"2010","unstructured":"Meyer, R., Strazny, T.: Petruchio: From Dynamic Networks to Nets. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 175\u2013179. Springer, Heidelberg (2010)"},{"doi-asserted-by":"crossref","unstructured":"Meyer, R., Strazny, T.: An algorithmic framework for coverability in well-structured systems. In: Application of Concurrency to System Design, ACSD (2012)","key":"35_CR30","DOI":"10.1109\/ACSD.2012.26"},{"unstructured":"Peierls, T., Goetz, B., Bloch, J., Bowbeer, J., Lea, D., Holmes, D.: Java Concurrency in Practice. Addison-Wesley Professional (2005)","key":"35_CR31"},{"doi-asserted-by":"crossref","unstructured":"Rackoff, C.: The covering and boundedness problems for vector addition systems. Theoretical Computer Science, TCS (1978)","key":"35_CR32","DOI":"10.1016\/0304-3975(78)90036-1"},{"key":"35_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"616","DOI":"10.1007\/978-3-642-15155-2_54","volume-title":"Mathematical Foundations of Computer Science 2010","author":"P. Schnoebelen","year":"2010","unstructured":"Schnoebelen, P.: Revisiting Ackermann-Hardness for Lossy Counter Machines and Reset Petri Nets. In: Hlin\u011bn\u00fd, P., Ku\u010dera, A. (eds.) MFCS 2010. LNCS, vol.\u00a06281, pp. 616\u2013628. Springer, Heidelberg (2010)"},{"key":"35_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1007\/978-3-642-27940-9_29","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D. Zufferey","year":"2012","unstructured":"Zufferey, D., Wies, T., Henzinger, T.A.: Ideal Abstractions for Well-Structured Transition Systems. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol.\u00a07148, pp. 445\u2013460. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","CONCUR 2012 \u2013 Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-32940-1_35.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T18:06:27Z","timestamp":1744049187000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-32940-1_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642329395","9783642329401"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-32940-1_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}