Thomas Reps
Mooly Sagiv
Skip Abstract Section
Skip Supplemental Material SectionAbstract
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.
Supplemental Material
Available for Download
pdf
a24-reps-apndx.pdf (118.5 KB)
Online appendix to finite differencing of logical formulas for static analysis on article 24.
- Akers, Jr., S. 1959. On a theory of Boolean functions. J. Soc. Indust. Appl. Math. 7, 4, 487--498.Google Scholar
Cross Ref
- 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. Google ScholarDigital Library
- Ball, T. and Rajamani, S. 2001. Automatically validating temporal safety properties of interfaces. In Proceedings of the SPIN Workshop. 103--122. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Boerger, E. and Staerk, R. 2003. Abstract State Machines: A Method for High-Level System Design and Analysis. Springer. Google ScholarDigital Library
- 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.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Cousot, P. 2003. Verification by abstract interpretation. In Verification: Theory and Practice. 243--268.Google Scholar
- 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. Google ScholarDigital Library
- Cousot, P. and Cousot, R. 1979. Systematic design of program analysis frameworks. In Proceedings of the Conference on Principles of Programming Languages. 269--282. Google ScholarDigital Library
- Das, S., Dill, D., and Park, S. 1999. Experience with predicate abstraction. In Proceedings of the Conference on Computer-Aided Verification. 160--171. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Dong, G. and Su, J. 1995. Incremental and decremental evaluation of transitive closure by first-order queries. Inform. Comput. 120, 101--106. Google ScholarDigital Library
- Dong, G. and Su, J. 2000. Incremental maintenance of recursive views using relational calculus/SQL. SIGMOD Rec. 29, 1, 44--51. Google ScholarDigital Library
- Dor, N., Rodeh, M., and Sagiv, M. 2000. Checking cleanness in linked lists. In Proceedings of the Static Analysis Symposium. 115--134. Google ScholarDigital Library
- Goldstine, H. 1977. A History of Numerical Analysis. Springer.Google Scholar
- 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.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Gupta, A. and Mumick, I., Eds. 1999. Materialized Views: Techniques, Implementations, and Applications. MIT Press, Cambridge, MA. Google ScholarDigital Library
- Henzinger, T., Jhala, R., Majumdar, R., and Sutre, G. 2002. Lazy abstraction. In Proceedings of the Conference on Principles of Programming Languages. 58--70. Google ScholarDigital Library
- Hesse, W. 2003. Dynamic computational complexity. Ph.D. thesis, Department of Computer Science, University of Massachusetts, Amherst, MA. Google ScholarDigital Library
- 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.Google Scholar
- 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. Google ScholarDigital Library
- Jackson, D. 2006. Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge, MA. Google ScholarDigital Library
- 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.Google Scholar
- Jeannet, B., Loginov, A., Reps, T., and Sagiv, M. 2010. A relational approach to interprocedural shape analysis. Trans. Program. Lang. Syst. 32, 2. Google ScholarDigital Library
- Klarlund, N. and Schwartzbach, M. 1993. Graph types. In Proceedings of the Conference on Principles of Programming Languages. 196--205. Google ScholarDigital Library
- Kurshan, R. 1994. Computer-Aided Verification of Coordinating Processes. Princeton University Press. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Lev-Ami, T. and Sagiv, M. 2000. TVLA: A system for implementing static analyses. In Proceedings of the Static Analysis Symposium. 280--301. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Liu, Y. and Teitelbaum, T. 1995. Systematic derivation of incremental programs. Sci. Comput. Program. 24, 2, 1--39. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Loginov, A., Reps, T., and Sagiv, M. 2005. Abstraction refinement via inductive learning. In Proceedings of the Conference on Computer-Aided Verification. 519--533. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Malmkjær, K. 1993. Abstract interpretation of partial-evaluation algorithms. Ph.D. thesis, Department of Computer and Information Science, Kansas State University, Manhattan, KS.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Michie, D. 1968. Memo functions and machine learning. Nature 218, 19--22.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- Mycroft, A. and Jones, N. 1985. A relational framework for abstract interpretation. In Programs as Data Objects. 156--171. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Nelson, G. 1983. Verifying reachability invariants of linked structures. In Proceedings of the Conference on Principles of Programming Languages. 38--47. Google ScholarDigital Library
- Nielson, F. 1989. Two-level semantics and abstract interpretation. Theor. Comput. Sci. 69, 2, 117--242. Google ScholarDigital Library
- Paige, R. and Koenig, S. 1982. Finite differencing of computable expressions. Trans. Program. Lang. Syst. 4, 3, 402--454. Google ScholarDigital Library
- Patnaik, S. and Immerman, N. 1997. Dyn-FO: A parallel, dynamic complexity class. J. Comput. Syst. Sci. 55, 2, 199--209. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google Scholar
- 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.Google Scholar
- Reynolds, J. 2002. Separation logic: A logic for shared mutable data structures. In Proceedings of the Conference on Logic in Computer Science. 55--74. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Rinetzky, N. and Sagiv, M. 2001. Interprocedural shape analysis for recursive programs. In Proceedings of the Conference on Compiler Construction. 133--149. Google ScholarDigital Library
- Sagiv, M., Reps, T., and Wilhelm, R. 2002. Parametric shape analysis via 3-valued logic. Trans. Program. Lang. Syst. 24, 3, 217--298. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Sharir, M. 1982. Some observations concerning formal differentiation of set theoretic expressions. Trans. Program. Lang. Syst. 4, 2, 196--225. Google ScholarDigital Library
- TVLA. TVLA system. www.cs.tau.ac.il/~tvla/.Google Scholar
- van Fraassen, B. 1966. Singular terms, truth-value gaps, and free logic. J. Phil. 63, 17, 481--495.Google ScholarCross Ref
- 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.Google Scholar
- Yorsh, G., Reps, T., Sagiv, M., and Wilhelm, R. 2007. Logical characterizations of heap abstractions. Trans. Comput. Logic 8, 1. Google ScholarDigital Library
Index Terms
- Finite differencing of logical formulas for static analysis
Recommendations
A relational approach to interprocedural shape analysis
This article addresses the verification of properties of imperative programs with recursive procedure calls, heap-allocated storage, and destructive updating of pointer-valued fields, that is, interprocedural shape analysis. The article makes three ...
Parametric shape analysis via 3-valued logic
Shape analysis concerns the problem of determining "shape invariants" for programs that perform destructive updating on dynamically allocated storage. This article presents a parametric framework for shape analysis that can be instantiated in different ...
Pushdown control-flow analysis for free
POPL '16Traditional control-flow analysis (CFA) for higher-order languages introduces spurious connections between callers and callees, and different invocations of a function may pollute each other's return flows. Recently, three distinct approaches have been ...
Comments