{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,24]],"date-time":"2025-05-24T07:26:58Z","timestamp":1748071618391},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540008989"},{"type":"electronic","value":"9783540365778"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36577-x_37","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:12:04Z","timestamp":1269897124000},"page":"505-520","source":"Crossref","is-referenced-by-count":16,"title":["Checking Properties of Heap-Manipulating Procedures with a Constraint Solver"],"prefix":"10.1007","author":[{"given":"Mandana","family":"Vaziri","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Jackson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"unstructured":"A. Andoni, D. Daniliuc, S. Khurshid, and D. Marinov. \u201cEvaluating the Small Scope Hypothesis\u201d, MIT Laboratory for Computer Science, September 2002. Unpublished manuscript.","key":"37_CR1"},{"doi-asserted-by":"crossref","unstructured":"T. Ball, S. K. Rajamani. \u201cThe SLAM Project: Debugging System Software via Static Analysis\u201d, Proc. POPL 2002, January 2002.","key":"37_CR2","DOI":"10.1145\/503272.503274"},{"doi-asserted-by":"crossref","unstructured":"D. R. Chase, M. Wegman and F. Zadeck. \u201cAnalysis of Pointers and Structures\u201d, Proc. Conf. on Programming Language Design and Implementation, 1990.","key":"37_CR3","DOI":"10.1145\/93542.93585"},{"doi-asserted-by":"crossref","unstructured":"J. C. Corbett, M. B. Dwyer, J. Hatcli., S. Laubach, C. S. Pasareanu, Robby, H. Zheng. \u201cBandera: Extracting Finite-State Models from Java Source Code\u201d, Proc. International Conference on Software Engineering, June 2000.","key":"37_CR4","DOI":"10.1145\/337180.337234"},{"unstructured":"T. H. Cormen, C. E. Leiserson, R. L. Rivest. \u201cIntroduction to Algorithms\u201d, MIT Press, 1990.","key":"37_CR5"},{"unstructured":"D. Detlefs, K. R. Leino, G. Nelson, and J. Saxe. \u201cExtended Static Checking\u201d. Technical Report 159, Compaq Systems Research Center, 1998.","key":"37_CR6"},{"unstructured":"Cormac Flanagan. Personal communication.","key":"37_CR7"},{"unstructured":"E. Goldberg and Y. Novikov. \u201cBerkMin: A fast and robust SAT-solver\u201d, In Design, Automation, and Test in Europe, March 2002.","key":"37_CR8"},{"doi-asserted-by":"crossref","unstructured":"G.J. Holzmann. \u201cThe Model Checker Spin\u201d, IEEE Trans. on Software Engineering, Vol. 23, 5, May 1997.","key":"37_CR9","DOI":"10.1109\/32.588521"},{"doi-asserted-by":"crossref","unstructured":"G. J. Holzmann and M. H. Smith. \u201cAutomating Software Feature Verification\u201d, Bell Labs Technical Journal, Vol. 5, 2, April-June 2000.","key":"37_CR10","DOI":"10.1002\/bltj.2223"},{"doi-asserted-by":"crossref","unstructured":"Daniel Jackson. \u201cAutomating First-Order Relational Logic\u201d, Proc. ACM SIGSOFT Conf. Foundations of Software Engineering, San Diego, November 2000.","key":"37_CR11","DOI":"10.1145\/355045.355063"},{"doi-asserted-by":"crossref","unstructured":"D. Jackson, I. Shlyakhter and M. Sridharan. \u201cA Micromodularity Mechanism\u201d, Proc. ACM SIGSOFT Conf. Foundations of Software Engineering, 2001.","key":"37_CR12","DOI":"10.1145\/503209.503219"},{"doi-asserted-by":"crossref","unstructured":"D. Jackson and M. Vaziri. \u201cFinding Bugs with a Constraint Solver\u201d, Proc. International Conference on Software Testing and Analysis, August 2000.","key":"37_CR13","DOI":"10.1145\/347324.383378"},{"doi-asserted-by":"crossref","unstructured":"R. Manevich, G. Ramalingam, J. Field, D. Goyal, M. Sagiv. \u201cCompactly Representing First-Order Structures for Static Analysis\u201d, In Proc. SAS 2002, 2002.","key":"37_CR14","DOI":"10.1007\/3-540-45789-5_16"},{"key":"37_CR15","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D. A. Plaisted","year":"1986","unstructured":"D. A. Plaisted and S. Greenbaum. \u201cA Structure-Preserving Clause Form Translation\u201d, Journal of Symbolic Computation, 2:293\u2013304, 1986.","journal-title":"Journal of Symbolic Computation"},{"issue":"3","key":"37_CR16","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"M. Sagiv, T. Reps, and R. Wilhelm. \u201cParametric shape analysis via 3-valued logic\u201d, In ACM Transactions on Programming Languages and Systems, 24(3), 217\u2013298, 2002.","journal-title":"In ACM Transactions on Programming Languages and Systems"},{"doi-asserted-by":"crossref","unstructured":"W. Visser, K. Havelund, G. Brat and S. Park. \u201cModel Checking Programs\u201d, International Conference on Automated Software Engineering, September 2000.","key":"37_CR17","DOI":"10.1109\/ASE.2000.873645"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36577-X_37","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T18:46:31Z","timestamp":1558982791000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36577-X_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008989","9783540365778"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-36577-x_37","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}