{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:05:41Z","timestamp":1725566741376},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540282310"},{"type":"electronic","value":"9783540318972"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11538363_28","type":"book-chapter","created":{"date-parts":[[2005,9,27]],"date-time":"2005-09-27T13:35:33Z","timestamp":1127828133000},"page":"397-412","source":"Crossref","is-referenced-by-count":4,"title":["Bounded Model Checking of Pointer Programs"],"prefix":"10.1007","author":[{"given":"Witold","family":"Charatonik","sequence":"first","affiliation":[]},{"given":"Lilia","family":"Georgieva","sequence":"additional","affiliation":[]},{"given":"Patrick","family":"Maier","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"28_CR1","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1093\/jigpal\/8.3.325","volume":"8","author":"N. Alechina","year":"2000","unstructured":"Alechina, N., Immerman, N.: Reachability logic: An efficient fragment of transitive closure logic. Logic Journal of IGPL\u00a08, 325\u2013337 (2000)","journal-title":"Logic Journal of IGPL"},{"volume-title":"The Description Logic Handbook","year":"2003","key":"28_CR2","unstructured":"Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook. Cambridge University Press, Cambridge (2003)"},{"key":"28_CR3","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/BF01459101","volume":"99","author":"P. Bernays","year":"1928","unstructured":"Bernays, P., Sch\u00f6nfinkel, M.: Zum Entscheidungsproblem der Mathematischen Logik. Math. Annalen\u00a099, 342\u2013372 (1928)","journal-title":"Math. Annalen"},{"key":"28_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDD. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"28_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-540-30538-5_9","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"R. Bornat","year":"2004","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P.: A decidable fragment of separation logic. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, pp. 97\u2013109. Springer, Heidelberg (2004)"},{"key":"28_CR6","doi-asserted-by":"crossref","unstructured":"Charatonik, W., Georgieva, L., Maier, P.: Bounded model checking of pointer programs. Technical Report MPI-I-2005-2-002, Max-Planck-Institut f\u00fcr Informatik (2005)","DOI":"10.1007\/11538363_28"},{"key":"28_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"28_CR8","volume-title":"The Decision Problem. Solvable Classes of Quantificational Formulas","author":"B. Dreben","year":"1979","unstructured":"Dreben, B., Goldfarb, W.D.: The Decision Problem. Solvable Classes of Quantificational Formulas. Addison-Wesley, Reading (1979)"},{"key":"28_CR9","doi-asserted-by":"publisher","first-page":"1719","DOI":"10.2307\/2586808","volume":"64","author":"E. Gr\u00e4del","year":"1999","unstructured":"Gr\u00e4del, E.: On the restraining power of guards. J. Symbolic Logic\u00a064, 1719\u20131742 (1999)","journal-title":"J. Symbolic Logic"},{"key":"28_CR10","first-page":"306","volume-title":"Proc. LICS 1997","author":"E. Gr\u00e4del","year":"1997","unstructured":"Gr\u00e4del, E., Otto, M., Rosen, E.: Two-variable logic with counting is decidable. In: Proc. LICS 1997, pp. 306\u2013317. IEEE Computer Society Press, Los Alamitos (1997)"},{"key":"28_CR11","first-page":"45","volume-title":"Proc. LICS 1999","author":"E. Gr\u00e4del","year":"1999","unstructured":"Gr\u00e4del, E., Walukiewicz, I.: Guarded fixed point logic. In: Proc. LICS 1999, pp. 45\u201354. IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"28_CR12","unstructured":"Herzig, A.: Raisonnement automatique en logique modale et algorithmes d\u2019unification. PhD thesis, Universit\u00e9 Paul Sabatier, Toulouse (1989)"},{"key":"28_CR13","unstructured":"Herzig, A.: A new decidable fragment of first order logic. In: Abstracts of the 3rd Logical Biennial, Summer School & Conference in honour of S. C. Kleene, Varna, Bulgaria (June 1990)"},{"key":"28_CR14","doi-asserted-by":"crossref","unstructured":"Huth, M., Pradhan, S.: Consistent partial model checking. Electronic Notes in Theoretical Computer Science\u00a023 (2003)","DOI":"10.1016\/j.entcs.2004.08.003"},{"key":"28_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-540-30124-0_15","volume-title":"Computer Science Logic","author":"N. Immerman","year":"2004","unstructured":"Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., Yorsh, G.: The boundary between decidability and undecidability for transitive-closure logics. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol.\u00a03210, pp. 160\u2013174. Springer, Heidelberg (2004)"},{"key":"28_CR16","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., Reps, T., Sagiv, M., 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":"28_CR17","doi-asserted-by":"crossref","unstructured":"Jackson, D., Vaziri, M.: Finding bugs with a constraint solver. In: Proc. ISSTA 2000, pp. 14\u201325 (2000)","DOI":"10.1145\/347324.383378"},{"key":"28_CR18","doi-asserted-by":"crossref","unstructured":"Klarlund, N., Schwartzbach, M.I.: Graph types. In: Proc. POPL 1993, pp. 196\u2013205 (1993)","DOI":"10.1145\/158511.158628"},{"key":"28_CR19","unstructured":"Kuncak, V., Rinard, M.: On role logic. Technical Report 925, MIT Computer Science and Artificial Intelligence Laboratory (2003)"},{"key":"28_CR20","doi-asserted-by":"crossref","unstructured":"M\u00f8ller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: Proc. PLDI 2001, pp. 221\u2013231 (2001)","DOI":"10.1145\/378795.378851"},{"key":"28_CR21","unstructured":"Ramsey, F.: On a problem of formal logic. In: Proc. London Mathematical Society, pp. 338\u2013384 (1928)"},{"key":"28_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-540-24725-8_28","volume-title":"Programming Languages and Systems","author":"A. Rensink","year":"2004","unstructured":"Rensink, A.: Canonical graph shapes. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 401\u2013415. Springer, Heidelberg (2004)"},{"key":"28_CR23","unstructured":"Reynolds, J.: Intuitionistic reasoning about shared mutable data structure. In: Proc. of the, Oxford-Microsoft Symposium in Honour of Sir Tony Hoare (1999)"},{"issue":"2","key":"28_CR24","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 problems via 3-valued logic. ACM TOPLAS\u00a024(2), 217\u2013298 (2002)","journal-title":"ACM TOPLAS"},{"key":"28_CR25","unstructured":"Wies, T.: Symbolic shape analysis. Master\u2019s thesis, MPI Informatik, Saarbr\u00fccken, Germany (2004)"},{"key":"28_CR26","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, S.: 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)"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11538363_28.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:13:39Z","timestamp":1605644019000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11538363_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540282310","9783540318972"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/11538363_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}