{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:34:01Z","timestamp":1775054041173,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642165573","type":"print"},{"value":"9783642165580","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-16558-0_44","type":"book-chapter","created":{"date-parts":[[2010,11,2]],"date-time":"2010-11-02T13:36:49Z","timestamp":1288705009000},"page":"535-548","source":"Crossref","is-referenced-by-count":41,"title":["A Memory Model for Static Analysis of C Programs"],"prefix":"10.1007","author":[{"given":"Zhongxing","family":"Xu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ted","family":"Kremenek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jian","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"44_CR1","doi-asserted-by":"crossref","unstructured":"Cadar, C., Twohey, P., Ganesh, V., Engler, D.: EXE: A system for automatically generating inputs of death using symbolic execution. Technical report, Computer System Laboratory, Stanford University (2006)","DOI":"10.1145\/1180405.1180445"},{"key":"44_CR2","unstructured":"Clang static analyzer, \n                    \n                      http:\/\/clang-analyzer.llvm.org\/"},{"key":"44_CR3","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: Directed automated random testing. In: Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, pp. 213\u2013223 (2005)","DOI":"10.1145\/1065010.1065036"},{"key":"44_CR4","doi-asserted-by":"crossref","unstructured":"Hampapuram, H., Yang, Y., Das, M.: Symbolic path simulation in path-sensitive dataflow analysis. In: Proceedings of the 6th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, pp. 52\u201358 (2005)","DOI":"10.1145\/1108792.1108808"},{"key":"44_CR5","unstructured":"WG14 ISO\/IEC\u00a09899:201x, editor. Programming Languages - C. ISO (1999), \n                    \n                      http:\/\/www.open-std.org\/jtc1\/sc22\/wg14\/www\/docs\/n1336.pdf"},{"key":"44_CR6","unstructured":"Kremenek, T.: Finding bugs with the clang static analyzer, \n                    \n                      http:\/\/llvm.org\/devmtg\/2008-08\/Kremenek_StaticAnalyzer.pdf"},{"key":"44_CR7","unstructured":"The LLVM compiler infrastructure, \n                    \n                      http:\/\/llvm.org\/"},{"key":"44_CR8","volume-title":"Semantics with applications: a formal introduction","author":"H.R. Nielson","year":"1992","unstructured":"Nielson, H.R., Nielson, F.: Semantics with applications: a formal introduction. John Wiley & Sons Inc., Chichester (1992)"},{"key":"44_CR9","doi-asserted-by":"crossref","unstructured":"Xie, Y., Aiken, A.: Saturn: A scalable framework for error detection using Boolean satisfiability. ACM Transactions on Programming Languages and Systems\u00a029(3) (2007)","DOI":"10.1145\/1232420.1232423"},{"key":"44_CR10","doi-asserted-by":"crossref","unstructured":"Xu, Z., Zhang, J.: A test data generation tool for unit testing of C programs. In: Proceedings of the International Conference on Quality Software, pp. 107\u2013116 (2006)","DOI":"10.1109\/QSIC.2006.7"},{"key":"44_CR11","unstructured":"Zhang, J.: Symbolic execution of program paths involving pointers and structure variables. In: Proceedings of the Fourth International Conference on Quality Software, pp. 87\u201392 (2004)"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification, and Validation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16558-0_44","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,22]],"date-time":"2019-03-22T02:23:12Z","timestamp":1553221392000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16558-0_44"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642165573","9783642165580"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16558-0_44","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}