{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T04:14:00Z","timestamp":1748751240849,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662491218"},{"type":"electronic","value":"9783662491225"}],"license":[{"start":{"date-parts":[[2015,12,25]],"date-time":"2015-12-25T00:00:00Z","timestamp":1451001600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49122-5_7","type":"book-chapter","created":{"date-parts":[[2015,12,24]],"date-time":"2015-12-24T05:01:36Z","timestamp":1450933296000},"page":"147-165","source":"Crossref","is-referenced-by-count":0,"title":["Lazy Constrained Monotonic Abstraction"],"prefix":"10.1007","author":[{"given":"Zeinab","family":"Ganjei","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ahmed","family":"Rezine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Petru","family":"Eles","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zebo","family":"Peng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,12,25]]},"reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-540-73368-3_17","volume-title":"Computer Aided Verification","author":"PA Abdulla","year":"2007","unstructured":"Abdulla, P.A., Delzanno, G., Rezine, A.: Parameterized verification of infinite-state processes with global conditions. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 145\u2013157. Springer, Heidelberg (2007)"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., \u010cer\u0101ns, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: Proceedigs of the LICS 1996, $$11^{th}$$ IEEE International Symposium on Logic in Computer Science, pp. 313\u2013321 (1996)","DOI":"10.1109\/LICS.1996.561359"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-642-15375-4_7","volume-title":"CONCUR 2010 - Concurrency Theory","author":"PA Abdulla","year":"2010","unstructured":"Abdulla, P.A., Chen, Y.-F., Delzanno, G., Haziza, F., Hong, C.-D., Rezine, A.: Constrained monotonic abstraction: a CEGAR for parameterized verification. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 86\u2013101. Springer, Heidelberg (2010)"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1007\/978-3-540-71209-1_56","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PA Abdulla","year":"2007","unstructured":"Abdulla, P.A., Delzanno, G., Ben Henda, N., Rezine, A.: Regular model checking without transducers (on efficient verification of parameterized systems). In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 721\u2013736. Springer, Heidelberg (2007)"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The SLAM Project: debugging system software via static analysis. In: Proceedings of the 29th ACM SIGPLAN-SIGACT, POPL 2002, pp. 1\u20133. ACM, New York (2002)","DOI":"10.1145\/565816.503274"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1007\/978-3-540-24730-2_42","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Bardin","year":"2004","unstructured":"Bardin, S., Finkel, A., Leroux, J.: FASTer acceleration of counter automata in practice. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 576\u2013590. Springer, Heidelberg (2004)"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/11817963_9","volume-title":"Computer Aided Verification","author":"S Bardin","year":"2006","unstructured":"Bardin, S., Leroux, J., Point, G.: FAST extended release. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 63\u201366. Springer, Heidelberg (2006)"},{"key":"7_CR8","unstructured":"Bonnet, R., Finkel, A., Leroux, J., Zeitoun, M.: Model checking vector addition systems with one zero-test (2012). arXiv preprint arXiv:1205.4458"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/11817963_47","volume-title":"Computer Aided Verification","author":"A Bouajjani","year":"2006","unstructured":"Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: Programs with lists are counter automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 517\u2013531. Springer, Heidelberg (2006)"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: SATABS: SAT-based predicate abstraction for ANSI-C. In: TACAS, pp. 570\u2013574. Springer (2005)","DOI":"10.1007\/978-3-540-31980-1_40"},{"issue":"8","key":"7_CR11","doi-asserted-by":"crossref","first-page":"150","DOI":"10.1145\/2858788.2688519","volume":"50","author":"Tiago Cogumbreiro","year":"2015","unstructured":"Cogumbreiro, T., Hu, R., Martins, F., Yoshida, N.: Dynamic deadlock verification for general barrier synchronisation. In: Proceeding of the 20th ACM SIGPLAN PPoPP Symposium, pp. 150\u2013160. ACM (2015)","journal-title":"ACM SIGPLAN Notices"},{"key":"7_CR12","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.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/10722167_8","volume-title":"Computer Aided Verification","author":"G Delzanno","year":"2000","unstructured":"Delzanno, G.: Automatic verification of parameterized cache coherence protocols. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 53\u201368. Springer, Heidelberg (2000)"},{"issue":"1","key":"7_CR14","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/s10703-012-0155-3","volume":"41","author":"AF Donaldson","year":"2012","unstructured":"Donaldson, A.F., Kaiser, A., Kroening, D., Tautschnig, M., Wahl, T.: Counterexample-guided abstraction refinement for symmetric concurrent programs. Formal Meth. Syst. Des. 41(1), 25\u201344 (2012)","journal-title":"Formal Meth. Syst. Des."},{"key":"7_CR15","unstructured":"Downey, A.: The Little Book of SEMAPHORES (2nd Edition): The Ins and Outs of Concurrency Control and Common Mistakes. Createspace Ind, Pub (2009). http:\/\/www.greenteapress.com\/semaphores\/"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Farzan, A., Kincaid, Z., Podelski, A.: Proofs that count. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, pp. 151\u2013164. ACM, New York (2014)","DOI":"10.1145\/2535838.2535885"},{"issue":"1\u20132","key":"7_CR17","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A Finkel","year":"2001","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere!. Theor. Comput. Sci. 256(1\u20132), 63\u201392 (2001)","journal-title":"Theor. Comput. Sci."},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1007\/978-3-662-46081-8_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Z Ganjei","year":"2015","unstructured":"Ganjei, Z., Rezine, A., Eles, P., Peng, Z.: Abstracting and counting synchronizing processes. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 227\u2013244. Springer, Heidelberg (2015)"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/11513988_38","volume-title":"Computer Aided Verification","author":"G Geeraerts","year":"2005","unstructured":"Geeraerts, G., Raskin, J.-F., Van Begin, L.: Expand, enlarge and check.. made efficient. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 394\u2013407. Springer, Heidelberg (2005)"},{"key":"7_CR20","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)"},{"issue":"1","key":"7_CR21","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1145\/565816.503279","volume":"37","author":"Thomas A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of the 29th ACM SIGPLAN-SIGACT, POPL 2002, pp. 58\u201370. ACM, New York (2002)","journal-title":"ACM SIGPLAN Notices"},{"issue":"1","key":"7_CR22","doi-asserted-by":"crossref","first-page":"326","DOI":"10.1112\/plms\/s3-2.1.326","volume":"s3-2","author":"Graham Higman","year":"1952","unstructured":"Higman, G.; Ordering by divisibility in abstract algebras. In: Proceedings of the London Mathematical Society, pp. 326\u2013336 (1952)","journal-title":"Proceedings of the London Mathematical Society"},{"key":"7_CR23","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. 7454, pp. 500\u2013515. Springer, Heidelberg (2012)"},{"key":"7_CR24","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. 8044, pp. 158\u2013173. Springer, Heidelberg (2013)"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Liu, P., Wahl, T.: Infinite-state backward exploration of boolean broadcast programs. In: Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design, pp. 155\u2013162. FMCAD Inc (2014)","DOI":"10.1109\/FMCAD.2014.6987608"},{"key":"7_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123\u2013136. Springer, Heidelberg (2006)"},{"key":"7_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"556","DOI":"10.1007\/978-3-642-28756-5_48","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Weissenbacher","year":"2012","unstructured":"Weissenbacher, G., Kroening, D., Malik, S.: Wolverine: battling bugs with interpolants. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 556\u2013558. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49122-5_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T22:49:38Z","timestamp":1748731778000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49122-5_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12,25]]},"ISBN":["9783662491218","9783662491225"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49122-5_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015,12,25]]}}}