{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:39:49Z","timestamp":1725493189839},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540008866"},{"type":"electronic","value":"9783540365754"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36575-3_26","type":"book-chapter","created":{"date-parts":[[2007,10,27]],"date-time":"2007-10-27T17:52:15Z","timestamp":1193507535000},"page":"380-398","source":"Crossref","is-referenced-by-count":31,"title":["Finite Differencing of Logical Formulas for Static Analysis"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Reps","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexey","family":"Loginov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"issue":"4","key":"26_CR1","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1137\/0107041","volume":"7","author":"S.B. Akers Jr.","year":"1959","unstructured":"S.B. Akers, Jr. On a theory of Boolean functions. J. Soc. Indust. Appl. Math., 7(4):487\u2013498, December 1959.","journal-title":"J. Soc. Indust. Appl. Math."},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"T. Ball, R. Majumdar, T. Millstein, and S.K. Rajamani. Automatic predicate abstraction of C programs. In Conf. on Prog. Lang. Design and Impl., NewYork, NY, 2001. ACM Press.","DOI":"10.1145\/378795.378846"},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Symp. on Princ. of Prog. Lang., pages 269\u2013282, NewYork, NY, 1979. ACM Press.","DOI":"10.1145\/567752.567778"},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"S. Das, D.L. Dill, and S. Park. Experience with predicate abstraction. In Proc. Computer-Aided Verif., pages 160\u2013171. Springer-Verlag, July 1999.","DOI":"10.1007\/3-540-48683-6_16"},{"key":"26_CR5","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1006\/inco.1995.1102","volume":"120","author":"G. Dong","year":"1995","unstructured":"G. Dong and J. Su. Incremental and decremental evaluation of transitive closure by first-order queries. Inf. and Comp., 120:101\u2013106, 1995.","journal-title":"Inf. and Comp."},{"issue":"1","key":"26_CR6","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1145\/344788.344808","volume":"29","author":"G. Dong","year":"2000","unstructured":"G. Dong and J. Su. Incremental maintenance of recursive views using relational calculus\/SQL. SIGMOD Record, 29(1):44\u201351, 2000.","journal-title":"SIGMOD Record"},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"S. Graf and H. Sa\u00efdi. Construction of abstract state graphs with PVS. In Proc. Computer-Aided Verif., pages 72\u201383, June 1997.","DOI":"10.1007\/3-540-63166-6_10"},{"volume-title":"Materialized Views: Techniques, Implementations, and Applications","year":"1999","key":"26_CR8","unstructured":"A. Gupta and I.S. Mumick, editors. Materialized Views: Techniques, Implementations, and Applications. The M.I.T. Press, Cambridge, MA, 1999."},{"key":"26_CR9","doi-asserted-by":"crossref","unstructured":"T. Lev-Ami, T. Reps, M. Sagiv, and R. Wilhelm. Putting static analysis towork for verification: A case study. In Int. Symp. on Software Testing and Analysis, pages 26\u201338, 2000.","DOI":"10.1145\/347636.348031"},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"T. Lev-Ami and M. Sagiv. TVLA: A system for implementing static analyses. In Static Analysis Symp., pages 280\u2013301, 2000.","DOI":"10.1007\/978-3-540-45099-3_15"},{"key":"26_CR11","doi-asserted-by":"crossref","unstructured":"Y.A. Liu, S.D. Stoller, and T. Teitelbaum. Discovering auxiliary information for incremental computation. In Symp. on Princ. of Prog. Lang., pages 157\u2013170, January 1996.","DOI":"10.1145\/237721.237769"},{"key":"26_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0167-6423(94)00031-9","volume":"24","author":"Y.A. Liu","year":"1995","unstructured":"Y.A. Liu and T. Teitelbaum. Systematic derivation of incremental programs. Sci. of Comp. Program., 24:1\u201339, 1995.","journal-title":"Sci. of Comp. Program."},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"K.L. McMillan. Verification of infinite state systems by compositional model checking. In CHARME, pages 219\u2013234, 1999.","DOI":"10.1007\/3-540-48153-2_17"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"A. M\u00f8ller and M.I. Schwartzbach. The pointer assertion logic engine. In Conf. on Prog. Lang. Design and Impl., pages 221\u2013231, 2001.","DOI":"10.1145\/381694.378851"},{"issue":"3","key":"26_CR15","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1145\/357172.357177","volume":"4","author":"R. Paige","year":"1982","unstructured":"R. Paige and S. Koenig. Finite differencing of computable expressions. Trans. on Prog. Lang. and Syst., 4(3):402\u2013454, July 1982.","journal-title":"Trans. on Prog. Lang. and Syst."},{"issue":"2","key":"26_CR16","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1006\/jcss.1997.1520","volume":"55","author":"S. Patnaik","year":"1997","unstructured":"S. Patnaik and N. Immerman. Dyn-FO: A parallel, dynamic complexity class. J. Comput. Syst. Sci., 55(2):199\u2013209, October 1997.","journal-title":"J. Comput. Syst. Sci."},{"issue":"3","key":"26_CR17","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. Trans. on Prog. Lang. and Syst., 24(3):217\u2013298, 2002.","journal-title":"Trans. on Prog. Lang. and Syst."},{"issue":"2","key":"26_CR18","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1145\/357162.357166","volume":"4","author":"M. Sharir","year":"1982","unstructured":"M. Sharir. Some observations concerning formal differentiation of set theoretic expressions. Trans. on Prog. Lang. and Syst., 4(2):196\u2013225, April 1982.","journal-title":"Trans. on Prog. Lang. and Syst."}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36575-3_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T22:17:41Z","timestamp":1556921861000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36575-3_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008866","9783540365754"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-36575-3_26","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}