{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:01:03Z","timestamp":1725490863683},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540735946"},{"type":"electronic","value":"9783540735953"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73595-3_11","type":"book-chapter","created":{"date-parts":[[2007,8,30]],"date-time":"2007-08-30T05:31:33Z","timestamp":1188451893000},"page":"147-166","source":"Crossref","is-referenced-by-count":17,"title":["Logical Interpretation: Static Program Analysis Using Theorem Proving"],"prefix":"10.1007","author":[{"given":"Ashish","family":"Tiwari","sequence":"first","affiliation":[]},{"given":"Sumit","family":"Gulwani","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Alpern, B., Wegman, M.N., Zadeck, F.K.: Detecting equality of variables in programs. In: 15th Annual ACM Symposium on POPL, pp. 1\u201311 (1988)","DOI":"10.1145\/73560.73561"},{"key":"11_CR2","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1016\/B978-044450813-3\/50010-2","volume-title":"Handbook of Automated Reasoning, ch. 8","author":"F. Baader","year":"2001","unstructured":"Baader, F., Snyder, W.: Unification theory. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 8, vol.\u00a0I, pp. 445\u2013532. Elsevier, Amsterdam (2001)"},{"key":"11_CR3","unstructured":"Cousot, P.: Forward relational infinitary static analysis, Lecture Notes (2005), Available at http:\/\/web.mit.edu\/afs\/athena.mit.edu\/course\/16\/16.399\/www"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th Annual ACM Symposium on POPL, pp. 234\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: 6th ACM Symp. on POPL, pp. 269\u2013282 (1979)","DOI":"10.1145\/567752.567778"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Rustan, K., Leino, M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: PLDI, pp. 234\u2013245 (2002)","DOI":"10.1145\/512529.512558"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1007\/978-3-540-27864-1_17","volume-title":"Static Analysis","author":"S. Gulwani","year":"2004","unstructured":"Gulwani, S., Necula, G.C.: A polynomial-time algorithm for global value numbering. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 212\u2013227. Springer, Heidelberg (2004)"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_19","volume-title":"Programming Languages and Systems","author":"S. Gulwani","year":"2006","unstructured":"Gulwani, S., Tiwari, A.: Assertion checking over combined abstraction of linear arithmetic and uninterpreted functions. In: Sestoft, P. (ed.) ESOP 2006 and ETAPS 2006. LNCS, vol.\u00a03924, Springer, Heidelberg (2006)"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Tiwari, A.: Combining abstract interpreters. In: PLDI (June 2006)","DOI":"10.1145\/1133981.1134026"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69738-1_26","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Gulwani","year":"2007","unstructured":"Gulwani, S., Tiwari, A.: Assertion checking unified. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, Springer, Heidelberg (to appear, 2007)"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Proc. European Symp. on Programming, ESOP 2007","author":"S. Gulwani","year":"2007","unstructured":"Gulwani, S., Tiwari, A.: Computing procedure summaries for interprocedural analysis. In: Proc. European Symp. on Programming, ESOP 2007. LNCS, Springer, Heidelberg (to appear, 2007)"},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"CAV","author":"S. Gulwani","year":"2007","unstructured":"Gulwani, S., Tiwari, A.: Static analysis of heap manipulating low-level software. In: CAV. LNCS, vol.\u00a04590, Springer, Heidelberg (2007)"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1007\/978-3-540-30538-5_26","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"S. Gulwani","year":"2004","unstructured":"Gulwani, S., Tiwari, A., Necula, G.C.: Join algorithms for the theory of uninterpreted symbols. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, pp. 311\u2013323. Springer, Heidelberg (2004)"},{"key":"11_CR14","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BF00268497","volume":"6","author":"M. Karr","year":"1976","unstructured":"Karr, M.: Affine relationships among variables of a program. Acta Informatica\u00a06, 133\u2013151 (1976)","journal-title":"Acta Informatica"},{"issue":"1","key":"11_CR15","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A. Mine","year":"2006","unstructured":"Mine, A.: The octagon abstract domain. Higher Order Symbol. Comput.\u00a019(1), 31\u2013100 (2006)","journal-title":"Higher Order Symbol. Comput."},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/978-3-540-30579-8_6","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M. M\u00fcller-Olm","year":"2005","unstructured":"M\u00fcller-Olm, M., R\u00fcthing, O., Seidl, H.: Checking Herbrand equalities and beyond. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 79\u201396. Springer, Heidelberg (2005)"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"M\u00fcller-Olm, M., Seidl, H.: A note on Karr\u2019s algorithm. In: 31st International Colloquium on Automata, Languages and Programming, pp. 1016\u20131028 (2004)","DOI":"10.1007\/978-3-540-27836-8_85"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: 31st ACM Symposium on POPL, pp. 330\u2013341 (January 2004)","DOI":"10.1145\/982962.964029"},{"issue":"2","key":"11_CR19","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/BFb0049431","volume-title":"Algorithms - ESA \u201994","author":"W. Plandowski","year":"1994","unstructured":"Plandowski, W.: Testing equivalence of morphisms on context-free languages. In: van Leeuwen, J. (ed.) ESA 1994. LNCS, vol.\u00a0855, pp. 460\u2013470. Springer, Heidelberg (1994)"},{"issue":"8","key":"11_CR21","doi-asserted-by":"publisher","first-page":"739","DOI":"10.1007\/s002360050068","volume":"33","author":"T. Reps","year":"1996","unstructured":"Reps, T.: On the sequential nature of interprocedural program-analysis problems. Acta Informatica\u00a033(8), 739\u2013757 (1996)","journal-title":"Acta Informatica"},{"key":"11_CR22","series-title":"Lecture Notes in Computer Science","volume-title":"Static Analysis","author":"E. Rodriguez-Carbonell","year":"2004","unstructured":"Rodriguez-Carbonell, E., Kapur, D.: An abstract interpretation approach for automatic generation of polynomial invariants. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, Springer, Heidelberg (2004)"},{"key":"11_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/3-540-48294-6_15","volume-title":"Static Analysis","author":"O. R\u00fcthing","year":"1999","unstructured":"R\u00fcthing, O., Knoop, J., Steffen, B.: Detecting equalities of variables: Combining efficiency with precision. In: Cortesi, A., Fil\u00e9, G. (eds.) SAS 1999. LNCS, vol.\u00a01694, pp. 232\u2013247. Springer, Heidelberg (1999)"},{"key":"11_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45614-7_1","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"N. Shankar","year":"2002","unstructured":"Shankar, N.: Little engines of proof. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 1\u201320. Springer, Heidelberg (2002)"},{"key":"11_CR25","first-page":"189","volume-title":"Program Flow Analysis: Theory and Applications","author":"M. Sharir","year":"1981","unstructured":"Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Program Flow Analysis: Theory and Applications, pp. 189\u2013233. Prentice-Hall, Englewood Cliffs (1981)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-21"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73595-3_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T05:53:00Z","timestamp":1619502780000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73595-3_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540735946","9783540735953"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73595-3_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}