{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,31]],"date-time":"2025-01-31T12:40:27Z","timestamp":1738327227246,"version":"3.35.0"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540691471"},{"type":"electronic","value":"9783540691495"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"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":[[2008]]},"DOI":"10.1007\/978-3-540-69149-5_23","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"214-226","source":"Crossref","is-referenced-by-count":0,"title":["Implications of a Data Structure Consistency Checking System"],"prefix":"10.1007","author":[{"given":"Viktor","family":"Kuncak","sequence":"first","affiliation":[]},{"given":"Patrick","family":"Lam","sequence":"additional","affiliation":[]},{"given":"Karen","family":"Zee","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Rinard","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Proc. ACM PLDI (2001)","DOI":"10.1145\/378795.378846"},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: CASSIS: Int. Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart devices (2004)","DOI":"10.1007\/978-3-540-30569-9_3"},{"issue":"6","key":"23_CR3","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1109\/71.180621","volume":"3","author":"W. Blume","year":"1992","unstructured":"Blume, W., Eigenmann, R.: Performance analysis of parallelizing compilers on the Perfect Benchmarks programs. IEEE Transactions on Parallel and Distributed Systems\u00a03(6), 643\u2013656 (1992)","journal-title":"IEEE Transactions on Parallel and Distributed Systems"},{"key":"23_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59207-2","volume-title":"The Classical Decision Problem","author":"E. B\u00f6rger","year":"1997","unstructured":"B\u00f6rger, E., Gr\u00e4del, E., Gurevich, Y.: The Classical Decision Problem. Springer, Heidelberg (1997)"},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"Chase, D.R., Wegman, M., Zadeck, F.K.: Analysis of pointers and structures. In: Proc. ACM PLDI (1990)","DOI":"10.1145\/93542.93585"},{"key":"23_CR6","doi-asserted-by":"crossref","unstructured":"Das, M., Lerner, S., Seigle, M.: ESP: Path-sensitive program verification in polynomial time. In: Proc. ACM PLDI (2002)","DOI":"10.1145\/512529.512538"},{"key":"23_CR7","volume-title":"Systematic Software Development using VDM","author":"C.B. Jones","year":"1986","unstructured":"Jones, C.B.: Systematic Software Development using VDM. Prentice Hall International, UK (1986)"},{"key":"23_CR8","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Lam, P., Rinard, M.: Role analysis. In: Annual ACM Symp. on Principles of Programming Languages (POPL) (2002)","DOI":"10.1145\/503272.503276"},{"key":"23_CR9","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Rinard, M.: Decision procedures for set-valued fields. In: 1st International Workshop on Abstract Interpretation of Object-Oriented Languages (AIOOL 2005) (2005)","DOI":"10.1016\/j.entcs.2005.01.022"},{"key":"23_CR10","unstructured":"Lam, P., Kuncak, V., Rinard, M.: On our experience with modular pluggable analyses. Technical Report 965, MIT CSAIL (September, 2004)"},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"Lam, P., Kuncak, V., Rinard, M.: Cross-cutting techniques in program specification and analysis. In: 4th International Conference on Aspect-Oriented Software Development (AOSD 2005) (2005)","DOI":"10.1145\/1052898.1052913"},{"key":"23_CR12","doi-asserted-by":"crossref","unstructured":"Lam, P., Kuncak, V., Rinard, M.: Generalized typestate checking for data structure consistency. In: 6th International Conference on Verification, Model Checking and Abstract Interpretation (2005)","DOI":"10.1007\/978-3-540-30579-8_28"},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"Lam, P., Kuncak, V., Rinard, M.: Hob: A tool for verifying data structure consistency. In: 14th International Conference on Compiler Construction (tool demo) (April, 2005)","DOI":"10.1007\/978-3-540-31985-6_16"},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"Lev-Ami, T., Reps, T., Sagiv, M., Wilhelm, R.: Putting static analysis to work for verification: A case study. In: International Symposium on Software Testing and Analysis (2000)","DOI":"10.1145\/347324.348031"},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: Proc. 7th International Static Analysis Symposium (2000)","DOI":"10.1007\/978-3-540-45099-3_15"},{"key":"23_CR16","unstructured":"Marinov, D.: Credible compilation. Master\u2019s thesis, Massachusetts Institute of Technology (2000)"},{"key":"23_CR17","unstructured":"Marnette, B., Kuncak, V., Rinard, M.: On algorithms and complexity for sets with cardinality constraints. Technical report, MIT CSAIL (August, 2005)"},{"key":"23_CR18","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Science Logic","author":"P. O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, Springer, Heidelberg (2001)"},{"key":"23_CR19","doi-asserted-by":"crossref","unstructured":"Ramalingam, G., Warshavsky, A., Field, J., Goyal, D., Sagiv, M.: Deriving specialized program analyses for certifying component-client conformance. In: PLDI (2002)","DOI":"10.1145\/512529.512540"},{"key":"23_CR20","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: 17th LICS, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"23_CR21","unstructured":"Rinard, M., Marinov, D.: Credible compilation with pointers. In: Proceedings of the Workshop on Run-Time Result Verification (1999)"},{"key":"23_CR22","unstructured":"Rinetzky, N.: Interprocedural shape analysis. Master\u2019s thesis, Technion - Israel Institute of Technology (2000)"},{"issue":"1","key":"23_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/271510.271517","volume":"20","author":"M. Sagiv","year":"1998","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Solving shape-analysis problems in languages with destructive updating. ACM TOPLAS\u00a020(1), 1\u201350 (1998)","journal-title":"ACM TOPLAS"},{"key":"23_CR24","doi-asserted-by":"crossref","unstructured":"Steensgaard, B.: Points-to analysis in almost linear time. In: Proc. 23rd ACM POPL, Petersburg Beach, FL (January, 1996)","DOI":"10.1145\/237721.237727"},{"key":"23_CR25","doi-asserted-by":"crossref","unstructured":"S\u0103lcianu, A.D., Rinard, M.: Purity and side-effect analysis for java programs. In: Proc. 6th International Conference on Verification, Model Checking and Abstract Interpretation (to appear, January 2005)","DOI":"10.1007\/978-3-540-30579-8_14"},{"key":"23_CR26","doi-asserted-by":"crossref","unstructured":"Xie, Y., Aiken, A.: Scalable error detection using boolean satisfiability. In: POPL 2005 (2005)","DOI":"10.1145\/1040305.1040334"},{"key":"23_CR27","unstructured":"Yang, J., Twohey, P., Engler, D., Musuvathi, M.: Using model checking to find serious file system errors. In: OSDI 2004 (2004)"},{"key":"23_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1007\/978-3-540-24730-2_39","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Yorsh","year":"2004","unstructured":"Yorsh, G., Reps, T., Sagiv, M.: Symbolically computing most-precise abstract operations for shape analysis. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 530\u2013545. Springer, Heidelberg (2004)"},{"key":"23_CR29","doi-asserted-by":"crossref","unstructured":"Yorsh, G., Skidanov, A., Reps, T., Sagiv, M.: Automatic assume\/guarantee reasoning for heap-manupilating programs. In: 1st AIOOL Workshop (2005)","DOI":"10.1016\/j.entcs.2005.01.028"},{"key":"23_CR30","unstructured":"Zee, K., Lam, P., Kuncak, V., Rinard, M.: Combining theorem proving with static analysis for data structure consistency. In: International Workshop on Software Verification and Validation (SVV 2004), Seattle (November, 2004)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69149-5_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,31]],"date-time":"2025-01-31T11:58:16Z","timestamp":1738324696000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69149-5_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540691471","9783540691495"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69149-5_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}