{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:46:41Z","timestamp":1772164001770,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":24,"publisher":"ACM","license":[{"start":{"date-parts":[[2009,6,15]],"date-time":"2009-06-15T00:00:00Z","timestamp":1245024000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2009,6,15]]},"DOI":"10.1145\/1542476.1542500","type":"proceedings-article","created":{"date-parts":[[2009,6,16]],"date-time":"2009-06-16T09:34:36Z","timestamp":1245144876000},"page":"211-222","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":29,"title":["Analyzing recursive programs using a fixed-point calculus"],"prefix":"10.1145","author":[{"given":"Salvatore","family":"La Torre","sequence":"first","affiliation":[{"name":"Universit\u00e0 degli Studi di Salerno, Salerno, Italy"}]},{"given":"Madhusudan","family":"Parthasarathy","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, IL, USA"}]},{"given":"Gennaro","family":"Parlato","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, IL, USA"}]}],"member":"320","published-online":{"date-parts":[[2009,6,15]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1075382.1075387"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"crossref","unstructured":"R.\n      Alur M.\n      McDougall and \n      Z.\n      Yang\n  . \n  Exploiting behavioral hierarchy for efficient model checking\n  . In E. Brinksma and K. G. Larsen editors CAV volume \n  2404\n   of \n  Lecture Notes in Computer Science pages \n  338\n  --\n  342\n  . \n  Springer 2002\n  .   R. Alur M. McDougall and Z. Yang. Exploiting behavioral hierarchy for efficient model checking. In E. Brinksma and K. G. Larsen editors CAV volume 2404 of Lecture Notes in Computer Science pages 338--342. Springer 2002.","DOI":"10.1007\/3-540-45657-0_25"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"crossref","unstructured":"T.\n      Ball B.\n      Cook V.\n      Levin and \n      S. K.\n      Rajamani\n  . \n  SLAM and Static Driver Verifier: Technology transfer of formal methods inside Microsoft\n  . In E. A. Boiten J. Derrick and G. Smith editors IFM volume \n  2999\n   of \n  Lecture Notes in Computer Science pages \n  1\n  --\n  20\n  . \n  Springer 2004\n  .  T. Ball B. Cook V. Levin and S. K. Rajamani. SLAM and Static Driver Verifier: Technology transfer of formal methods inside Microsoft. In E. A. Boiten J. Derrick and G. Smith editors IFM volume 2999 of Lecture Notes in Computer Science pages 1--20. Springer 2004.","DOI":"10.1007\/978-3-540-24756-2_1"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"T.\n      Ball\n     and \n      S. K.\n      Rajamani\n  . \n  Bebop: A symbolic model checker for Boolean programs\n  . In K. Havelund J. Penix and W. Visser editors SPIN volume \n  1885\n   of \n  Lecture Notes in Computer Science pages \n  113\n  --\n  130\n  . \n  Springer 2000\n  .   T. Ball and S. K. Rajamani. Bebop: A symbolic model checker for Boolean programs. In K. Havelund J. Penix and W. Visser editors SPIN volume 1885 of Lecture Notes in Computer Science pages 113--130. Springer 2000.","DOI":"10.1007\/10722468_7"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503274"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0044-z"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","unstructured":"A.\n      Biere\n    .\n  Mucke -- efficient mu-calculus model checking\n  . In O. Grumberg editor CAV volume \n  1254\n   of \n  Lecture Notes in Computer Science pages \n  468\n  --\n  471\n  . \n  Springer 1997\n  .   A. Biere. Mucke -- efficient mu-calculus model checking. In O. Grumberg editor CAV volume 1254 of Lecture Notes in Computer Science pages 468--471. Springer 1997.","DOI":"10.1007\/3-540-63166-6_50"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01969548"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328460"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_37"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"crossref","unstructured":"J.\n      Esparza\n     and \n      S.\n      Schwoon\n  . \n  A BDD-based model checker for recursive programs\n  . In G. Berry H. Comon and A. Finkel editors CAV volume \n  2102\n   of \n  Lecture Notes in Computer Science pages \n  324\n  --\n  336\n  . \n  Springer 2001\n  .   J. Esparza and S. Schwoon. A BDD-based model checker for recursive programs. In G. Berry H. Comon and A. Finkel editors CAV volume 2102 of Lecture Notes in Computer Science pages 324--336. Springer 2001.","DOI":"10.1007\/3-540-44585-4_30"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_7"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065167.1065169"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996861"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250785"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/996841"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/996893.996845"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","unstructured":"T.W.\n      Reps S.\n      Schwoon and \n      S.\n      Jha\n  . \n  Weighted pushdown systems and their application to interprocedural dataflow analysis\n  . In R. Cousot editor SAS volume \n  2694\n   of \n  Lecture Notes in Computer Science pages \n  189\n  --\n  213\n  . \n  Springer 2003\n  .   T.W. Reps S. Schwoon and S. Jha. Weighted pushdown systems and their application to interprocedural dataflow analysis. In R. Cousot editor SAS volume 2694 of Lecture Notes in Computer Science pages 189--213. Springer 2003.","DOI":"10.1007\/3-540-44898-5_11"},{"key":"e_1_3_2_1_22_1","volume-title":"Program Flow Analysis: Theory and Applications","author":"Sharir M.","year":"1981","unstructured":"M. Sharir and A. Pnueli . Two approaches to inter-procedural data-flow analysis . In Program Flow Analysis: Theory and Applications , 1981 . M. Sharir and A. Pnueli. Two approaches to inter-procedural data-flow analysis. In Program Flow Analysis: Theory and Applications, 1981."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85114-1_19"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2894"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/996893.996859"}],"event":{"name":"PLDI '09: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Dublin Ireland","acronym":"PLDI '09","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"]},"container-title":["Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1542476.1542500","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1542476.1542500","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:29:49Z","timestamp":1750238989000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1542476.1542500"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,6,15]]},"references-count":24,"alternative-id":["10.1145\/1542476.1542500","10.1145\/1542476"],"URL":"https:\/\/doi.org\/10.1145\/1542476.1542500","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1543135.1542500","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2009,6,15]]},"assertion":[{"value":"2009-06-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}