{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:50:54Z","timestamp":1725490254987},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540424963"},{"type":"electronic","value":"9783540446835"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44683-4_18","type":"book-chapter","created":{"date-parts":[[2007,8,29]],"date-time":"2007-08-29T01:32:38Z","timestamp":1188351158000},"page":"198-211","source":"Crossref","is-referenced-by-count":1,"title":["Automatic Verification of Recursive Procedures with One Integer Parameter"],"prefix":"10.1007","author":[{"given":"Ahmed","family":"Bouajjani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Habermehl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Richard","family":"Mayr","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,9,5]]},"reference":[{"key":"18_CR1","series-title":"Lect Notes Comput Sci","volume-title":"International Conference on Concurrency Theory (CONCUR\u201997)","author":"A. Bouajjani","year":"1997","unstructured":"A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: application to model checking. In International Conference on Concurrency Theory (CONCUR\u201997), volume 1243 of LNCS. Springer Verlag, 1997."},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, P. Habermehl, and R. Mayr. Automatic Verification of Recursive Procedures with one Integer Parameter. Technical Report LIAFA, 2001. available at http:\/\/www.informatik.uni-freiburg.de\/~mayrri\/index.html","DOI":"10.1007\/3-540-44683-4_18"},{"key":"18_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1007\/978-3-540-48654-1_9","volume-title":"CONCUR\u201994","author":"O. Burkart","year":"1994","unstructured":"O. Burkart and B. Steffen. Pushdown processes: Parallel composition and model checking. In CONCUR\u201994, volume 836 of LNCS, pages 98\u2013113. Springer Verlag, 1994."},{"key":"18_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-69678-4","volume-title":"Proceedings of ICALP\u201997","author":"O. Burkart","year":"1997","unstructured":"O. Burkart and B. Steffen. Model checking the full modal mu-calculus for infinite sequential processes. In Proceedings of ICALP\u201997, volume 1256 of LNCS. Springer Verlag, 1997."},{"key":"18_CR5","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of CAV 2000","author":"J. Esparza","year":"2000","unstructured":"J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. Efficient algorithms for model checking pushdown systems. In Proc. of CAV 2000, volume 1855 of LNCS. Springer, 2000."},{"key":"18_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1007\/3-540-49019-1_2","volume-title":"Proc. of FoSSaCS\u201999","author":"J. Esparza","year":"1999","unstructured":"J. Esparza and J. Knoop. An automata-theoretic approach to interprocedural data-flow analysis. In Proc. of FoSSaCS\u201999, volume 1578 of LNCS, pages 14\u201330. Springer Verlag, 1999."},{"key":"18_CR7","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1145\/322047.322058","volume":"25","author":"O. Ibarra","year":"1978","unstructured":"O. Ibarra. Reversal-bounded multicounter machines and their decision problems. Journal of the ACM, 25:116\u2013133, 1978.","journal-title":"Journal of the ACM"},{"key":"18_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44618-4_15","volume-title":"Proc. of CONCUR 2000","author":"O. Ibarra","year":"2000","unstructured":"O. Ibarra, T. Bultan, and J. Su. Reachability analysis for some models of infinite-state transition systems. In Proc. of CONCUR 2000, volume 1877 of LNCS. Springer, 2000."},{"key":"18_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/10719839_37","volume-title":"Proc. of LATIN 2000","author":"R. Mayr","year":"2000","unstructured":"R. Mayr. Undecidable problems in unreliable computations. In Proc. of LATIN 2000, volume 1776 of LNCS. Springer Verlag, 2000."},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"J. van Leeuwen, editor. Handbook of Theoretical Computer Science: Volume A, Algorithms and Complexity. Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88071-0.50015-1"},{"key":"18_CR11","series-title":"Lect Notes Comput Sci","volume-title":"International Conference on Computer Aided Verification (CAV\u201996)","author":"I. Walukiewicz","year":"1996","unstructured":"I. Walukiewicz. Pushdown processes: games and model checking. In International Conference on Computer Aided Verification (CAV\u201996), volume 1102 of LNCS. Springer, 1996."}],"container-title":["Lecture Notes in Computer Science","Mathematical Foundations of Computer Science 2001"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44683-4_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T17:27:39Z","timestamp":1556818059000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44683-4_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540424963","9783540446835"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-44683-4_18","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}