{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,9]],"date-time":"2025-03-09T10:10:09Z","timestamp":1741515009493,"version":"3.38.0"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2011,8,27]],"date-time":"2011-08-27T00:00:00Z","timestamp":1314403200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2012,4]]},"DOI":"10.1007\/s10009-011-0213-y","type":"journal-article","created":{"date-parts":[[2011,8,26]],"date-time":"2011-08-26T11:36:28Z","timestamp":1314358588000},"page":"207-222","source":"Crossref","is-referenced-by-count":5,"title":["A lightweight regular model checking approach for parameterized systems"],"prefix":"10.1007","volume":"14","author":[{"given":"Giorgio","family":"Delzanno","sequence":"first","affiliation":[]},{"given":"Ahmed","family":"Rezine","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2011,8,27]]},"reference":[{"key":"213_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., \u010cer\u0101ns, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. LICS 313\u2013321 (1996)","DOI":"10.1109\/LICS.1996.561359"},{"key":"213_CR2","doi-asserted-by":"crossref","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: CONCUR, pp. 86\u2013101 (2010)","DOI":"10.1007\/978-3-642-15375-4_7"},{"key":"213_CR3","unstructured":"Abdulla, P.A., Ben Henda, N., Delzanno, G., Rezine, A.: Regular model checking without transducers. In: TACAS, pp. 721\u2013736 (2007)"},{"key":"213_CR4","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Ben Henda, N., Delzanno, G., Rezine, A.: Handling parameterized systems with non-atomic global conditions. In: VMCAI, pp. 22\u201336 (2008)","DOI":"10.1007\/978-3-540-78163-9_7"},{"key":"213_CR5","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Delzanno, G., Rezine, A.: Parameterized verification of infinite-state processes with global conditions. In: CAV, pp. 145\u2013157 (2007)","DOI":"10.1007\/978-3-540-73368-3_17"},{"key":"213_CR6","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Delzanno, G., Haziza, F., Rezine, A.: Parameterized tree systems. In: FORTE\u201908, pp. 69\u201383 (2008)","DOI":"10.1007\/978-3-540-68855-6_5"},{"key":"213_CR7","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Delzanno, G., Rezine, A.: Approximated context-sensitive analysis for parameterized verification. In: FMOODS\/FORTE, pp. 41\u201356 (2009)","DOI":"10.1007\/978-3-642-02138-1_3"},{"key":"213_CR8","doi-asserted-by":"crossref","unstructured":"Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.: Parameterized verification with automatically computed inductive assertions. In: CAV, pp. 221\u2013234 (2001)","DOI":"10.1007\/3-540-44585-4_19"},{"key":"213_CR9","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract regular model checking. In: CAV, pp. 372\u2013386 (2004)","DOI":"10.1007\/978-3-540-27813-9_29"},{"issue":"2","key":"213_CR10","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1016\/j.ic.2005.11.007","volume":"205","author":"A. Bouajjani","year":"2007","unstructured":"Bouajjani A., Muscholl A., Touili T.: Permutation rewriting and algorithmic verification. Inf. Comp. 205(2), 199\u2013224 (2007)","journal-title":"Inf. Comp."},{"key":"213_CR11","doi-asserted-by":"crossref","unstructured":"Clarke, E., Talupur, M., Veith, H.: Environment abstraction for parameterized verification. In: VMCAI, pp. 126\u2013141 (2006)","DOI":"10.1007\/11609773_9"},{"issue":"10","key":"213_CR12","doi-asserted-by":"crossref","first-page":"667","DOI":"10.1145\/362759.362813","volume":"14","author":"P.-J. Courtois","year":"1971","unstructured":"Courtois P.-J., Heymans F., Lorge Parnas D.: Concurrent control with \u201creaders\u201d and \u201cwriters\u201d. CACM 14(10), 667\u2013668 (1971)","journal-title":"CACM"},{"issue":"3","key":"213_CR13","first-page":"257","volume":"23","author":"G. Delzanno","year":"2003","unstructured":"Delzanno G.: Constraint-based verification of parameterized cache coherence protocols. FMSD 23(3), 257\u2013301 (2003)","journal-title":"FMSD"},{"key":"213_CR14","doi-asserted-by":"crossref","unstructured":"Emmi, M., Jhala, R., Kohler, E., Majumdar, R.: Verifying reference counted objects. In: TACAS, pp. 352\u2013367 (2009)","DOI":"10.1007\/978-3-642-00768-2_30"},{"issue":"4","key":"213_CR15","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-6(4:10)2010","volume":"6","author":"S. Ghilardi","year":"2010","unstructured":"Ghilardi S., Ranise S.: Backward reachability of array-based systems by SMT solving: termination and invariant synthesis. Log. Methods Comput. Sci. 6(4), 1\u201348 (2010)","journal-title":"Log. Methods Comput. Sci."},{"key":"213_CR16","doi-asserted-by":"crossref","unstructured":"Gribomont, E., Zenner, G.: Automated verification of Szymanski\u2019s algorithm. In: TACAS, pp. 424\u2013438 (1998)","DOI":"10.1007\/BFb0054187"},{"key":"213_CR17","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"T.A. Henzinger","year":"1997","unstructured":"Henzinger T.A., Ho P.-H., Wong-Toi H.: HyTech: a model checker for hybrid systems. STTT 1, 110\u2013122 (1997)","journal-title":"STTT"},{"issue":"7","key":"213_CR18","doi-asserted-by":"crossref","first-page":"326","DOI":"10.1112\/plms\/s3-2.1.326","volume":"2","author":"G. Higman","year":"1952","unstructured":"Higman G.: Ordering by divisibility in abstract algebras. Lond. Math. Soc. (3) 2(7), 326\u2013336 (1952)","journal-title":"Lond. Math. Soc. (3)"},{"key":"213_CR19","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1016\/S0304-3975(00)00103-1","volume":"256","author":"Y. Kesten","year":"2001","unstructured":"Kesten Y., Maler O., Marcus M., Pnueli A., Shahar E.: Symbolic model checking with rich assertional languages. TCS 256, 93\u2013112 (2001)","journal-title":"TCS"},{"issue":"8","key":"213_CR20","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/361082.361093","volume":"17","author":"L. Lamport","year":"1974","unstructured":"Lamport L.: A new solution of Dijkstra\u2019s concurrent programming problem. Commun. ACM 17(8), 453\u2013455 (1974)","journal-title":"Commun. ACM"},{"key":"213_CR21","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: An exercise in the verification of multi-process programs. In: Beauty is Our Business, pp. 289\u2013301 (1990)","DOI":"10.1007\/978-1-4612-4476-9_34"},{"key":"213_CR22","unstructured":"Nilsson, M.: Regular model checking. PhD thesis, Uppsala University (2005)"},{"key":"213_CR23","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Ruah, S., Zuck, L.: Automatic deductive verification with invisible invariants. In: TACAS, pp. 82\u201397 (2001)","DOI":"10.1007\/3-540-45319-9_7"},{"key":"213_CR24","unstructured":"Talupur, M.: Abstraction techniques for parameterized verification. PhD thesis, CMU (2006)"},{"key":"213_CR25","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. LICS 332\u2013344 (1986)"},{"issue":"1","key":"213_CR26","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/s10009-002-0091-4","volume":"5","author":"T. Yavuz-Kahveci","year":"2003","unstructured":"Yavuz-Kahveci T., Bultan T.: A symbolic manipulator for automated verification of reactive systems with heterogeneous data types. STTT 5(1), 15\u201333 (2003)","journal-title":"STTT"},{"key":"213_CR27","doi-asserted-by":"crossref","unstructured":"Yavuz-Kahveci, T., Bultan, T.: Verification of parameterized hierarchical state machines using action language verifier. In: MEMOCODE, pp. 79\u201388 (2005)","DOI":"10.1007\/11513988_40"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0213-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-011-0213-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0213-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,9]],"date-time":"2025-03-09T09:41:54Z","timestamp":1741513314000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-011-0213-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,8,27]]},"references-count":27,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,4]]}},"alternative-id":["213"],"URL":"https:\/\/doi.org\/10.1007\/s10009-011-0213-y","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2011,8,27]]}}}