{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,2,9]],"date-time":"2024-02-09T23:30:16Z","timestamp":1707521416022},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2012,1,4]],"date-time":"2012-01-04T00:00:00Z","timestamp":1325635200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2012,4]]},"DOI":"10.1007\/s10703-011-0136-y","type":"journal-article","created":{"date-parts":[[2012,1,3]],"date-time":"2012-01-03T12:30:55Z","timestamp":1325593855000},"page":"206-231","source":"Crossref","is-referenced-by-count":13,"title":["Bounded underapproximations"],"prefix":"10.1007","volume":"40","author":[{"given":"Pierre","family":"Ganty","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Benjamin","family":"Monmege","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,1,4]]},"reference":[{"key":"136_CR1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"474","DOI":"10.1007\/11562948_35","volume-title":"ATVA \u201905: proc 3rd int symp on automated technology for verification and analysis","author":"S Bardin","year":"2005","unstructured":"Bardin S, Finkel A, Leroux J, Schnoebelen P (2005) Flat acceleration in symbolic model checking. In: ATVA \u201905: proc 3rd int symp on automated technology for verification and analysis. LNCS, vol\u00a03707. Springer, Berlin, pp 474\u2013488"},{"key":"136_CR2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"316","DOI":"10.1007\/3-540-10843-2_26","volume-title":"ICALP \u201981: proc of 8th int colloquium on automata, languages and programming","author":"M Blattner","year":"1981","unstructured":"Blattner M, Latteux M (1981) Parikh-bounded languages. In: ICALP \u201981: proc of 8th int colloquium on automata, languages and programming. LNCS, vol 115. Springer, Berlin, pp 316\u2013323"},{"key":"136_CR3","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1145\/604131.604137","volume-title":"POPL \u201903: proc 30th ACM SIGPLAN-SIGACT symp on principles of programming languages","author":"A Bouajjani","year":"2003","unstructured":"Bouajjani A, Esparza J, Touili T (2003) A generic approach to the static analysis of concurrent programs with procedures. In: POPL \u201903: proc 30th ACM SIGPLAN-SIGACT symp on principles of programming languages. ACM Press, New York, pp 62\u201373"},{"key":"136_CR4","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-642-00768-2_29","volume-title":"TACAS \u201909: proc 15th int conf on tools and algorithms for the construction and analysis of systems","author":"M Bozga","year":"2009","unstructured":"Bozga M, G\u00eerlea C, Iosif R (2009) Iterating octagons. In: TACAS \u201909: proc 15th int conf on tools and algorithms for the construction and analysis of systems. LNCS, vol 5505. Springer, Berlin, pp 337\u2013351"},{"key":"136_CR5","series-title":"LNCS","first-page":"517","volume-title":"CAV \u201906: proc 18th int conf on computer aided verification","author":"M Bozga","year":"2006","unstructured":"Bozga M, Iosif R, Moro P, Vojnar T, Bouajjani A, Habermehl P (2006) Programs with lists are counter automata. In: CAV \u201906: proc 18th int conf on computer aided verification. LNCS, vol 4144. Springer, Berlin, pp 517\u2013531"},{"key":"136_CR6","first-page":"499","volume-title":"POPL \u201911: proc 38th ACM SIGACT-SIGPLAN symp on principles of programming languages","author":"J Esparza","year":"2011","unstructured":"Esparza J, Ganty P (2011) Complexity of pattern-based verification for multithreaded programs. In: POPL \u201911: proc 38th ACM SIGACT-SIGPLAN symp on principles of programming languages. ACM Press, New York, pp 499\u2013510"},{"key":"136_CR7","unstructured":"Esparza J, Ganty P, Kiefer S, Luttenberger M (2010) Parikh\u2019s theorem: A simple and direct automaton construction. CoRR, abs\/1006.3825"},{"key":"136_CR8","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1007\/978-3-540-70583-3_2","volume-title":"ICALP \u201908: proc 35th int coll on automata, languages and programming","author":"J Esparza","year":"2008","unstructured":"Esparza J, Kiefer S, Luttenberger M (2008) Newton\u2019s method for \u03c9-continuous semirings. In: ICALP \u201908: proc 35th int coll on automata, languages and programming. LNCS, vol 5126. Springer, Berlin, pp 14\u201326. Invited paper"},{"issue":"6","key":"136_CR9","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1145\/1857914.1857917","volume":"57","author":"J Esparza","year":"2010","unstructured":"Esparza J, Kiefer S, Luttenberger M (2010) Newtonian program analysis. J ACM 57(6):331\u20133347","journal-title":"J ACM"},{"key":"136_CR10","series-title":"LNCS","first-page":"145","volume-title":"FSTTCS \u201902: proc 22nd int conf on foundations of software technology and theoretical computer science","author":"A Finkel","year":"2002","unstructured":"Finkel A, Leroux J (2002) How to compose Presburger-accelerations: applications to broadcast protocols. In: FSTTCS \u201902: proc 22nd int conf on foundations of software technology and theoretical computer science. LNCS, vol 2556. Springer, Berlin, pp 145\u2013156"},{"key":"136_CR11","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"600","DOI":"10.1007\/978-3-642-14295-6_52","volume-title":"CAV \u201910: proc 20th int conf on computer aided verification","author":"P Ganty","year":"2010","unstructured":"Ganty P, Majumdar R, Monmege B (2010) Bounded underapproximations. In: CAV \u201910: proc 20th int conf on computer aided verification. LNCS, vol 6174. Springer, Berlin, pp 600\u2013614. See also CoRR report abs\/0809.1236"},{"key":"136_CR12","volume-title":"The mathematical theory of context-free languages","author":"S Ginsburg","year":"1966","unstructured":"Ginsburg S (1966) The mathematical theory of context-free languages. McGraw-Hill, New York"},{"issue":"2","key":"136_CR13","first-page":"333","volume":"113","author":"S Ginsburg","year":"1964","unstructured":"Ginsburg S, Spanier EH (1964) Bounded ALGOL-like languages. Trans Am Math Soc 113(2):333\u2013368","journal-title":"Trans Am Math Soc"},{"key":"136_CR14","series-title":"LNCS","volume-title":"CAV \u201911: proc 21th int conf on computer aided verification","author":"M Hague","year":"2011","unstructured":"Hague M, Lin AW (2011) Model checking recursive programs with numeric data types. In: CAV \u201911: proc 21th int conf on computer aided verification. LNCS. Springer, Berlin"},{"key":"136_CR15","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1006\/jcss.2002.1836","volume":"65","author":"T Harju","year":"2002","unstructured":"Harju T, Ibarra OH, Karhum\u00e4ki J, Salomaa A (2002) Some decision problems concerning semilinearity and commutation. J Comput Syst Sci 65:278\u2013294","journal-title":"J Comput Syst Sci"},{"key":"136_CR16","volume-title":"Introduction to automata theory, languages and computation","author":"JE Hopcroft","year":"1979","unstructured":"Hopcroft JE, Ullman JD (1979) Introduction to automata theory, languages and computation, 1st edn. Addison-Wesley, Reading","edition":"1"},{"key":"136_CR17","unstructured":"Kahlon V Tractable dataflow analysis for concurrent programs via bounded languages. Patent WO\/2009\/094439, July 2009"},{"key":"136_CR18","first-page":"255","volume-title":"FCT \u201979: fundamentals of computation theory, Proc of the conf on algebraic, arithmetic, and categorial methods in computation theory","author":"M Latteux","year":"1979","unstructured":"Latteux M, Leguy J (1979) Une propri\u00e9t\u00e9 de la famille GRE. In: FCT \u201979: fundamentals of computation theory, Proc of the conf on algebraic, arithmetic, and categorial methods in computation theory. Akademie-Verlag, Berlin, pp 255\u2013261"},{"key":"136_CR19","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"402","DOI":"10.1007\/978-3-540-28644-8_26","volume-title":"CONCUR \u201904: proc 15th int conf on concurrency theory","author":"J Leroux","year":"2004","unstructured":"Leroux J, Sutre G (2004) On flatness for 2-dimensional vector addition systems with states. In: CONCUR \u201904: proc 15th int conf on concurrency theory. LNCS, vol 3170. Springer, Berlin, pp 402\u2013416"},{"key":"136_CR20","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/978-3-540-31980-1_7","volume-title":"TACAS \u201905: proc 11th int conf on tools and algorithms for the construction and analysis of systems","author":"S Qadeer","year":"2005","unstructured":"Qadeer S, Rehof J (2005) Context-bounded model checking of concurrent software. In: TACAS \u201905: proc 11th int conf on tools and algorithms for the construction and analysis of systems. LNCS, vol 3440. Springer, Berlin, pp 93\u2013107"},{"issue":"2","key":"136_CR21","doi-asserted-by":"crossref","first-page":"416","DOI":"10.1145\/349214.349241","volume":"22","author":"G Ramalingam","year":"2000","unstructured":"Ramalingam G (2000) Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans Program Lang Syst 22(2):416\u2013430","journal-title":"ACM Trans Program Lang Syst"},{"key":"136_CR22","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"270","DOI":"10.1007\/978-3-540-85114-1_19","volume-title":"SPIN\u201908: proc of 15th int model checking software workshop","author":"D Suwimonteerabuth","year":"2008","unstructured":"Suwimonteerabuth D, Esparza J, Schwoon S (2008) Symbolic context-bounded analysis of multithreaded Java programs. In: SPIN\u201908: proc of 15th int model checking software workshop. LNCS, vol 5156. Springer, Berlin, pp 270\u2013287"},{"key":"136_CR23","unstructured":"To AW (2010) Model checking infinite-state systems: generic and specific approaches. PhD thesis, School of Informatics, University of Edinburgh"},{"key":"136_CR24","unstructured":"van Begin L (2003) Efficient verification of counting abstractions for parametric systems. PhD thesis, Universit\u00e9 Libre de Bruxelles, Belgium"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-011-0136-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-011-0136-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-011-0136-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T22:05:52Z","timestamp":1559253952000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-011-0136-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,1,4]]},"references-count":24,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,4]]}},"alternative-id":["136"],"URL":"https:\/\/doi.org\/10.1007\/s10703-011-0136-y","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,1,4]]}}}