{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:59:05Z","timestamp":1725551945645},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540311393"},{"type":"electronic","value":"9783540316220"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11609773_11","type":"book-chapter","created":{"date-parts":[[2005,12,12]],"date-time":"2005-12-12T07:28:57Z","timestamp":1134372537000},"page":"157-173","source":"Crossref","is-referenced-by-count":26,"title":["Field Constraint Analysis"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Wies","sequence":"first","affiliation":[]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[]},{"given":"Patrick","family":"Lam","sequence":"additional","affiliation":[]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Rinard","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"Refinement Calculus","author":"R.-J. Back","year":"1998","unstructured":"Back, R.-J., von Wright, J.: Refinement Calculus. Springer, Heidelberg (1998)"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-540-30579-8_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"I. Balaban","year":"2005","unstructured":"Balaban, I., Pnueli, A., Zuck, L.: Shape analysis by predicate abstraction. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 164\u2013180. Springer, Heidelberg (2005)"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, pp. 269\u2013282 (1979)","DOI":"10.1145\/567752.567778"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/3-540-36384-X_25","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D. Dams","year":"2002","unstructured":"Dams, D., Namjoshi, K.S.: Shape analysis through predicate abstraction and model checking. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 310\u2013323. Springer, Heidelberg (2002)"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Fradet, P., M\u00e9tayer, D.L.: Shape types. In: Proc. 24th ACM POPL (1997)","DOI":"10.1145\/263699.263706"},{"key":"11_CR6","unstructured":"Ghiya, R., Hendren, L.: Is it a tree, a DAG, or a cyclic graph? In: Proc. 23rd ACM POPL (1996)"},{"key":"11_CR7","unstructured":"Gr\u00e4del, E.: Decidable fragments of first-order and fixed-point logic. From prefix-vocabulary classes to guarded logics. In: Proceedings of Kalm\u00e1r Workshop on Logic and Computer Science, Szeged (2003)"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL (2002)","DOI":"10.1145\/503272.503279"},{"key":"11_CR9","volume-title":"Descriptive Complexity","author":"N. Immerman","year":"1998","unstructured":"Immerman, N.: Descriptive Complexity. Springer, Heidelberg (1998)"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Immerman, N., Rabinovich, A.M., Reps, T.W., Sagiv, S., Yorsh, G.: The boundary between decidability and undecidability for transitive-closure logics. In: Computer Science Logic (CSL), pp. 160\u2013174 (2004)","DOI":"10.1007\/978-3-540-30124-0_15"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-540-27813-9_22","volume-title":"Computer Aided Verification","author":"N. Immerman","year":"2004","unstructured":"Immerman, N., Rabinovich, A.M., Reps, T.W., Sagiv, S., Yorsh, G.: Verification via structure simulation. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 281\u2013294. Springer, Heidelberg (2004)"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Jensen, J.L., J\u00f8rgensen, M.E., Klarlund, N., Schwartzbach, M.I.: Automatic verification of pointer programs using monadic second order logic. In: Proc. ACM PLDI, Las Vegas, NV (1997)","DOI":"10.1145\/258915.258936"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/3-540-44674-5_15","volume-title":"Implementation and Application of Automata","author":"N. Klarlund","year":"2001","unstructured":"Klarlund, N., M\u00f8ller, A., Schwartzbach, M.I.: MONA implementation secrets. In: Yu, S., P\u0103un, A. (eds.) CIAA 2000. LNCS, vol.\u00a02088, p. 182. Springer, Heidelberg (2001)"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Klarlund, N., Schwartzbach, M.I.: Graph types. In: Proc. 20th ACM POPL, Charleston, SC (1993)","DOI":"10.1145\/158511.158628"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Lam, P., Rinard, M.: Role analysis. In: Proc. 29th POPL (2002)","DOI":"10.1145\/503272.503276"},{"key":"11_CR16","unstructured":"Kuncak, V., Lam, P., Zee, K., Rinard, M.: Implications of a data structure consistency checking system. In: Int. conf. on Verified Software: Theories, Tools, Experiments (VSTTE, IFIP Working Group 2.3 Conference), Z\u00fcrich (October 2005)"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Rinard, M.: Boolean algebra of shape analysis constraints. In: Proc. 5th International Conference on Verification, Model Checking and Abstract Interpretation (2004)","DOI":"10.1007\/978-3-540-24622-0_7"},{"key":"11_CR18","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":"11_CR19","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Qadeer, S.: Verifying properties of well-founded linked lists. In: POPL 2006 (2006)","DOI":"10.1145\/1111037.1111048"},{"key":"11_CR20","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":"11_CR21","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":"11_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-540-31987-0_10","volume-title":"Programming Languages and Systems","author":"O. Lee","year":"2005","unstructured":"Lee, O., Yang, H., Yi, K.: Automatic verification of pointer programs using grammar-based shape analysis. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 124\u2013140. Springer, Heidelberg (2005)"},{"key":"11_CR23","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/11532231_8","volume-title":"Automated Deduction \u2013 CADE-20","author":"T. Lev-Ami","year":"2005","unstructured":"Lev-Ami, T., Immerman, N., Reps, T., Sagiv, M., Srivastava, S., Yorsh, G.: Simulating reachability using first-order logic with applications to verification of linked data structures. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 99\u2013115. Springer, Heidelberg (2005)"},{"key":"11_CR24","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":"11_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/11513988_47","volume-title":"Computer Aided Verification","author":"S. McPeak","year":"2005","unstructured":"McPeak, S., Necula, G.C.: Data structure specifications via local equality axioms. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 476\u2013490. Springer, Heidelberg (2005)"},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"M\u00f8ller, A., Schwartzbach, M.I.: The Pointer Assertion Logic Engine. In: Programming Language Design and Implementation (2001)","DOI":"10.1145\/378795.378851"},{"volume-title":"Program Flow Analysis: Theory and Applications","year":"1981","key":"11_CR27","unstructured":"Muchnick, S.S., Jones, N.D. (eds.): Program Flow Analysis: Theory and Applications. Prentice-Hall, Inc., Englewood Cliffs (1981)"},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"Nelson, G.: Verifying reachability invariants of linked structures. In: POPL (1983)","DOI":"10.1145\/567067.567073"},{"key":"11_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/11547662_19","volume-title":"Static Analysis","author":"A. Podelski","year":"2005","unstructured":"Podelski, A., Wies, T.: Boolean heaps. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 268\u2013283. Springer, Heidelberg (2005)"},{"issue":"6","key":"11_CR30","doi-asserted-by":"publisher","first-page":"668","DOI":"10.1145\/78973.78977","volume":"33","author":"W. Pugh","year":"1990","unstructured":"Pugh, W.: Skip lists: A probabilistic alternative to balanced trees. Communications of the ACM\u00a033(6), 668\u2013676 (1990)","journal-title":"Communications of the ACM"},{"key":"11_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/3-540-36575-3_26","volume-title":"Programming Languages and Systems","author":"T. Reps","year":"2003","unstructured":"Reps, T., Sagiv, M., Loginov, A.: Finite differencing of logical formulas for static analysis. In: Degano, P. (ed.) ESOP 2003. LNCS, vol.\u00a02618, pp. 380\u2013398. Springer, Heidelberg (2003)"},{"issue":"3","key":"11_CR32","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":"11_CR33","unstructured":"Wies, T.: Symbolic shape analysis. Master\u2019s thesis, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany (September 2004)"},{"key":"11_CR34","doi-asserted-by":"crossref","unstructured":"Wies, T., Kuncak, V., Lam, P., Podelski, A., Rinard, M.: On field constraint analysis. Technical Report MIT-CSAIL-TR-2005-072, MIT-LCS-TR-1010, MIT CSAIL (November 2005)","DOI":"10.1007\/11609773_11"},{"key":"11_CR35","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":"11_CR36","unstructured":"Yorsh, G., Reps, T., Sagiv, M., Wilhelm, R.: Logical characterizations of heap abstractions. In: TOCL (2005) (to appear)"},{"key":"11_CR37","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"}],"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\/11609773_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:06:57Z","timestamp":1619507217000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11609773_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540311393","9783540316220"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/11609773_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}