{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T21:51:30Z","timestamp":1725573090511},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540242970"},{"type":"electronic","value":"9783540305798"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-30579-8_28","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T16:45:34Z","timestamp":1292863534000},"page":"430-447","source":"Crossref","is-referenced-by-count":38,"title":["Generalized Typestate Checking for Data Structure Consistency"],"prefix":"10.1007","author":[{"given":"Patrick","family":"Lam","sequence":"first","affiliation":[]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Rinard","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"28_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":"28_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/3-540-46002-0_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2002","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Relative completeness of abstraction refinement for software model checking. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, p. 158. Springer, Heidelberg (2002)"},{"issue":"6","key":"28_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":"28_CR4","unstructured":"Clarke, L., Richardson, D.: Symbolic evaluation methods for program analysis. In: Program Flow Analysis: Theory and Applications, ch. 9. Prentice-Hall, Inc., Englewood Cliffs (1981)"},{"key":"28_CR5","first-page":"269","volume-title":"Proc. 6th POPL","author":"P. Cousot","year":"1979","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proc. 6th POPL, San Antonio, Texas, pp. 269\u2013282. ACM Press, New York (1979)"},{"key":"28_CR6","first-page":"84","volume-title":"Conference Record of the 5th POPL","author":"P. Cousot","year":"1978","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Conference Record of the 5th POPL, Tucson, Arizona, pp. 84\u201397. ACM Press, New York (1978)"},{"key":"28_CR7","doi-asserted-by":"crossref","unstructured":"DeLine, R., F\u00e4hndrich, M.: Enforcing high-level protocols in low-level software. In: Proc. ACM PLDI (2001)","DOI":"10.1145\/378795.378811"},{"key":"28_CR8","doi-asserted-by":"crossref","unstructured":"DeLine, R., F\u00e4hndrich, M.: Typestates for objects. In: Proc. 18th ECOOP (June 2004)","DOI":"10.1007\/978-3-540-24851-4_21"},{"key":"28_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/3-540-45337-7_8","volume-title":"ECOOP 2001 - Object-Oriented Programming","author":"S. Drossopoulou","year":"2001","unstructured":"Drossopoulou, S., Damiani, F., Dezani-Ciancaglini, M., Giannini, P.: Fickle: Dynamic object re-classification. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol.\u00a02072, pp. 130\u2013149. Springer, Heidelberg (2001)"},{"key":"28_CR10","doi-asserted-by":"crossref","unstructured":"Fahndrich, M., DeLine, R.: Adoption and focus: Practical linear types for imperative programming. In: Proc. ACM PLDI (2002)","DOI":"10.1145\/512529.512532"},{"key":"28_CR11","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1145\/949305.949332","volume-title":"Proceedings of the 18th ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications","author":"M. F\u00e4hndrich","year":"2003","unstructured":"F\u00e4hndrich, M., Leino, K.R.M.: Declaring and checking non-null types in an objectoriented language. In: Proceedings of the 18th ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications, pp. 302\u2013312. ACM Press, New York (2003)"},{"key":"28_CR12","unstructured":"F\u00e4hndrich, M., Leino, K.R.M.: Heap monotonic typestates. In: International Workshop on Aliasing, Confinement and Ownership in object-oriented programming, IWACO (2003)"},{"key":"28_CR13","doi-asserted-by":"crossref","unstructured":"Field, J., Goyal, D., Ramalingam, G., Yahav, E.: Typestate verification: Abstraction techniques and complexity results. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694. Springer, Heidelberg (2003)","DOI":"10.1007\/3-540-44898-5_25"},{"key":"28_CR14","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: Generating compact verification conditions. In: Proc. 28th ACM POPL (2001)","DOI":"10.1145\/360204.360220"},{"key":"28_CR15","series-title":"Elements of Reusable Object-Oriented Software","volume-title":"Design Patterns","author":"E. Gamma","year":"1994","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlisside, J.: Design Patterns. Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading (1994)"},{"key":"28_CR16","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: 31st POPL (2004)","DOI":"10.1145\/964001.964021"},{"key":"28_CR17","doi-asserted-by":"crossref","unstructured":"Jeannet, B., Loginov, A., Reps, T., Sagiv, M.: A relational approach to interprocedural shape analysis. In: 11th SAS (2004)","DOI":"10.1007\/978-3-540-27864-1_19"},{"key":"28_CR18","unstructured":"Klarlund, N., M\u00f8ller, A.: MONA Version 1.4 User Manual. BRICS Notes Series NS-01-1, Department of Computer Science, University of Aarhus (January 2001)"},{"key":"28_CR19","doi-asserted-by":"crossref","unstructured":"Klarlund, N., M\u00f8ller, A., Schwartzbach, M.I.: MONA implementation secrets. In: Proc. 5th International Conference on Implementation and Application of Automata. LNCS, vol.\u00a02000 (2001)","DOI":"10.1007\/3-540-44674-5_15"},{"key":"28_CR20","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1016\/0304-3975(80)90048-1","volume":"10","author":"D. Kozen","year":"1980","unstructured":"Kozen, D.: Complexity of boolean algebras. Theoretical Computer Science\u00a010, 221\u2013247 (1980)","journal-title":"Theoretical Computer Science"},{"key":"28_CR21","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Lam, P., Rinard, M.: Role analysis. In: Proc. 29th POPL (2002)","DOI":"10.1145\/503272.503276"},{"key":"28_CR22","unstructured":"Kuncak, V., Rinard, M.: The first-order theory of sets with cardinality constraints is decidable. Technical Report 958, MIT CSAIL (July 2004)"},{"key":"28_CR23","doi-asserted-by":"crossref","unstructured":"Lam, P., Kuncak, V., Rinard, M.: Generalized Typestate Checking for Data Structure Consistency 447. On our experience with modular pluggable analyses. Technical Report 965, MIT CSAIL (September 2004)","DOI":"10.1007\/978-3-540-30579-8_28"},{"key":"28_CR24","unstructured":"Lam, P., Kuncak, V., Zee, K., Rinard, M.: The Hob project web page (2004), http:\/\/cag.csail.mit.edu\/~plam\/hob\/"},{"key":"28_CR25","unstructured":"Leino, K.R.M.: Efficient weakest preconditions. KRML114a (2003)"},{"key":"28_CR26","first-page":"228","volume":"76","author":"L. Loewenheim","year":"1915","unstructured":"Loewenheim, L.: \u00dcber m\u00f6gligkeiten im relativkalk\u00fcl. Math. Annalen\u00a076, 228\u2013251 (1915)","journal-title":"Math. Annalen"},{"key":"28_CR27","doi-asserted-by":"crossref","unstructured":"M\u00f8ller, A., Schwartzbach, M.I.: The Pointer Assertion Logic Engine. In: Proc. ACM PLDI (2001)","DOI":"10.1145\/378795.378851"},{"issue":"3","key":"28_CR28","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM TOPLAS\u00a024(3), 217\u2013298 (2002)","journal-title":"ACM TOPLAS"},{"key":"28_CR29","unstructured":"Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis problems. In: Program Flow Analysis: Theory and Applications. Prentice-Hall, Inc., Englewood Cliffs (1981)"},{"key":"28_CR30","volume-title":"Typestate: A programming language concept for enhancing software reliability","author":"R.E. Strom","year":"1986","unstructured":"Strom, R.E., Yemini, S.: Typestate: A programming language concept for enhancing software reliability, January. IEEE TSE, Los Alamitos (1986)"},{"key":"28_CR31","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","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30579-8_28.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:24:18Z","timestamp":1605759858000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30579-8_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540242970","9783540305798"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30579-8_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}