{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:32:36Z","timestamp":1750307556713,"version":"3.41.0"},"reference-count":63,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2010,8,1]],"date-time":"2010-08-01T00:00:00Z","timestamp":1280620800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["CCR-{9619219, 9986308}CCF-{0540955, 0524051}"],"award-info":[{"award-number":["CCR-{9619219, 9986308}CCF-{0540955, 0524051}"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-01-1-{0708,0796}"],"award-info":[{"award-number":["N00014-01-1-{0708,0796}"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001742","name":"United States-Israel Binational Science Foundation","doi-asserted-by":"publisher","award":["96-00337"],"award-info":[{"award-number":["96-00337"]}],"id":[{"id":"10.13039\/501100001742","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCR-{9619219, 9986308}CCF-{0540955, 0524051}"],"award-info":[{"award-number":["CCR-{9619219, 9986308}CCF-{0540955, 0524051}"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2010,8]]},"abstract":"<jats:p>\n            This article concerns mechanisms for maintaining the value of an instrumentation relation (also known as a\n            <jats:italic>derived relation<\/jats:italic>\n            or\n            <jats:italic>view<\/jats:italic>\n            ), defined via a logical formula over core relations, in response to changes in the values of the core relations. It presents an algorithm for transforming the instrumentation relation's defining formula into a\n            <jats:italic>relation-maintenance formula<\/jats:italic>\n            that captures what the instrumentation relation's new value should be. The algorithm runs in time linear in the size of the defining formula.\n          <\/jats:p>\n          <jats:p>The technique applies to program analysis problems in which the semantics of statements is expressed using logical formulas that describe changes to core relation values. It provides a way to obtain values of the instrumentation relations that reflect the changes in core relation values produced by executing a given statement.<\/jats:p>\n          <jats:p>We present experimental evidence that our technique is an effective one: for a variety of benchmarks, the relation-maintenance formulas produced automatically using our approach yield the same precision as the best available hand-crafted ones.<\/jats:p>","DOI":"10.1145\/1749608.1749613","type":"journal-article","created":{"date-parts":[[2010,8,11]],"date-time":"2010-08-11T12:57:24Z","timestamp":1281531444000},"page":"1-55","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Finite differencing of logical formulas for static analysis"],"prefix":"10.1145","volume":"32","author":[{"given":"Thomas","family":"Reps","sequence":"first","affiliation":[{"name":"University of Wisconsin and GrammaTech, Inc."}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexey","family":"Loginov","sequence":"additional","affiliation":[{"name":"GrammaTech, Inc."}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2010,8,13]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1137\/0107041"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"volume-title":"Proceedings of the SPIN Workshop. 103--122","author":"Ball T.","key":"e_1_2_2_3_1","unstructured":"Ball , T. and Rajamani , S . 2001. Automatically validating temporal safety properties of interfaces . In Proceedings of the SPIN Workshop. 103--122 . Ball, T. and Rajamani, S. 2001. Automatically validating temporal safety properties of interfaces. In Proceedings of the SPIN Workshop. 103--122."},{"volume-title":"Proceedings of the Conference on Computer-Aided Verification. 178--192","author":"Berdine J.","key":"e_1_2_2_4_1","unstructured":"Berdine , J. , Calcagno , C. , Cook , B. , Distefano , D. , O'Hearn , P. , Wies , T. , and Yang , H . 2007. Shape analysis for composite data structures . In Proceedings of the Conference on Computer-Aided Verification. 178--192 . Berdine, J., Calcagno, C., Cook, B., Distefano, D., O'Hearn, P., Wies, T., and Yang, H. 2007. Shape analysis for composite data structures. In Proceedings of the Conference on Computer-Aided Verification. 178--192."},{"key":"e_1_2_2_5_1","unstructured":"Boerger E. and Staerk R. 2003. Abstract State Machines: A Method for High-Level System Design and Analysis. Springer.   Boerger E. and Staerk R. 2003. Abstract State Machines: A Method for High-Level System Design and Analysis. Springer."},{"key":"e_1_2_2_6_1","unstructured":"Bogudlov I. Lev-Ami T. Reps T. and Sagiv M. 2007a. Revamping TVLA: Making parametric shape analysis competitive. Tech. rep. TR-2007-01-01 Tel-Aviv University Tel-Aviv Israel.  Bogudlov I. Lev-Ami T. Reps T. and Sagiv M. 2007a. Revamping TVLA: Making parametric shape analysis competitive. Tech. rep. TR-2007-01-01 Tel-Aviv University Tel-Aviv Israel."},{"volume-title":"Proceedings of the Conference on Computer-Aided Verification. 221--225","author":"Bogudlov I.","key":"e_1_2_2_7_1","unstructured":"Bogudlov , I. , Lev-Ami , T. , Reps , T. , and Sagiv , M . 2007b. Revamping TVLA: Making parametric shape analysis competitive (tool paper) . In Proceedings of the Conference on Computer-Aided Verification. 221--225 . Bogudlov, I., Lev-Ami, T., Reps, T., and Sagiv, M. 2007b. Revamping TVLA: Making parametric shape analysis competitive (tool paper). In Proceedings of the Conference on Computer-Aided Verification. 221--225."},{"volume-title":"Proceedings of the International Conference on Software Engineering. 385--395","author":"Chaki S.","key":"e_1_2_2_8_1","unstructured":"Chaki , S. , Clarke , E. , Groce , A. , Jha , S. , and Veith , H . 2003. Modular verification of software components in C . In Proceedings of the International Conference on Software Engineering. 385--395 . Chaki, S., Clarke, E., Groce, A., Jha, S., and Veith, H. 2003. Modular verification of software components in C. In Proceedings of the International Conference on Software Engineering. 385--395."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.734089"},{"key":"e_1_2_2_10_1","doi-asserted-by":"crossref","unstructured":"Cousot P. 2003. Verification by abstract interpretation. In Verification: Theory and Practice. 243--268.  Cousot P. 2003. Verification by abstract interpretation. In Verification: Theory and Practice. 243--268.","DOI":"10.1007\/978-3-540-39910-0_11"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"volume-title":"Proceedings of the Conference on Computer-Aided Verification. 160--171","author":"Das S.","key":"e_1_2_2_13_1","unstructured":"Das , S. , Dill , D. , and Park , S . 1999. Experience with predicate abstraction . In Proceedings of the Conference on Computer-Aided Verification. 160--171 . Das, S., Dill, D., and Park, S. 1999. Experience with predicate abstraction. In Proceedings of the Conference on Computer-Aided Verification. 160--171."},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_19"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1102"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/344788.344808"},{"volume-title":"Proceedings of the Static Analysis Symposium. 115--134","author":"Dor N.","key":"e_1_2_2_17_1","unstructured":"Dor , N. , Rodeh , M. , and Sagiv , M . 2000. Checking cleanness in linked lists . In Proceedings of the Static Analysis Symposium. 115--134 . Dor, N., Rodeh, M., and Sagiv, M. 2000. Checking cleanness in linked lists. In Proceedings of the Static Analysis Symposium. 115--134."},{"volume-title":"A History of Numerical Analysis","author":"Goldstine H.","key":"e_1_2_2_18_1","unstructured":"Goldstine , H. 1977. A History of Numerical Analysis . Springer . Goldstine, H. 1977. A History of Numerical Analysis. Springer."},{"volume-title":"Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems. 512--529","author":"Gopan D.","key":"e_1_2_2_19_1","unstructured":"Gopan , D. , DiMaio , F. , Dor , N. , Reps , T. , and Sagiv , M . 2004. Numeric domains with summarized dimensions . In Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems. 512--529 . Gopan, D., DiMaio, F., Dor, N., Reps, T., and Sagiv, M. 2004. Numeric domains with summarized dimensions. In Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems. 512--529."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040333"},{"volume-title":"Proceedings of the Conference on Computer-Aided Verification. 72--83","author":"Graf S.","key":"e_1_2_2_21_1","unstructured":"Graf , S. and Sa\u00efdi , H . 1997. Construction of abstract state graphs with PVS . In Proceedings of the Conference on Computer-Aided Verification. 72--83 . Graf, S. and Sa\u00efdi, H. 1997. Construction of abstract state graphs with PVS. In Proceedings of the Conference on Computer-Aided Verification. 72--83."},{"key":"e_1_2_2_22_1","volume-title":"Eds","author":"Gupta A.","year":"1999","unstructured":"Gupta , A. and Mumick , I. , Eds . 1999 . Materialized Views : Techniques, Implementations, and Applications. MIT Press , Cambridge, MA. Gupta, A. and Mumick, I., Eds. 1999. Materialized Views: Techniques, Implementations, and Applications. MIT Press, Cambridge, MA."},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"volume-title":"Proceedings of the Conference on Computer-Aided Verification. 281--294","author":"Immerman N.","key":"e_1_2_2_25_1","unstructured":"Immerman , N. , Rabinovich , A. , Reps , T. , Sagiv , M. , and Yorsh , G . 2004. Verification via structure simulation . In Proceedings of the Conference on Computer-Aided Verification. 281--294 . Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., and Yorsh, G. 2004. Verification via structure simulation. In Proceedings of the Conference on Computer-Aided Verification. 281--294."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.375719"},{"key":"e_1_2_2_27_1","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"Jackson D.","year":"2006","unstructured":"Jackson , D. 2006 . Software Abstractions: Logic, Language, and Analysis . MIT Press, Cambridge , MA. Jackson, D. 2006. Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge, MA."},{"volume-title":"Proceedings of the Static Analysis Symposium. 246--264","author":"Jeannet B.","key":"e_1_2_2_28_1","unstructured":"Jeannet , B. , Loginov , A. , Reps , T. , and Sagiv , M . 2004. A relational approach to interprocedural shape analysis . In Proceedings of the Static Analysis Symposium. 246--264 . Jeannet, B., Loginov, A., Reps, T., and Sagiv, M. 2004. A relational approach to interprocedural shape analysis. In Proceedings of the Static Analysis Symposium. 246--264."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1667048.1667050"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158628"},{"volume-title":"Computer-Aided Verification of Coordinating Processes","author":"Kurshan R.","key":"e_1_2_2_31_1","unstructured":"Kurshan , R. 1994. Computer-Aided Verification of Coordinating Processes . Princeton University Press . Kurshan, R. 1994. Computer-Aided Verification of Coordinating Processes. Princeton University Press."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111048"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/347324.348031"},{"volume-title":"Proceedings of the Static Analysis Symposium. 280--301","author":"Lev-Ami T.","key":"e_1_2_2_34_1","unstructured":"Lev-Ami , T. and Sagiv , M . 2000. TVLA: A system for implementing static analyses . In Proceedings of the Static Analysis Symposium. 280--301 . Lev-Ami, T. and Sagiv, M. 2000. TVLA: A system for implementing static analyses. In Proceedings of the Static Analysis Symposium. 280--301."},{"volume-title":"Proceedings of the Conference on Compiler Construction. 36--52","author":"Lim J.","key":"e_1_2_2_35_1","unstructured":"Lim , J. and Reps , T . 2008. A system for generating static analyzers for machine instructions . In Proceedings of the Conference on Compiler Construction. 36--52 . Lim, J. and Reps, T. 2008. A system for generating static analyzers for machine instructions. In Proceedings of the Conference on Compiler Construction. 36--52."},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237769"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)00031-9"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_50"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_17"},{"key":"e_1_2_2_41_1","doi-asserted-by":"crossref","unstructured":"Loginov A. Reps T. and Sagiv M. 2007. Refinement-based verification for possibly-cyclic lists. In Program Analysis and Compilation Theory and Practice: Essays Dedicated to Reinhard Wilhelm. 247--272.   Loginov A. Reps T. and Sagiv M. 2007. Refinement-based verification for possibly-cyclic lists. In Program Analysis and Compilation Theory and Practice: Essays Dedicated to Reinhard Wilhelm. 247--272.","DOI":"10.1007\/978-3-540-71322-7_12"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_13"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.5555\/646704.702020"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1038\/218019a0"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378851"},{"key":"e_1_2_2_47_1","doi-asserted-by":"crossref","unstructured":"Mycroft A. and Jones N. 1985. A relational framework for abstract interpretation. In Programs as Data Objects. 156--171.   Mycroft A. and Jones N. 1985. A relational framework for abstract interpretation. In Programs as Data Objects. 156--171.","DOI":"10.1007\/3-540-16446-4_9"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/512644.512672"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/567067.567073"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(89)90091-1"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/357172.357177"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1997.1520"},{"volume-title":"Proceedings of the Conference on Logic in Computer Science. 40--54","author":"Reps T.","key":"e_1_2_2_53_1","unstructured":"Reps , T. , Loginov , A. , and Sagiv , M . 2002. Semantic minimization of 3-valued propositional formulae . In Proceedings of the Conference on Logic in Computer Science. 40--54 . Reps, T., Loginov, A., and Sagiv, M. 2002. Semantic minimization of 3-valued propositional formulae. In Proceedings of the Conference on Logic in Computer Science. 40--54."},{"volume-title":"Proceedings of the European Symposium on Programming. 380--398","author":"Reps T.","key":"e_1_2_2_54_1","unstructured":"Reps , T. , Sagiv , M. , and Loginov , A . 2003. Finite differencing of logical formulas for static analysis . In Proceedings of the European Symposium on Programming. 380--398 . Reps, T., Sagiv, M., and Loginov, A. 2003. Finite differencing of logical formulas for static analysis. In Proceedings of the European Symposium on Programming. 380--398."},{"volume-title":"Proceedings of the Conference on Computer-Aided Verification. 15--30","author":"Reps T.","key":"e_1_2_2_55_1","unstructured":"Reps , T. , Sagiv , M. , and Wilhelm , R . 2004a. Static program analysis via 3-valued logic . In Proceedings of the Conference on Computer-Aided Verification. 15--30 . Reps, T., Sagiv, M., and Wilhelm, R. 2004a. Static program analysis via 3-valued logic. In Proceedings of the Conference on Computer-Aided Verification. 15--30."},{"volume-title":"Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation. 252--266","author":"Reps T.","key":"e_1_2_2_56_1","unstructured":"Reps , T. , Sagiv , M. , and Yorsh , G . 2004b. Symbolic implementation of the best transformer . In Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation. 252--266 . Reps, T., Sagiv, M., and Yorsh, G. 2004b. Symbolic implementation of the best transformer. In Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation. 252--266."},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040330"},{"volume-title":"Proceedings of the Conference on Compiler Construction. 133--149","author":"Rinetzky N.","key":"e_1_2_2_59_1","unstructured":"Rinetzky , N. and Sagiv , M . 2001. Interprocedural shape analysis for recursive programs . In Proceedings of the Conference on Compiler Construction. 133--149 . Rinetzky, N. and Sagiv, M. 2001. Interprocedural shape analysis for recursive programs. In Proceedings of the Conference on Compiler Construction. 133--149."},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250750"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/357162.357166"},{"key":"e_1_2_2_63_1","unstructured":"TVLA. TVLA system. www.cs.tau.ac.il\/~tvla\/.  TVLA. TVLA system. www.cs.tau.ac.il\/~tvla\/."},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.2307\/2024549"},{"volume-title":"Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems. 530--545","author":"Yorsh G.","key":"e_1_2_2_65_1","unstructured":"Yorsh , G. , Reps , T. , and Sagiv , M . 2004. Symbolically computing most-precise abstract operations for shape analysis . In Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems. 530--545 . Yorsh, G., Reps, T., and Sagiv, M. 2004. Symbolically computing most-precise abstract operations for shape analysis. In Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems. 530--545."},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/1182613.1182618"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1749608.1749613","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1749608.1749613","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:23:45Z","timestamp":1750249425000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1749608.1749613"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,8]]},"references-count":63,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2010,8]]}},"alternative-id":["10.1145\/1749608.1749613"],"URL":"https:\/\/doi.org\/10.1145\/1749608.1749613","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2010,8]]},"assertion":[{"value":"2009-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-12-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-08-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}