skip to main content
research-article
Open access

Finite differencing of logical formulas for static analysis

Published: 13 August 2010 Publication History

Abstract

This article concerns mechanisms for maintaining the value of an instrumentation relation (also known as a derived relation or view), 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 relation-maintenance formula that captures what the instrumentation relation's new value should be. The algorithm runs in time linear in the size of the defining formula.
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.
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.

Supplementary Material

Reps Appendix (a24-reps-apndx.pdf)
Online appendix to finite differencing of logical formulas for static analysis on article 24.

References

[1]
Akers, Jr., S. 1959. On a theory of Boolean functions. J. Soc. Indust. Appl. Math. 7, 4, 487--498.
[2]
Ball, T., Majumdar, R., Millstein, T., and Rajamani, S. 2001. Automatic predicate abstraction of C programs. In Proceedings of the Conference on Programming Language Design and Implementation. 203--213.
[3]
Ball, T. and Rajamani, S. 2001. Automatically validating temporal safety properties of interfaces. In Proceedings of the SPIN Workshop. 103--122.
[4]
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.
[5]
Boerger, E. and Staerk, R. 2003. Abstract State Machines: A Method for High-Level System Design and Analysis. Springer.
[6]
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.
[7]
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.
[8]
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.
[9]
Clarke, E., Grumberg, O., Jha, S., Lu, Y., and Veith, H. 2000. Counterexample-guided abstraction refinement. In Proceedings of the Conference on Computer-Aided Verification. 154--169.
[10]
Cousot, P. 2003. Verification by abstract interpretation. In Verification: Theory and Practice. 243--268.
[11]
Cousot, P. and Cousot, R. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In Proceedings of the Conference on Principles of Programming Languages. 238--252.
[12]
Cousot, P. and Cousot, R. 1979. Systematic design of program analysis frameworks. In Proceedings of the Conference on Principles of Programming Languages. 269--282.
[13]
Das, S., Dill, D., and Park, S. 1999. Experience with predicate abstraction. In Proceedings of the Conference on Computer-Aided Verification. 160--171.
[14]
Distefano, D., O'Hearn, P., and Yang, H. 2006. A local shape analysis based on separation logic. In Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems. 287--302.
[15]
Dong, G. and Su, J. 1995. Incremental and decremental evaluation of transitive closure by first-order queries. Inform. Comput. 120, 101--106.
[16]
Dong, G. and Su, J. 2000. Incremental maintenance of recursive views using relational calculus/SQL. SIGMOD Rec. 29, 1, 44--51.
[17]
Dor, N., Rodeh, M., and Sagiv, M. 2000. Checking cleanness in linked lists. In Proceedings of the Static Analysis Symposium. 115--134.
[18]
Goldstine, H. 1977. A History of Numerical Analysis. Springer.
[19]
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.
[20]
Gopan, D., Reps, T., and Sagiv, M. 2005. A framework for numeric analysis of array operations. In Proceedings of the Conference on Principles of Programming Languages. 338--350.
[21]
Graf, S. and Saïdi, H. 1997. Construction of abstract state graphs with PVS. In Proceedings of the Conference on Computer-Aided Verification. 72--83.
[22]
Gupta, A. and Mumick, I., Eds. 1999. Materialized Views: Techniques, Implementations, and Applications. MIT Press, Cambridge, MA.
[23]
Henzinger, T., Jhala, R., Majumdar, R., and Sutre, G. 2002. Lazy abstraction. In Proceedings of the Conference on Principles of Programming Languages. 58--70.
[24]
Hesse, W. 2003. Dynamic computational complexity. Ph.D. thesis, Department of Computer Science, University of Massachusetts, Amherst, MA.
[25]
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.
[26]
Ishtiaq, S. and O'Hearn, P. 2001. BI as an assertion language for mutable data structures. In Proceedings of the Conference on Principles of Programming Languages. 14--26.
[27]
Jackson, D. 2006. Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge, MA.
[28]
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.
[29]
Jeannet, B., Loginov, A., Reps, T., and Sagiv, M. 2010. A relational approach to interprocedural shape analysis. Trans. Program. Lang. Syst. 32, 2.
[30]
Klarlund, N. and Schwartzbach, M. 1993. Graph types. In Proceedings of the Conference on Principles of Programming Languages. 196--205.
[31]
Kurshan, R. 1994. Computer-Aided Verification of Coordinating Processes. Princeton University Press.
[32]
Lahiri, S. and Qadeer, S. 2006. Verifying properties of well-founded linked lists. In Proceedings of the Conference on Principles of Programming Languages. 115--126.
[33]
Lev-Ami, T., Reps, T., Sagiv, M., and Wilhelm, R. 2000. Putting static analysis to work for verification: A case study. In Proceedings of the International Symposium on Software Testing and Analysis. 26--38.
[34]
Lev-Ami, T. and Sagiv, M. 2000. TVLA: A system for implementing static analyses. In Proceedings of the Static Analysis Symposium. 280--301.
[35]
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.
[36]
Liu, Y., Stoller, S., and Teitelbaum, T. 1996. Discovering auxiliary information for incremental computation. In Proceedings of the Conference on Principles of Programming Languages. 157--170.
[37]
Liu, Y. and Teitelbaum, T. 1995. Systematic derivation of incremental programs. Sci. Comput. Program. 24, 2, 1--39.
[38]
Loginov, A. 2006. Refinement-based program verification via three-valued-logic analysis. Ph.D. thesis, Tech. rep. 1574. Computer Science Department, University of Wisconsin, Madison, WI.
[39]
Loginov, A., Reps, T., and Sagiv, M. 2005. Abstraction refinement via inductive learning. In Proceedings of the Conference on Computer-Aided Verification. 519--533.
[40]
Loginov, A., Reps, T., and Sagiv, M. 2006. Automated verification of the Deutsch-Schorr-Waite tree-traversal algorithm. In Proceedings of the Static Analysis Symposium. 261--279.
[41]
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.
[42]
Malmkjær, K. 1993. Abstract interpretation of partial-evaluation algorithms. Ph.D. thesis, Department of Computer and Information Science, Kansas State University, Manhattan, KS.
[43]
Manevich, R., Yahav, E., Ramalingam, G., and Sagiv, M. 2005. Predicate abstraction and canonical abstraction for singly-linked lists. In Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation. 181--198.
[44]
McMillan, K. 1999. Verification of infinite state systems by compositional model checking. In Proceedings of the Conference on Correct Hardware Design and Verification Methods (CHARME'99). 219--234.
[45]
Michie, D. 1968. Memo functions and machine learning. Nature 218, 19--22.
[46]
Møller, A. and Schwartzbach, M. 2001. The pointer assertion logic engine. In Proceedings of the Conference on Programming Language Design and Implementation. 221--231.
[47]
Mycroft, A. and Jones, N. 1985. A relational framework for abstract interpretation. In Programs as Data Objects. 156--171.
[48]
Mycroft, A. and Jones, N. 1986. Data flow analysis of applicative programs using minimal function graphs. In Proceedings of the Conference on Principles of Programming Languages. 296--306.
[49]
Nelson, G. 1983. Verifying reachability invariants of linked structures. In Proceedings of the Conference on Principles of Programming Languages. 38--47.
[50]
Nielson, F. 1989. Two-level semantics and abstract interpretation. Theor. Comput. Sci. 69, 2, 117--242.
[51]
Paige, R. and Koenig, S. 1982. Finite differencing of computable expressions. Trans. Program. Lang. Syst. 4, 3, 402--454.
[52]
Patnaik, S. and Immerman, N. 1997. Dyn-FO: A parallel, dynamic complexity class. J. Comput. Syst. Sci. 55, 2, 199--209.
[53]
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.
[54]
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.
[55]
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.
[56]
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.
[57]
Reynolds, J. 2002. Separation logic: A logic for shared mutable data structures. In Proceedings of the Conference on Logic in Computer Science. 55--74.
[58]
Rinetzky, N., Bauer, J., Reps, T., Sagiv, M., and Wilhelm, R. 2005. A semantics for procedure local heaps and its abstractions. In Proceedings of the Conference on Principles of Programming Languages. 296--309.
[59]
Rinetzky, N. and Sagiv, M. 2001. Interprocedural shape analysis for recursive programs. In Proceedings of the Conference on Compiler Construction. 133--149.
[60]
Sagiv, M., Reps, T., and Wilhelm, R. 2002. Parametric shape analysis via 3-valued logic. Trans. Program. Lang. Syst. 24, 3, 217--298.
[61]
Scherpelz, E., Lerner, S., and Chambers, C. 2007. Automatic inference of optimizer flow functions from semantic meanings. In Proceedings of the Conference on Programming Language Design and Implementation. 135--145.
[62]
Sharir, M. 1982. Some observations concerning formal differentiation of set theoretic expressions. Trans. Program. Lang. Syst. 4, 2, 196--225.
[63]
TVLA. TVLA system. www.cs.tau.ac.il/~tvla/.
[64]
van Fraassen, B. 1966. Singular terms, truth-value gaps, and free logic. J. Phil. 63, 17, 481--495.
[65]
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.
[66]
Yorsh, G., Reps, T., Sagiv, M., and Wilhelm, R. 2007. Logical characterizations of heap abstractions. Trans. Comput. Logic 8, 1.

Cited By

View all
  • (2023)A General Noninterference Policy for Polynomial TimeProceedings of the ACM on Programming Languages10.1145/35712217:POPL(806-832)Online publication date: 11-Jan-2023
  • (2017)Paxos made EPR: decidable reasoning about distributed protocolsProceedings of the ACM on Programming Languages10.1145/31405681:OOPSLA(1-31)Online publication date: 12-Oct-2017
  • (2017)Bounded Quantifier Instantiation for Checking Inductive InvariantsProceedings, Part I, of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 1020510.1007/978-3-662-54577-5_5(76-95)Online publication date: 22-Apr-2017
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems
ACM Transactions on Programming Languages and Systems  Volume 32, Issue 6
August 2010
215 pages
ISSN:0164-0925
EISSN:1558-4593
DOI:10.1145/1749608
Issue’s Table of Contents
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Accepted: 01 December 2010
Published: 13 August 2010
Revised: 01 August 2009
Received: 01 March 2009
Published in TOPLAS Volume 32, Issue 6

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. 3 - valued logic
  2. Abstract interpretation
  3. finite differencing
  4. materialized view
  5. shape analysis
  6. static analysis

Qualifiers

  • Research-article
  • Research
  • Refereed

Funding Sources

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)51
  • Downloads (Last 6 weeks)12
Reflects downloads up to 14 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2023)A General Noninterference Policy for Polynomial TimeProceedings of the ACM on Programming Languages10.1145/35712217:POPL(806-832)Online publication date: 11-Jan-2023
  • (2017)Paxos made EPR: decidable reasoning about distributed protocolsProceedings of the ACM on Programming Languages10.1145/31405681:OOPSLA(1-31)Online publication date: 12-Oct-2017
  • (2017)Bounded Quantifier Instantiation for Checking Inductive InvariantsProceedings, Part I, of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 1020510.1007/978-3-662-54577-5_5(76-95)Online publication date: 22-Apr-2017
  • (2016)Automating Abstract InterpretationProceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 958310.1007/978-3-662-49122-5_1(3-40)Online publication date: 17-Jan-2016
  • (2013)Effectively-Propositional Reasoning about Reachability in Linked Data StructuresProceedings of the 25th International Conference on Computer Aided Verification - Volume 804410.5555/2958031.2958053(756-772)Online publication date: 13-Jul-2013
  • (2013)TSLACM Transactions on Programming Languages and Systems10.1145/2450136.245013935:1(1-59)Online publication date: 1-Apr-2013
  • (2013)Effectively-Propositional Reasoning about Reachability in Linked Data StructuresComputer Aided Verification10.1007/978-3-642-39799-8_53(756-772)Online publication date: 2013
  • (2013)FESAProceedings of the 22nd international conference on Compiler Construction10.1007/978-3-642-37051-9_5(82-101)Online publication date: 16-Mar-2013
  • (2011)Sound and complete abstract graph transformationProceedings of the 14th Brazilian conference on Formal Methods: foundations and Applications10.1007/978-3-642-25032-3_7(92-107)Online publication date: 26-Sep-2011

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Full Access

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media