article

Data-driven precondition inference with learned features

Authors:

Todd MillsteinAuthors Info & Claims

ACM SIGPLAN Notices, Volume 51, Issue 6

Pages 42 - 56

https://doi.org/10.1145/2980983.2908099

Published: 02 June 2016 Publication History

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.

References

[1]

A. Albarghouthi, S. Gulwani, and Z. Kincaid. Recursive program synthesis. In Computer Aided Verification - 25th International Conference, pages 934–950, 2013.

[2]

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.

Digital Library

[3]

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.

Digital Library

[4]

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.

Digital Library

[5]

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.

Digital Library

[6]

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.

[7]

C. Cortes and V. Vapnik. Support-vector networks. Machine Learning, 20(3):273–297, 1995.

[8]

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.

Digital Library

[9]

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.

Digital Library

[10]

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.

Digital Library

[11]

E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, New Jersey, 1976.

Digital Library

[12]

I. Dillig and T. Dillig. Explain: A tool for performing abductive inference. In Computer Aided Verification - 25th International Conference, pages 684–689. Springer, 2013.

[13]

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.

Digital Library

[14]

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.

Digital Library

[15]

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.

[16]

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.

Digital Library

[17]

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.

Digital Library

[18]

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.

[19]

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.

Digital Library

[20]

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.

Digital Library

[21]

T. Gehr, D. Dimitrov, and M. T. Vechev. Learning commutativity specifications. In Computer Aided Verification - 27th International Conference, pages 307–323, 2015.

[22]

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.

Digital Library

[23]

R. Giacobazzi. Abductive analysis of modular logic programs. Journal of Logic and Computation, 8(4):457–483, 1998.

[24]

D. Gopan and T. W. Reps. Guided static analysis. In Static Analysis, 14th International Symposium, pages 349– 365, 2007.

Digital Library

[25]

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.

Digital Library

[26]

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.

Digital Library

[27]

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.

Digital Library

[28]

D. Jackson. Software Abstractions: Logic, Language, and Analysis. MIT Press, 2006.

Digital Library

[29]

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.

Digital Library

[30]

M. Kawaguchi, S. K. Lahiri, and H. Rebelo. Conditional equivalence. Technical Report MSR-TR-2010-119, Microsoft Research, October 2010.

[31]

M. J. Kearns and U. V. Vazirani. An Introduction to Computational Learning Theory. The MIT Press, Cambridge, Massachusetts, 1994.

Digital Library

[32]

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.

Digital Library

[33]

S. Krishna, C. Puhrsch, and T. Wies. Learning invariants using decision trees. CoRR, abs/1501.04725, 2015.

[34]

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.

[35]

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.

Digital Library

[36]

L. Mauborgne and X. Rival. Trace partitioning in abstract interpretation based static analyzers. In European Symposium on Programming, 2005.

Digital Library

[37]

Y. Moy. Sufficient preconditions for modular assertion checking. In Verification, Model Checking, and Abstract Interpretation, 9th International Conference, pages 188–202, 2008.

Digital Library

[38]

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.

Digital Library

[39]

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.

Digital Library

[40]

J. R. Quinlan. Induction of decision trees. Machine Learning, 1(1):81–106, 1986.

[41]

S. Sankaranarayanan, F. Ivancic, I. Shlyakhter, and A. Gupta. Static analysis in disjunctive numerical domains. In Static Analysis Symposium, pages 3–17, 2006.

Digital Library

[42]

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.

Digital Library

[43]

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.

Digital Library

[44]

M. N. Seghir and D. Kroening. Counterexample-guided precondition inference. In 22nd European Symposium on Programming, pages 451–471, 2013.

Digital Library

[45]

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.

[46]

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.

Digital Library

[47]

R. Sharma, A. V. Nori, and A. Aiken. Interpolants as classifiers. In Computer Aided Verification - 24th International Conference, pages 71–87, 2012.

Digital Library

[48]

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.

[49]

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.

Digital Library

[50]

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.

Digital Library

[51]

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.

Digital Library

[52]

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.

Digital Library

Cited By

Wu GCao WYao YWei HChen TMa XFilkov VRay BZhou M(2024)LLM Meets Bounded Model Checking: Neuro-symbolic Loop Invariant InferenceProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695014(406-417)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695014
Dinella ELahiri SNaik Md'Amorim M(2024)Inferring Natural Preconditions via Program TransformationCompanion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering10.1145/3663529.3663865(657-658)Online publication date: 10-Jul-2024
https://dl.acm.org/doi/10.1145/3663529.3663865
Sellami YGirol GRecoules FCouroussé DBardin S(2024)Inference of Robust Reachability ConstraintsProceedings of the ACM on Programming Languages10.1145/36329338:POPL(2731-2760)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632933
Show More Cited By

Index Terms

Data-driven precondition inference with learned features

Recommendations

Data-driven precondition inference with learned features
PLDI '16: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation

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 ...
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 Three

This 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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 51, Issue 6

PLDI '16

June 2016

726 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2980983

Editor:
Andy Gill
University of Kansas, Lawrence, KS

Issue’s Table of Contents

PLDI '16: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation
June 2016
726 pages
ISBN:9781450342612
DOI:10.1145/2908080
General Chair:
Chandra Krintz
University of California at Santa Barbara, USA
,
Program Chair:
Emery Berger
University of Massachusetts at Amherst, USA

Copyright © 2016 ACM.

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 the author(s) 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

Published: 02 June 2016

Published in SIGPLAN Volume 51, Issue 6

Check for updates

Author Tags

Qualifiers

Article

Funding Sources

NSF

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

94
Total Citations
View Citations
896
Total Downloads

Downloads (Last 12 months)106
Downloads (Last 6 weeks)20

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Wu GCao WYao YWei HChen TMa XFilkov VRay BZhou M(2024)LLM Meets Bounded Model Checking: Neuro-symbolic Loop Invariant InferenceProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695014(406-417)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695014
Dinella ELahiri SNaik Md'Amorim M(2024)Inferring Natural Preconditions via Program TransformationCompanion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering10.1145/3663529.3663865(657-658)Online publication date: 10-Jul-2024
https://dl.acm.org/doi/10.1145/3663529.3663865
Sellami YGirol GRecoules FCouroussé DBardin S(2024)Inference of Robust Reachability ConstraintsProceedings of the ACM on Programming Languages10.1145/36329338:POPL(2731-2760)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632933
Wen CCao JSu JXu ZQin SHe MLi HCheung STian C(2024)Enchanting Program Specification Synthesis by Large Language Models Using Static Analysis and Program VerificationComputer Aided Verification10.1007/978-3-031-65630-9_16(302-328)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65630-9_16
Luo ZSi X(2024)Chronosymbolic Learning: Efficient CHC Solving with Symbolic Reasoning and Inductive LearningAI Verification10.1007/978-3-031-65112-0_1(1-28)Online publication date: 22-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65112-0_1
Sumanth Prabhu SFedyukovich GD’Souza D(2024)Maximal Quantified Precondition Synthesis for Linear Array LoopsProgramming Languages and Systems10.1007/978-3-031-57267-8_10(245-274)Online publication date: 5-Apr-2024
https://doi.org/10.1007/978-3-031-57267-8_10
Sumanth Prabhu SD’Souza DChakraborty SVenkatesh RFedyukovich G(2024)Weakest Precondition Inference for Non-Deterministic Linear Array ProgramsTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57249-4_9(175-195)Online publication date: 5-Apr-2024
https://doi.org/10.1007/978-3-031-57249-4_9
Takhar GRoy S(2023)SR-SFLL: Structurally Robust Stripped Functionality Logic LockingComputer Aided Verification10.1007/978-3-031-37709-9_10(190-212)Online publication date: 17-Jul-2023
https://doi.org/10.1007/978-3-031-37709-9_10
Wang JWang C(2022)Learning to Synthesize Relational InvariantsProceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering10.1145/3551349.3556942(1-12)Online publication date: 10-Oct-2022
https://dl.acm.org/doi/10.1145/3551349.3556942
Riley DFedyukovich GRoychoudhury ACadar CKim M(2022)Multi-phase invariant synthesisProceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3540250.3549166(607-619)Online publication date: 7-Nov-2022
https://dl.acm.org/doi/10.1145/3540250.3549166
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents