{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:42:03Z","timestamp":1750308123715,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":15,"publisher":"ACM","license":[{"start":{"date-parts":[[2006,1,9]],"date-time":"2006-01-09T00:00:00Z","timestamp":1136764800000},"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":[[2006,1,9]]},"DOI":"10.1145\/1111542.1111551","type":"proceedings-article","created":{"date-parts":[[2006,2,6]],"date-time":"2006-02-06T15:52:40Z","timestamp":1139241160000},"page":"48-57","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["A dead variable analysis for explicit model checking"],"prefix":"10.1145","author":[{"given":"Micah","family":"Lewis","sequence":"first","affiliation":[{"name":"Brigham Young U."}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Jones","sequence":"additional","affiliation":[{"name":"Brigham Young U."}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2006,1,9]]},"reference":[{"key":"e_1_3_2_1_1_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 Klaus Havelund John Penix and Willem Visser editors 7th International SPIN Workshop volume \n  1885\n   of \n  Lecture Notes in Computer Science pages \n  113\n  --\n  130\n  . \n  Springer August \n  2000\n  .]]   T. Ball and S. K. Rajamani. Bebop: A symbolic model checker for boolean programs. In Klaus Havelund John Penix and Willem Visser editors 7th International SPIN Workshop volume 1885 of Lecture Notes in Computer Science pages 113--130. Springer August 2000.]]","DOI":"10.1007\/10722468_7"},{"key":"e_1_3_2_1_2_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1007\/3-540-48294-6_11","volume-title":"Static Analysis, 6th International Symposium, SAS '99, Venice, Italy, September 22--24","author":"Bozga Marius","year":"1999","unstructured":"Marius Bozga , Jean-Claude Fernandez , and Lucian Ghirvu . State space reduction based on live variables analysis . In Agostino Cortesi and Gilberto Fil\u00e9, editors, Static Analysis, 6th International Symposium, SAS '99, Venice, Italy, September 22--24 , 1999 , Proceedings, volume 1694 of Lecture Notes in Computer Science , pages 164 -- 178 . Springer , 1999.]] Marius Bozga, Jean-Claude Fernandez, and Lucian Ghirvu. State space reduction based on live variables analysis. In Agostino Cortesi and Gilberto Fil\u00e9, editors, Static Analysis, 6th International Symposium, SAS '99, Venice, Italy, September 22--24, 1999, Proceedings, volume 1694 of Lecture Notes in Computer Science, pages 164--178. Springer, 1999.]]"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337234"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"crossref","unstructured":"Yifei Dong and C. R. Ramakrishnan. An optimizing compiler for efficient model checking. In FORTE XII \/ PSTV XIX '99: Proceedings of the IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XII) and Protocol Specification Testing and Verification (PSTV XIX) pages 241--256. Kluwer B. V. 1999.]]   Yifei Dong and C. R. Ramakrishnan. An optimizing compiler for efficient model checking. In FORTE XII \/ PSTV XIX '99: Proceedings of the IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XII) and Protocol Specification Testing and Verification (PSTV XIX) pages 241--256. Kluwer B. V. 1999.]]","DOI":"10.1007\/978-0-387-35578-8_14"},{"key":"e_1_3_2_1_7_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1007\/3-540-44829-2_17","volume-title":"Proceedings of the 10th International Workshop on Model Checking of Software (SPIN)","author":"Henzinger T. A.","year":"2003","unstructured":"T. A. Henzinger , R. Jhala , R. Majumdar , and G. Sutre . Software verification with Blast . In T. Ball and S. K. Rajamani, editors, Proceedings of the 10th International Workshop on Model Checking of Software (SPIN) , volume 2648 of Lecture Notes in Computer Science , pages 235 -- 239 , Portland , OR , May 2003 .]] T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Software verification with Blast. In T. Ball and S. K. Rajamani, editors, Proceedings of the 10th International Workshop on Model Checking of Software (SPIN), volume 2648 of Lecture Notes in Computer Science, pages 235--239, Portland, OR, May 2003.]]"},{"key":"e_1_3_2_1_8_1","volume-title":"Proceedings of the Third Spin Workshop","author":"Holzmann G. J.","year":"1997","unstructured":"G. J. Holzmann . State compression in Spin . In Proceedings of the Third Spin Workshop , Twente University, The Netherlands , April 1997 .]] G. J. Holzmann. State compression in Spin. In Proceedings of the Third Spin Workshop, Twente University, The Netherlands, April 1997.]]"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/645879.758300"},{"key":"e_1_3_2_1_10_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/978-3-540-24732-6_4","volume-title":"Proceedings of 11th International SPIN Workshop, Barcelona, Spain","author":"Leven Peter","year":"2004","unstructured":"Peter Leven , Tilman Mehler , and Stefan Edelkamp . Directed error detection in C++ with the assembley-level model checker StEAM . In Proceedings of 11th International SPIN Workshop, Barcelona, Spain , volume 2989 of Lecture Notes in Computer Science , pages 39 -- 56 . Springer , 2004 .]] Peter Leven, Tilman Mehler, and Stefan Edelkamp. Directed error detection in C++ with the assembley-level model checker StEAM. In Proceedings of 11th International SPIN Workshop, Barcelona, Spain, volume 2989 of Lecture Notes in Computer Science, pages 39--56. Springer, 2004.]]"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11537328_20"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/949952.940107"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1101908.1101982"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268950"},{"key":"e_1_3_2_1_16_1","volume-title":"Proceedings of the Workshop on Advances in Verification (WAVE'00)","author":"Visser W.","year":"2000","unstructured":"W. Visser , K. Havelund , G. Brat , and S. Park . Java PathFinder: Second generation of a Java model checker. In G. Gopalakrishnan, editor , Proceedings of the Workshop on Advances in Verification (WAVE'00) , July 2000 .]] W. Visser, K. Havelund, G. Brat, and S. Park. Java PathFinder: Second generation of a Java model checker. In G. Gopalakrishnan, editor, Proceedings of the Workshop on Advances in Verification (WAVE'00), July 2000.]]"}],"event":{"name":"PEPM06: Partial Evaluation and Program Manipulation 2006","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Charleston South Carolina","acronym":"PEPM06"},"container-title":["Proceedings of the 2006 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1111542.1111551","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1111542.1111551","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:08:23Z","timestamp":1750262903000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1111542.1111551"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,1,9]]},"references-count":15,"alternative-id":["10.1145\/1111542.1111551","10.1145\/1111542"],"URL":"https:\/\/doi.org\/10.1145\/1111542.1111551","relation":{},"subject":[],"published":{"date-parts":[[2006,1,9]]},"assertion":[{"value":"2006-01-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}