{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T04:17:40Z","timestamp":1759033060761},"reference-count":21,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2002,9,1]],"date-time":"2002-09-01T00:00:00Z","timestamp":1030838400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3984,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2002,9]]},"DOI":"10.1016\/s1571-0661(04)80351-7","type":"journal-article","created":{"date-parts":[[2004,9,28]],"date-time":"2004-09-28T19:29:25Z","timestamp":1096399765000},"page":"195-219","source":"Crossref","is-referenced-by-count":1,"special_numbering":"C","title":["Model Checking Erlang Programs \u2013 Abstracting Recursive Function Calls"],"prefix":"10.1016","volume":"64","author":[{"given":"Frank","family":"Huch","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)80351-7_NEWBIB1","series-title":"Concurrent Programming in Erlang","author":"Armstrong","year":"1993"},{"key":"10.1016\/S1571-0661(04)80351-7_NEWBIB2","unstructured":"Thomas Arts and Clara Benac Earle. Development of a verified Erlang program for resource locking. In Formal Methods in Industrial Critical Systems, Paris, France, July 2001."},{"key":"10.1016\/S1571-0661(04)80351-7_NEWBIB3","first-page":"138","article-title":"More infinite results","volume":"62","author":"Burkart","year":"1997","journal-title":"Bulletin of the European Association for Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80351-7_NEWBIB4","doi-asserted-by":"crossref","unstructured":"Olaf Burkart and Bernhard Steffen. Model checking for context-free processes. In W. R. Cleaveland, editor, CONCUR'92: Third International Conference on Concurrency Theory, volume 630 of Lecture Notes in Computer Science, pages 123\u2013137, Stony Brook, New York, 24\u201327 August 1992. Springer.","DOI":"10.1007\/BFb0084787"},{"key":"10.1016\/S1571-0661(04)80351-7_NEWBIB5","series-title":"Model Checking","author":"Clarke","year":"1999"},{"key":"10.1016\/S1571-0661(04)80351-7_NEWBIB6","doi-asserted-by":"crossref","unstructured":"Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In Proceedings of the 4th ACM Symposium on Principles of Programming Languages, Los Angeles, pages 238\u2013252, New York, NY, 1977. ACM.","DOI":"10.1145\/512950.512973"},{"key":"10.1016\/S1571-0661(04)80351-7_NEWBIB7","doi-asserted-by":"crossref","unstructured":"Matthew B. Dwyer and Corina S. Pasareanu. Filter-based model checking of partial systems. In Proceedings of the ACM SIGSOFT Sixth International Symposium on the Foundation of Software Engineering, November 1998.","DOI":"10.1145\/288195.288307"},{"issue":"3","key":"10.1016\/S1571-0661(04)80351-7_NEWBIB8","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1016\/0304-3975(87)90109-5","article-title":"A syntactic theory of sequential control","volume":"52","author":"Felleisen","year":"1987","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"10.1016\/S1571-0661(04)80351-7_NEWBIB9","doi-asserted-by":"crossref","DOI":"10.1007\/s100090050043","article-title":"Model checking Java programs using Java PathFinder","volume":"2","author":"Havelund","year":"1998","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"10.1016\/S1571-0661(04)80351-7_NEWBIB10","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1007\/3-540-60218-6_34","article-title":"Proving properties of concurrent systems with SPIN","volume":"962","author":"Gerard Holzmann","year":"1995","journal-title":"Lecture Notes in Computer Sience"},{"key":"10.1016\/S1571-0661(04)80351-7_NEWBIB11","doi-asserted-by":"crossref","unstructured":"Frank Huch. Verification of Erlang programs using abstract interpretation and model checking. ACM SIGPLAN Notices, 34(9):261\u2013272, September 1999. Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP '99).","DOI":"10.1145\/317636.317908"},{"key":"10.1016\/S1571-0661(04)80351-7_NEWBIB12","doi-asserted-by":"crossref","unstructured":"Frank Huch. Verification of Erlang programs using abstract interpretation and model checking \u2013- extended version. Technical Report 99\u201302, RWTH Aachen, 1999.","DOI":"10.1145\/317636.317908"},{"key":"10.1016\/S1571-0661(04)80351-7_NEWBIB13","article-title":"Model checking Erlang programs - abstracting the context-free structure","volume":"55","author":"Huch","year":"2001"},{"key":"10.1016\/S1571-0661(04)80351-7_NEWBIB14","series-title":"Handbook of Logic in Computer Science","first-page":"527","article-title":"Abstract interpretation: a semanticsbased tool for program analysis","author":"Neil Jones","year":"1994"},{"key":"10.1016\/S1571-0661(04)80351-7_NEWBIB15","doi-asserted-by":"crossref","unstructured":"Orna Lichtenstein and Amir Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, pages 97\u2013107, New Orleans, Louisiana, January 13\u201316, 1985. ACM SIGACT-SIGPLAN, ACM Press.","DOI":"10.1145\/318593.318622"},{"key":"10.1016\/S1571-0661(04)80351-7_NEWBIB16","series-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Manna","year":"1992"},{"key":"10.1016\/S1571-0661(04)80351-7_NEWBIB17","series-title":"Temporal Verification of Reactive Systems (Safety)","author":"Manna","year":"1995"},{"key":"10.1016\/S1571-0661(04)80351-7_NEWBIB18","doi-asserted-by":"crossref","unstructured":"Thomas Noll, Lars-\u00e5ke Fredlund, and Dilian Gurov. The Erlang verification tool. In Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'01), volume 2031 of Lecture Notes in Computer Science, pages 582\u2013585. Springer, 2001.","DOI":"10.1007\/3-540-45319-9_41"},{"key":"10.1016\/S1571-0661(04)80351-7_NEWBIB19","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1007\/3-540-49727-7_22","article-title":"Program analysis as model checking of abstract interpretations","volume":"1503","author":"Schmidt","year":"1998","journal-title":"Lecture Notes in Computer Sience"},{"key":"10.1016\/S1571-0661(04)80351-7_NEWBIB20","series-title":"Program Flow Analysis: Theory and Applications","first-page":"189","article-title":"Two approaches to interprocedural data flow analysis","author":"Sharir","year":"1981"},{"key":"10.1016\/S1571-0661(04)80351-7_NEWBIB21","doi-asserted-by":"crossref","unstructured":"Moshe Y. Vardi. An Automata-Theoretic Approach to Linear Temporal Logic, volume 1043 of Lecture Notes in Computer Science, pages 238\u2013266. Springer, New York, NY, USA, 1996.","DOI":"10.1007\/3-540-60915-6_6"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104803517?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104803517?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,2,3]],"date-time":"2019-02-03T12:22:49Z","timestamp":1549196569000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104803517"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,9]]},"references-count":21,"alternative-id":["S1571066104803517"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80351-7","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2002,9]]}}}