Saswat Padhi
Rahul Sharma
Todd Millstein
ABSTRACT
We extend the data-driven approach to inferring preconditions for code from a set of test executions. Prior work requires a fixed set of features, atomic predicates that define the search space of possible preconditions, to be specified in advance. In contrast, we introduce a technique for on-demand feature learning, which automatically expands the search space of candidate preconditions in a targeted manner as necessary. We have instantiated our approach in a tool called PIE. In addition to making precondition inference more expressive, we show how to apply our feature-learning technique to the setting of data-driven loop invariant inference. We evaluate our approach by using PIE to infer rich preconditions for black-box OCaml library functions and using our loop-invariant inference algorithm as part of an automatic program verifier for C++ programs.
- A. Albarghouthi, S. Gulwani, and Z. Kincaid. Recursive program synthesis. In Computer Aided Verification - 25th International Conference, pages 934–950, 2013.Google Scholar
- C. Calcagno, D. Distefano, P. W. O’Hearn, and H. Yang. Compositional shape analysis by means of bi-abduction. Journal of the ACM, 58(6), 2011. Google ScholarDigital Library
- S. Chandra, S. J. Fink, and M. Sridharan. Snugglebug: A powerful approach to weakest preconditions. In Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 363–374, 2009. Google ScholarDigital Library
- A. Cheung, A. Solar-Lezama, and S. Madden. Using program synthesis for social recommendations. In 21st ACM International Conference on Information and Knowledge Management, pages 1732–1736, 2012. Google ScholarDigital Library
- E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In Computer Aided Verification - 12th International Conference, pages 154–169, 2000. Google ScholarDigital Library
- M. Colón, S. Sankaranarayanan, and H. Sipma. Linear invariant generation using non-linear constraint solving. In Computer Aided Verification - 15th International Conference, pages 420–432, 2003.Google Scholar
- C. Cortes and V. Vapnik. Support-vector networks. Machine Learning, 20(3):273–297, 1995. 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 Fourth ACM Symposium on Principles of Programming Languages, pages 238–252, 1977. Google ScholarDigital Library
- P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Fifth Annual ACM Symposium on Principles of Programming Languages, pages 84–96, 1978. Google ScholarDigital Library
- P. Cousot, R. Cousot, M. Fähndrich, and F. Logozzo. Automatic inference of necessary preconditions. In Verification, Model Checking, and Abstract Interpretation - 14th International Conference, pages 128–148, 2013. Google ScholarDigital Library
- E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, New Jersey, 1976.Google ScholarDigital Library
- I. Dillig and T. Dillig. Explain: A tool for performing abductive inference. In Computer Aided Verification - 25th International Conference, pages 684–689. Springer, 2013.Google Scholar
- I. Dillig, T. Dillig, B. Li, and K. L. McMillan. Inductive invariant generation via abductive inference. In Proceedings of the 2013 ACM SIGPLAN International Conference on Object-Oriented Programming Systems Languages & Applications, pages 443–456, 2013. Google ScholarDigital Library
- 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. Sci. Comput. Program., 69(1-3):35–45, 2007. Google ScholarDigital Library
- M. Fähndrich and F. Logozzo. Static contract checking with abstract interpretation. In Formal Verification of Object-Oriented Software - International Conference, pages 10–30, 2010.Google Scholar
- J. K. Feser, S. Chaudhuri, and I. Dillig. Synthesizing data structure transformations from input-output examples. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 229–239, 2015. Google ScholarDigital Library
- G. Filé and F. Ranzato. Improving abstract interpretations by systematic lifting to the powerset. In Logic Programming, Proceedings of the 1994 International Symposium, pages 655–669, 1994. Google ScholarDigital Library
- J. P. Galeotti, C. A. Furia, E. May, G. Fraser, and A. Zeller. Dynamate: Dynamically inferring loop invariants for automatic full functional verification. In Hardware and Software: Verification and Testing - 10th International Haifa Verification Conference, pages 48–53, 2014.Google Scholar
- P. Garg, C. Löding, P. Madhusudan, and D. Neider. ICE: A robust framework for learning invariants. In Computer Aided Verification - 26th International Conference, pages 69–87, 2014. Google ScholarDigital Library
- P. Garg, D. Neider, P. Madhusudan, and D. Roth. Learning invariants using decision trees and implication counterexamples. In Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 499–512, 2016. Google ScholarDigital Library
- T. Gehr, D. Dimitrov, and M. T. Vechev. Learning commutativity specifications. In Computer Aided Verification - 27th International Conference, pages 307–323, 2015.Google Scholar
- K. Ghorbal, F. Ivancic, G. Balakrishnan, N. Maeda, and A. Gupta. Donut domains: Efficient non-convex domains for abstract interpretation. In Verification, Model Checking, and Abstract Interpretation - 13th International Conference, pages 235–250, 2012. Google ScholarDigital Library
- R. Giacobazzi. Abductive analysis of modular logic programs. Journal of Logic and Computation, 8(4):457–483, 1998.Google ScholarCross Ref
- D. Gopan and T. W. Reps. Guided static analysis. In Static Analysis, 14th International Symposium, pages 349– 365, 2007. Google ScholarDigital Library
- S. Gulwani and N. Jojic. Program verification as probabilistic inference. In Proceedings of the 34th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, pages 277–289, 2007. Google ScholarDigital Library
- S. Gulwani, S. Srivastava, and R. Venkatesan. Program analysis as constraint solving. In Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, pages 281–292, 2008. Google ScholarDigital Library
- A. Gupta, R. Majumdar, and A. Rybalchenko. From tests to proofs. In Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, pages 262–276, 2009. Google ScholarDigital Library
- D. Jackson. Software Abstractions: Logic, Language, and Analysis. MIT Press, 2006. Google ScholarDigital Library
- Y. Jung, S. Kong, B. Wang, and K. Yi. Deriving invariants by algorithmic learning, decision procedures, and predicate abstraction. In Verification, Model Checking, and Abstract Interpretation, 11th International Conference, pages 180–196, 2010. Google ScholarDigital Library
- M. Kawaguchi, S. K. Lahiri, and H. Rebelo. Conditional equivalence. Technical Report MSR-TR-2010-119, Microsoft Research, October 2010.Google Scholar
- M. J. Kearns and U. V. Vazirani. An Introduction to Computational Learning Theory. The MIT Press, Cambridge, Massachusetts, 1994. Google ScholarDigital Library
- S. Kong, Y. Jung, C. David, B. Wang, and K. Yi. Automatically inferring quantified loop invariants by algorithmic learning from simple templates. In Programming Languages and Systems - 8th Asian Symposium, pages 328–343, 2010. Google ScholarDigital Library
- S. Krishna, C. Puhrsch, and T. Wies. Learning invariants using decision trees. CoRR, abs/1501.04725, 2015.Google Scholar
- T. Lev-Ami, M. Sagiv, T. Reps, and S. Gulwani. Backward analysis for inferring quantified preconditions. Technical Report TR-2007-12-01, Tel Aviv University, 2007.Google Scholar
- T. Liang, A. Reynolds, C. Tinelli, C. Barrett, and M. Deters. A DPLL(T) theory solver for a theory of strings and regular expressions. In Computer Aided Verification - 26th International Conference, pages 646–662, 2014. Google ScholarDigital Library
- L. Mauborgne and X. Rival. Trace partitioning in abstract interpretation based static analyzers. In European Symposium on Programming, 2005. Google ScholarDigital Library
- Y. Moy. Sufficient preconditions for modular assertion checking. In Verification, Model Checking, and Abstract Interpretation, 9th International Conference, pages 188–202, 2008. Google ScholarDigital Library
- J. W. Nimmer and M. D. Ernst. Automatic generation of program specifications. In Proceedings of the International Symposium on Software Testing and Analysis, pages 229–239, 2002. Google ScholarDigital Library
- J. W. Nimmer and M. D. Ernst. Invariant inference for static checking:. In Proceedings of the 10th ACM SIGSOFT Symposium on Foundations of Software Engineering, pages 11–20, 2002. Google ScholarDigital Library
- J. R. Quinlan. Induction of decision trees. Machine Learning, 1(1):81–106, 1986. Google ScholarCross Ref
- S. Sankaranarayanan, F. Ivancic, I. Shlyakhter, and A. Gupta. Static analysis in disjunctive numerical domains. In Static Analysis Symposium, pages 3–17, 2006. Google ScholarDigital Library
- S. Sankaranarayanan, S. Chaudhuri, F. Ivancic, and A. Gupta. Dynamic inference of likely data preconditions over predicates by tree learning. In ACM/SIGSOFT International Symposium on Software Testing and Analysis, pages 295–306, 2008. Google ScholarDigital Library
- T. W. Schiller, K. Donohue, F. Coward, and M. D. Ernst. Case studies and tools for contract specifications. In Proceedings of the 36th International Conference on Software Engineering, pages 596–607, 2014. Google ScholarDigital Library
- M. N. Seghir and D. Kroening. Counterexample-guided precondition inference. In 22nd European Symposium on Programming, pages 451–471, 2013. Google ScholarDigital Library
- M. N. Seghir and P. Schrammel. Necessary and sufficient preconditions via eager abstraction. In Programming Languages and Systems - 12th Asian Symposium, pages 236–254, 2014.Google Scholar
- R. Sharma and A. Aiken. From invariant checking to invariant inference using randomized search. In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, pages 88–105, 2014. Google ScholarDigital Library
- R. Sharma, A. V. Nori, and A. Aiken. Interpolants as classifiers. In Computer Aided Verification - 24th International Conference, pages 71–87, 2012. Google ScholarDigital Library
- R. Sharma, S. Gupta, B. Hariharan, A. Aiken, and A. V. Nori. Verification as learning geometric concepts. In Static Analysis - 20th International Symposium, pages 388–411, 2013.Google Scholar
- R. Sharma, E. Schkufza, B. R. Churchill, and A. Aiken. Conditionally correct superoptimization. In Proceedings of the 2013 ACM SIGPLAN International Conference on Object-Oriented Programming Systems Languages & Applications, pages 147–162, 2015. Google ScholarDigital Library
- A. Solar-Lezama, L. Tancau, R. Bodik, S. Seshia, and V. Saraswat. Combinatorial sketching for finite programs. In Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems, pages 404–415, 2006. Google ScholarDigital Library
- S. Srivastava, S. Gulwani, and J. S. Foster. From program verification to program synthesis. In 37th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, pages 313–326, 2010. Google ScholarDigital Library
- Y. Zheng, X. Zhang, and V. Ganesh. Z3-str: a z3-based string solver for web application analysis. In Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, pages 114–124, 2013. Google ScholarDigital Library
Index Terms
- Data-driven precondition inference with learned features
Recommendations
Data-driven precondition inference with learned features
PLDI '16We extend the data-driven approach to inferring preconditions for code from a set of test executions. Prior work requires a fixed set of features, atomic predicates that define the search space of possible preconditions, to be specified in advance. In ...
Inference with multinomial data: why to weaken the prior strength
IJCAI'11: Proceedings of the Twenty-Second international joint conference on Artificial Intelligence - Volume Volume ThreeThis paper considers inference from multinomial data and addresses the problem of choosing the strength of the Dirichlet prior under a mean-squared error criterion. We compare the Maximum Likelihood Estimator (MLE) and the most commonly used Bayesian ...
Averaged collapsed variational bayes inference
This paper presents the Averaged CVB (ACVB) inference and oers convergence-guaranteed and practically useful fast Collapsed Variational Bayes (CVB) inferences. CVB inferences yield more precise inferences of Bayesian probabilistic models than ...
Comments