{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:08:20Z","timestamp":1725516500246},"publisher-location":"Berlin, Heidelberg","reference-count":37,"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_11","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"82-92","source":"Crossref","is-referenced-by-count":0,"title":["Automatic Verification of Strongly Dynamic Software Systems"],"prefix":"10.1007","author":[{"given":"N.","family":"Dor","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J.","family":"Field","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"D.","family":"Gopan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"T.","family":"Lev-Ami","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Loginov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R.","family":"Manevich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"G.","family":"Ramalingam","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"T.","family":"Reps","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"N.","family":"Rinetzky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Sagiv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R.","family":"Wilhelm","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"E.","family":"Yahav","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"G.","family":"Yorsh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","unstructured":"Arnold, G.: Combining heap analyses by intersecting abstractions. Master\u2019s thesis, Tel Aviv University (October 2004)"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Ashcraft, K., Engler, D.: Using programmer-written compiler extensions to catch security holes. In: Proc. IEEE Symp. on Security and Privacy, Oakland, CA (May 2002)","DOI":"10.1109\/SECPRI.2002.1004368"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/BFb0053547","volume-title":"Foundations of Software Science and Computation Structures","author":"L. Cardelli","year":"1998","unstructured":"Cardelli, L., Gordon, A.D.: Mobile ambients. In: Nivat, M. (ed.) ETAPS 1998 and FOSSACS 1998. LNCS, vol.\u00a01378, pp. 140\u2013155. Springer, Heidelberg (1998)"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Proc. Computer Aided Verification, pp. 154\u2013169 (2000)","DOI":"10.1007\/10722167_15"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Corbett, J., Dwyer, M., Hatcliff, J., Pasareanu, C., R.,, Laubach, S., Zheng, H.: Bandera: Extracting finite-state models from Java source code. In: Proc. Intl. Conf. on Software Eng, June 2000, pp. 439\u2013448 (2000)","DOI":"10.1145\/337180.337234"},{"key":"11_CR6","first-page":"269","volume-title":"Proc. Symp. on Principles of Prog. Languages","author":"P. Cousot","year":"1979","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proc. Symp. on Principles of Prog. Languages, pp. 269\u2013282. ACM Press, New York (1979)"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Das, M., Lerner, S., Seigle, M.: ESP: Path-sensitive program verification in polynomial time. In: Proc. Conf. on Prog. Lang. Design and Impl, pp. 57\u201368 (June 2002)","DOI":"10.1145\/543552.512538"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"DeLine, R., F\u00e4hndrich, M.: Enforcing high-level protocols in low-level software. In: Proc. Conf. on Prog. Lang. Design and Impl. pp. 59\u201369 (June 2001)","DOI":"10.1145\/378795.378811"},{"key":"11_CR9","volume-title":"Proc. Static Analysis Symp.","author":"N. Dor","year":"2000","unstructured":"Dor, N., Rodeh, M., Sagiv, M.: Checking cleanness in linked lists. In: Proc. Static Analysis Symp. Springer, Heidelberg (2000)"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1007\/3-540-44898-5_25","volume-title":"Static Analysis","author":"J. Field","year":"2003","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, pp. 439\u2013462. Springer, Heidelberg (2003)"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for java. In: Proc. Conf. on Prog. Lang. Design and Impl. Berlin, pp. 234\u2013245 (June 2002)","DOI":"10.1145\/512529.512558"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Foster, J.S., Terauchi, T., Aiken, A.: Flow-sensitive type qualifiers. In: Proc. Conf. on Prog. Lang. Design and Impl. Berlin, pp. 1\u201312 (June 2002)","DOI":"10.1145\/512529.512531"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Gopan, D., DiMaio, F., Dor, N., Reps, T., Sagiv, M.: Numeric domains with summarized dimensions. In: Tools and Algs.for the Construct.and Anal.of Syst. pp. 512\u2013529 (2004)","DOI":"10.1007\/978-3-540-24730-2_38"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Gopan, D., Reps, T., Sagiv, M.: Numeric analysis of array operations. In: Proc. Symp. on Principles of Prog. Languages (2005)","DOI":"10.1145\/1040305.1040333"},{"issue":"2","key":"11_CR15","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/BF00976239","volume":"4","author":"C.A.R. Hoare","year":"1975","unstructured":"Hoare, C.A.R.: Recursive data structures. Int. J. of Comp. and Inf. Sci.\u00a04(2), 105\u2013132 (1975)","journal-title":"Int. J. of Comp. and Inf. Sci."},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Jeannet, B., Gopan, D., Reps, T.: A relational abstraction for functions. In: To appear in Proc. 12th Int. Static Analysis Symp. (September 2005) (to appear)","DOI":"10.1007\/11547662_14"},{"key":"11_CR17","volume-title":"Proc. Static Analysis Symp.","author":"B. Jeannet","year":"2004","unstructured":"Jeannet, B., Loginov, A., Reps, T., Sagiv, M.: A relational approach to interprocedural shape analysis. In: Proc. Static Analysis Symp. Springer, Heidelberg (2004)"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: Proc. Static Analysis Symp. pp. 280\u2013301 (2000)","DOI":"10.1007\/978-3-540-45099-3_15"},{"key":"11_CR19","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: Int.Symp.on Softw.Testing and Analysis, pp. 26\u201338 (2000)","DOI":"10.1145\/347324.348031"},{"key":"11_CR20","unstructured":"Loginov, A., Reps, T., Sagiv, M.: Learning abstractions for verifying data-structure properties. In: Int.Conf.on Computer Aided Verif. (2005)"},{"key":"11_CR21","doi-asserted-by":"crossref","unstructured":"Manevich, R., Ramalingam, G., Field, J., Goyal, D., Sagiv, M.: Compactly representing first-order structures for static analysis. In: Proc. Static Analysis Symp. pp. 196\u2013212 (2002)","DOI":"10.1007\/3-540-45789-5_16"},{"key":"11_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-540-27864-1_20","volume-title":"Static Analysis","author":"R. Manevich","year":"2004","unstructured":"Manevich, R., Sagiv, M., Ramalingam, G., Field, J.: Partially disjunctive heap abstraction. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 265\u2013279. Springer, Heidelberg (2004)"},{"key":"11_CR23","series-title":"Lecture Notes in Computer Science","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R. Manevich","year":"2005","unstructured":"Manevich, R., Yahav, E., Ramalingam, G., Sagiv, M.: Predicate abstraction and canonical abstraction for singly-linked lists. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, Springer, Heidelberg (2005)"},{"key":"11_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/3-540-46425-5_20","volume-title":"Programming Languages and Systems","author":"F. Nielson","year":"2000","unstructured":"Nielson, F., Nielson, H.R., Sagiv, M.: A Kleene Analysis of Mobile Ambients. In: Smolka, G. (ed.) ESOP 2000 and ETAPS 2000. LNCS, vol.\u00a01782, pp. 305\u2013319. Springer, Heidelberg (2000)"},{"key":"11_CR25","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: Proc. Conf. on Prog. Lang. Design and Impl. pp. 83\u201394 (2002)","DOI":"10.1145\/512529.512540"},{"key":"11_CR26","unstructured":"Reig, F.: Detecting security vulnerabilities in C code with type checking (extended abstract) (2003), http:\/\/www.cs.nott.ac.uk\/~fxr\/"},{"key":"11_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/3-540-45306-7_10","volume-title":"Compiler Construction","author":"N. Rinetskey","year":"2001","unstructured":"Rinetskey, N., Sagiv, M.: Interprocedural shape analysis for recursive programs. In: Wilhelm, R. (ed.) CC 2001 and ETAPS 2001. LNCS, vol.\u00a02027, pp. 133\u2013149. Springer, Heidelberg (2001)"},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"Rinetzky, N., Bauer, J., Reps, T., Sagiv, M., Wilhelm, R.: A semantics for procedure local heaps and its abstractions. In: Proc. Symp. on Principles of Prog. Languages (2005)","DOI":"10.1145\/1040305.1040330"},{"key":"11_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_20","volume-title":"Static Analysis","author":"N. Rinetzky","year":"2005","unstructured":"Rinetzky, N., Sagiv, M., Yahav, E.: Interprocedural shape analysis for cutpoint-free programs. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, Springer, Heidelberg (2005)"},{"issue":"3","key":"11_CR30","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 Transactions on Programming Languages and Systems\u00a024(3), 217\u2013298 (2002)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"11_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/3-540-44898-5_27","volume-title":"Static Analysis","author":"R. Shaham","year":"2003","unstructured":"Shaham, R., Yahav, E., Kolodner, E.K., Sagiv, M.: Establishing local temporal heap safety properties with applications to compile-time memory management. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 483\u2013503. Springer, Heidelberg (2003)"},{"issue":"1","key":"11_CR32","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1109\/TSE.1986.6312929","volume":"12","author":"R.E. Strom","year":"1986","unstructured":"Strom, R.E., Yemini, S.: Typestate: A programming language concept for enhancing software reliability. IEEE Trans. Software Eng.\u00a012(1), 157\u2013171 (1986)","journal-title":"IEEE Trans. Software Eng."},{"key":"11_CR33","doi-asserted-by":"crossref","unstructured":"Yahav, E.: Verifying safety properties of concurrent Java programs using 3-valued logic. In: Proc. Symp. on Principles of Prog. Languages, pp. 27\u201340 (2001)","DOI":"10.1145\/373243.360206"},{"key":"11_CR34","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1145\/996841.996846","volume-title":"Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation","author":"E. Yahav","year":"2004","unstructured":"Yahav, E., Ramalingam, G.: Verifying safety properties using separation and heterogeneous abstractions. In: Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, pp. 25\u201334. ACM Press, New York (2004), doi:10.1145\/996841.996846"},{"key":"11_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/3-540-36575-3_15","volume-title":"Programming Languages and Systems","author":"E. Yahav","year":"2003","unstructured":"Yahav, E., Reps, T., Sagiv, M., Wilhelm, R.: Verifying temporal heap properties specified via evolution logic. In: Degano, P. (ed.) ESOP 2003 and ETAPS 2003. LNCS, vol.\u00a02618, pp. 204\u2013222. Springer, Heidelberg (2003)"},{"key":"11_CR36","doi-asserted-by":"crossref","unstructured":"Yahav, E., Sagiv, M.: Automatically verifying concurrent queue algorithms. In: Workshop on Software Model Checking (2003)","DOI":"10.1016\/S1571-0661(05)80006-4"},{"key":"11_CR37","doi-asserted-by":"crossref","unstructured":"Yorsh, G., Reps, T., Sagiv, M.: Symbolically computing most-precise abstract operations for shape analysis. In: Tools and Algs.for the Construct.and Anal.of Syst. pp. 530\u2013545 (2004)","DOI":"10.1007\/978-3-540-24730-2_39"}],"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_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T07:42:31Z","timestamp":1557733351000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69149-5_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540691471","9783540691495"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69149-5_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}