ABSTRACT
Program invariants are important for defect detection, program verification, and program repair. However, existing techniques have limited support for important classes of invariants such as disjunctions, which express the semantics of conditional statements. We propose a method for generating disjunctive invariants over numerical domains, which are inexpressible using classical convex polyhedra. Using dynamic analysis and reformulating the problem in non-standard ``max-plus'' and ``min-plus'' algebras, our method constructs hulls over program trace points. Critically, we introduce and infer a weak class of such invariants that balances expressive power against the computational cost of generating nonconvex shapes in high dimensions.
Existing dynamic inference techniques often generate spurious invariants that fit some program traces but do not generalize. With the insight that generating dynamic invariants is easy, we propose to verify these invariants statically using k-inductive SMT theorem proving which allows us to validate invariants that are not classically inductive.
Results on difficult kernels involving nonlinear arithmetic and abstract arrays suggest that this hybrid approach efficiently generates and proves correct program invariants.
- X. Allamigeon, S. Gaubert, and É. Goubault. Inferring min and max invariants using max-plus polyhedra. In Static Analysis, pages 189–204. Springer, 2008. Google ScholarDigital Library
- X. Allamigeon and R. D. Katz. Minimal external representations of tropical polyhedra. Journal of Combinatorial Theory, Series A, 120(4):907–940, 2013. Google ScholarDigital Library
- T. Ball and S. K. Rajamani. Automatically validating temporal safety properties of interfaces. In SPIN Workshop on Model Checking of Software, pages 103–122, May 2001. Google ScholarDigital Library
- B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. A static analyzer for large safety-critical software. In Programming Languages Design and Implementation, pages 196–207, 2003. Google ScholarDigital Library
- E. R. Carbonell. Automatic Generation of Polynomial Invariants for System Verification. PhD thesis, Technical University of Catalonia (UPC), Barcelona, 2006.Google Scholar
- E. R. Carbonell and D. Kapur. Generating all polynomial invariants in simple loops. Journal of Symbolic Computation, 42(4):443–476, 2007. Google ScholarDigital Library
- J.-P. Comet. Application of max-plus algebra to biological sequence comparisons. Theoretical computer science, 293(1):189–217, 2003. Google ScholarDigital Library
- P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Principles of Programming Languages, pages 238–252, 1977. Google ScholarDigital Library
- P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. The Astrée analyzer. In European Symposium on Programming, pages 21–30, 2005.Google ScholarDigital Library
- P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. The Astrée analyzer. In Proc. of The European Symposium on Programming (ESOP’05), volume 3444 of Lecture Notes in Computer Science (LNCS), pages 21–30. Springer, Apr. 2005.Google ScholarDigital Library
- P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Principles of Programming Languages, pages 84–96, 1978. Google ScholarDigital Library
- M. Daniel-Cavalcante, M. F. Magalhaes, and R. Santos-Mendes. The max-plus algebra and the network calculus. In Discrete Event Systems, 2006 8th International Workshop on, pages 433–438. IEEE, 2006.Google Scholar
- M. Das, S. Lerner, and M. Seigle. ESP: path-sensitive program verification in polynomial time. SIGPLAN Notices, 37(5):57–68, 2002. Google ScholarDigital Library
- L. De Moura and N. Bjørner. Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems, pages 337–340. Springer, 2008. http://research.microsoft.com/en-us/um/ redmond/projects/z3/.Google ScholarDigital Library
- D. L. Detlefs, K. R. M. Leino, G. Nelson, and J. B. Saxe. Extended static checking. 1998.Google Scholar
- E. W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Communication ACM, 18:453–457, 1975. Google ScholarDigital Library
- A. F. Donaldson, L. Haller, D. Kroening, and P. Rümmer. Software verification using k-induction. In Static Analysis Symposium, pages 351–368, 2011. Google ScholarDigital Library
- M. D. Ernst, W. G. Griswold, Y. Kataoka, and D. Notkin. Dynamically discovering program invariants involving collections. University of Washington, TR UW-CSE-99-11-02, 2000.Google Scholar
- M. D. Ernst, J. H. Perkins, P. J. Guo, S. McCamant, C. Pacheco, M. S. Tschantz, and C. Xiao. The Daikon system for dynamic detection of likely invariants. Science of Computer Programming, 2007. Google ScholarDigital Library
- S. Gulwani. Program verification as probabilistic inference. In Principles of Programming Languages, pages 277–289. ACM, 2007. Google ScholarDigital Library
- B. Heidergott and J. W. van der Woude. Max Plus at work: modeling and analysis of synchronized systems: a course on Max-Plus algebra and its applications, volume 13. Princeton University Press, 2006.Google Scholar
- T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In Principles of Programming Languages, pages 58–70, 2002. Google ScholarDigital Library
- B. Jeannet. Interproc analyzer for recursive programs with numerical variables. INRIA, software and documentation are available at the following URL: http://pop-art. inrialpes. fr/interproc/interprocweb. cgi. Last accessed, pages 06–11, 2010.Google Scholar
- D. Jovanovi´ c and L. De Moura. Solving non-linear arithmetic. In Automated Reasoning, pages 339–354. Springer, 2012. Google ScholarDigital Library
- T. Kahsai, Y. Ge, and C. Tinelli. Instantiation-based invariant discovery. In NASA Formal Methods, pages 192–206. Springer, 2011. Google ScholarDigital Library
- T. Kahsai and C. Tinelli. PKIND: a parallel k-induction based model checker. In J. Barnat and K. Heljanko, editors, Proceedings of 10th International Workshop on Parallel and Distributed Methods in verifiCation (Snowbird, Utah, USA), Electronic Proceedings in Theoretical Computer Science, pages 55–62, 2011.Google Scholar
- D. Kapur, Z. Zhang, M. Horbach, H. Zhao, Q. Lu, and T. Nguyen. Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants. In M. Bonacina and M. Stickel, editors, Automated Reasoning and Mathematics: Essays in Memory of William W. McCune, volume 7788 of Lecture Notes in Computer Science, pages 189–228. Springer, 2013. Google ScholarDigital Library
- K. R. M. Leino. This is Boogie 2. Manuscript KRML, 178, 2008.Google Scholar
- X. Leroy. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In Principles of Programming Languages, pages 42–54, 2006. Google ScholarDigital Library
- A. Miné. Weakly relational numerical abstract domains. PhD thesis, PhD thesis, École Polytechnique, Palaiseau, France, 2004.Google Scholar
- T. Nguyen, D. Kapur, W. Weimer, and S. Forrest. Using Dynamic Analysis to Discover Polynomial and Array Invariants. In International Conference on Software Engineering, pages 683–693. IEEE, 2012. Google ScholarDigital Library
- T. Nguyen, D. Kapur, W. Weimer, and S. Forrest. DIG: A Dynamic Invariant Generator for Polynomial and Array Invariants. ACM Transactions on Software Engineering and Methodology, to appear, 2014.Google Scholar
- J. W. Nimmer and M. D. Ernst. Static verification of dynamically detected program invariants: Integrating Daikon and ESC/Java. Electr. Notes Theor. Comput. Sci., 55(2):255–276, 2001.Google ScholarCross Ref
- J. W. Nimmer and M. D. Ernst. Automatic generation of program specifications. In International Symposium on Software Testing and Analysis, pages 232–242, Rome, Italy, Jul 2002. Google ScholarDigital Library
- P. Nuzzo, A. Puggelli, S. A. Seshia, and A. Sangiovanni-Vincentelli. CalCS: SMT solving for non-linear convex constraints. In Formal Methods in Computer-Aided Design, pages 71–80, 2010. Google ScholarDigital Library
- C. Popeea and W.-N. Chin. Inferring disjunctive postconditions. In Advances in Computer Science-ASIAN 2006. Secure Software and Related Issues, pages 331–345. Springer, 2007. Google ScholarDigital Library
- E. Rodr´ıguez-Carbonell and D. Kapur. Automatic generation of polynomial invariants of bounded degree using abstract interpretation, volume 64. Elsevier North-Holland, Inc., Amsterdam, 2007.Google ScholarDigital Library
- S. Sankaranarayanan, F. Ivanˇ ci´ c, I. Shlyakhter, and A. Gupta. Static analysis in disjunctive numerical domains. In Static Analysis, pages 3–17. Springer, 2006. Google ScholarDigital Library
- R. Sharma, S. Gupta, B. Hariharan, A. Aiken, and A. V. Nori. Verification as learning geometric concepts. In Static Analysis, pages 388–411. Springer, 2013.Google Scholar
- M. Sheeran, S. Singh, and G. St˚ almarck. Checking safety properties using induction and a sat-solver. In Formal Methods in Computer-Aided Design, pages 127–144. Springer, 2000. Google ScholarDigital Library
- W. Stein et al. Sage Mathematics Software, 2012. http://www.sagemath.org.Google Scholar
- Y. Wei, Y. Pei, C. A. Furia, L. S. Silva, S. Buchholz, B. Meyer, and A. Zeller. Automated fixing of programs with contracts. In International Symposium on Software Testing and Analysis, pages 61–72, 2010. Google ScholarDigital Library
- W. Weimer. Patches as better bug reports. In Generative Programming and Component Engineering, 2006. Google ScholarDigital Library
Index Terms
- Using dynamic analysis to generate disjunctive invariants
Recommendations
DIG: A Dynamic Invariant Generator for Polynomial and Array Invariants
Special Issue International Conference on Software Engineering (ICSE 2012) and Regular PapersThis article describes and evaluates DIG, a dynamic invariant generator that infers invariants from observed program traces, focusing on numerical and array variables. For numerical invariants, DIG supports both nonlinear equalities and inequalities of ...
Uniform proofs and disjunctive logic programming
LICS '95: Proceedings of the 10th Annual IEEE Symposium on Logic in Computer ScienceOne formulation of the concept of logic programming is the notion of an abstract logic programming language. Central to its definition is a uniform proof, which enforces the requirements of inference direction, including goal-directedness, and the ...
Predicate abstraction in a program logic calculus
Predicate abstraction is a form of abstract interpretation where the abstract domain is constructed from a finite set of predicates over the variables of the program. This paper explores a way to integrate predicate abstraction into a calculus for ...
Comments