P. Ezudheen
Skip Abstract Section
Skip Supplemental Material SectionAbstract
We design learning algorithms for synthesizing invariants using Horn implication counterexamples (Horn-ICE), extending the ICE-learning model. In particular, we describe a decision-tree learning algorithm that learns from nonlinear Horn-ICE samples, works in polynomial time, and uses statistical heuristics to learn small trees that satisfy the samples. Since most verification proofs can be modeled using nonlinear Horn clauses, Horn-ICE learning is a more robust technique to learn inductive annotations that prove programs correct. Our experiments show that an implementation of our algorithm is able to learn adequate inductive invariants and contracts efficiently for a variety of sequential and concurrent programs.
Supplemental Material
- Thomas Ball, Rupak Majumdar, Todd D. Millstein, and Sriram K. Rajamani. 2001. Automatic Predicate Abstraction of C Programs. In PLDI, 2001. 203–213. Google Scholar
Digital Library
- Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. 2005. Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In FMCO 2005 (LNCS), Vol. 4111. Springer, 364–387. Google ScholarDigital Library
- Adam Betts, Nathan Chong, Alastair F. Donaldson, Shaz Qadeer, and Paul Thomson. 2012. GP UVerify: a verifier for GP U kernels. In OOPSLA 2012. ACM, 113–132. Google ScholarDigital Library
- Tewodros A. Beyene, Corneliu Popeea, and Andrey Rybalchenko. 2013. Solving Existentially Quantified Horn Clauses. In CAV 2013 (LNCS). Springer, 869–882.Google Scholar
- Dirk Beyer. 2017. Software Verification with Validation of Results - (Report on SV-COMP 2017). In TACAS 2017 (LNCS), Vol. 10206. 331–349. Google ScholarDigital Library
- Nikolaj Bjørner, Kenneth L. McMillan, and Andrey Rybalchenko. 2013. On Solving Universally Quantified Horn Clauses. In SAS 2013. 105–125.Google Scholar
- Aaron R. Bradley. 2011. SAT-Based Model Checking without Unrolling. In VMCAI 2011 (LNCS), Vol. 6538. Springer, 70–87. Google ScholarDigital Library
- Marc Brockschmidt, Yuxin Chen, Pushmeet Kohli, Siddharth Krishna, and Daniel Tarlow. 2017. Learning Shape Analysis. In SAS 2017. 66–87.Google Scholar
- Adrien Champion, Tomoya Chiba, Naoki Kobayashi, and Ryosuke Sato. 2018. ICE-Based Refinement Type Discovery for Higher-Order Functional Programs. In Proc. TACAS 2018, Thessaloniki, Greece, April 14-20, 2018 (LNCS), Vol. 10805. Springer, 365–384.Google ScholarCross Ref
- Nathan Chong, Alastair F. Donaldson, Paul H. J. Kelly, Jeroen Ketema, and Shaz Qadeer. 2013. Barrier invariants: a shared state abstraction for the analysis of data-dependent GP U kernels. In Proc. OOPSLA 2013, Indianapolis, USA, October 26-31, 2013. ACM, 605–622. Google ScholarDigital Library
- Michael Colón, Sriram Sankaranarayanan, and Henny Sipma. 2003. Linear Invariant Generation Using Non-linear Constraint Solving. In CAV 2003 (LNCS), Vol. 2725. Springer, 420–432.Google Scholar
- Patrick Cousot and Radhia Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In POPL 1977. ACM Press, 238–252. Google ScholarDigital Library
- Leonardo Mendonça de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In TACAS 2008 (LNCS), Vol. 4963. Springer, 337–340.Google ScholarCross Ref
- Isil Dillig, Thomas Dillig, Boyang Li, and Kenneth L. McMillan. 2013. Inductive invariant generation via abductive inference. In Object Oriented Programming Systems Languages & Applications, OOPSLA 2013. 443–456. Google ScholarDigital Library
- William F. Dowling and Jean H. Gallier. 1984. Linear-Time Algorithms for Testing the Satisfiability of Propositional Horn Formulae. J. Log. Program. 1, 3 (1984), 267–284.Google ScholarCross Ref
- Michael D. Ernst, Adam Czeisler, William G. Griswold, and David Notkin. 2000. Quickly detecting relevant program invariants. In ICSE 2000. ACM Press, 449–458. Google ScholarDigital Library
- Grigory Fedyukovich, Samuel J Kaufman, and Rastislav Bodik. 2017. Sampling Invariants from Frequency Distributions. (2017).Google Scholar
- Cormac Flanagan and K. Rustan M. Leino. 2001. Houdini, an Annotation Assistant for ESC/Java. In FME 2001 (LNCS), Vol. 2021. Springer, 500–517. Google ScholarDigital Library
- Pranav Garg, Christof Löding, P. Madhusudan, and Daniel Neider. 2013. Learning Universally Quantified Invariants of Linear Data Structures. In CAV 2013 (LNCS), Vol. 8044. Springer, 813–829.Google Scholar
- Pranav Garg, Christof Löding, P. Madhusudan, and Daniel Neider. 2014. ICE: A Robust Framework for Learning Invariants. In CAV 2014 (LNCS), Vol. 8559. Springer, 69–87. Google ScholarDigital Library
- Pranav Garg, Daniel Neider, P. Madhusudan, and Dan Roth. 2016. Learning invariants using decision trees and implication counterexamples. In POPL 2016. ACM, 499–512. Google ScholarDigital Library
- Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko. 2012. Synthesizing software verifiers from proof rules. In PLDI 2012. ACM, 405–416. Google ScholarDigital Library
- Sumit Gulwani, Saurabh Srivastava, and Ramarathnam Venkatesan. 2008. Program analysis as constraint solving. In PLDI 2008. ACM, 281–292. Google ScholarDigital Library
- Ashutosh Gupta and Andrey Rybalchenko. 2009. InvGen: An Efficient Invariant Generator. In CAV 2009 (LNCS), Vol. 5643. Springer, 634–640. Google ScholarDigital Library
- Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A. Navas. 2015. The SeaHorn Verification Framework. In CAV 2015 (LNCS), Vol. 9206. Springer, 343–361.Google Scholar
- Matthias Heizmann, Jürgen Christ, Daniel Dietsch, Evren Ermis, Jochen Hoenicke, Markus Lindenmann, Alexander Nutz, Christian Schilling, and Andreas Podelski. 2013. Ultimate Automizer with SMTInterpol. In Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’13). Springer-Verlag, Berlin, Heidelberg, 641–643. Google ScholarDigital Library
- Krystof Hoder and Nikolaj Bjørner. 2012. Generalized Property Directed Reachability. In SAT 2012 (LNCS), Vol. 7317. Springer, 157–171. Google ScholarDigital Library
- Ranjit Jhala and Kenneth L. McMillan. 2006. A Practical and Complete Approach to Predicate Refinement. In TACAS 2006 (LNCS), Vol. 3920. Springer, 459–473. Google ScholarDigital Library
- C. B. Jones. 1983. Tentative Steps Toward a Development Method for Interfering Programs. Transactions on Programming Languages and System 5, 4 (1983), 596–619. Google ScholarDigital Library
- Aleksandr Karbyshev, Nikolaj Bjørner, Shachar Itzhaky, Noam Rinetzky, and Sharon Shoham. 2015. Property-Directed Inference of Universal Invariants or Proving Their Absence. In CAV 2015 (LNCS), Vol. 9206. Springer, 583–602.Google ScholarCross Ref
- Kenneth L. McMillan. 2003. Interpolation and SAT-Based Model Checking. In CAV 2003 (LNCS), Vol. 2725. Springer, 1–13.Google Scholar
- Antoine Miné. 2014. Relational Thread-Modular Static Value Analysis by Abstract Interpretation. In VMCAI 2014 (LNCS), Vol. 8318. Springer, 39–58. Google ScholarDigital Library
- Antoine Miné. 2014. Relational thread-modular static value analysis by abstract interpretation. In International Conference on Verification, Model Checking, and Abstract Interpretation. Springer, 39–58. Google ScholarDigital Library
- Daniel Neider, Pranav Garg, P Madhusudan, Shambwaditya Saha, and Daejun Park. 2018. Invariant Synthesis for Incomplete Verification Engines. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 232–250.Google Scholar
- ThanhVu Nguyen, Deepak Kapur, Westley Weimer, and Stephanie Forrest. 2012. Using dynamic analysis to discover polynomial and array invariants. In ICSE 2012. IEEE, 683–693. Google ScholarDigital Library
- Susan Owicki and David Gries. 1976. Verifying properties of parallel programs: An axiomatic approach. Commun. ACM 19, 5 (1976), 279–285. Google ScholarDigital Library
- Saswat Padhi, Rahul Sharma, and Todd D. Millstein. 2016. Data-driven precondition inference with learned features. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016. 42–56. Google ScholarDigital Library
- Zvonimir Pavlinovic, Akash Lal, and Rahul Sharma. 2016. Inferring annotations for device drivers from verification histories. In Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, ASE 2016. 450–460. Google ScholarDigital Library
- J. Ross Quinlan. 1986. Induction of Decision Trees. Machine Learning 1, 1 (1986), 81–106. Google ScholarCross Ref
- Rahul Sharma and Alex Aiken. 2014. From Invariant Checking to Invariant Inference Using Randomized Search. In CAV 2014 (LNCS), Vol. 8559. Springer, 88–105. Google ScholarDigital Library
- Rahul Sharma, Saurabh Gupta, Bharath Hariharan, Alex Aiken, Percy Liang, and Aditya V. Nori. 2013b. A Data Driven Approach for Algebraic Loop Invariants. In ESOP 2013 (LNCS), Vol. 7792. Springer, 574–592. Google ScholarDigital Library
- Rahul Sharma, Saurabh Gupta, Bharath Hariharan, Alex Aiken, and Aditya V. Nori. 2013a. Verification as Learning Geometric Concepts. In SAS 2013 (LNCS), Vol. 7935. 388–411.Google Scholar
- Rahul Sharma, Aditya V. Nori, and Alex Aiken. 2012. Interpolants as Classifiers. In CAV 2012 (LNCS), Vol. 7358. Springer, 71–87. Google ScholarDigital Library
- Yakir Vizel, Arie Gurfinkel, Sharon Shoham, and Sharad Malik. 2017. IC3 - Flipping the E in ICE. In VMCAI 2017 (LNCS), Vol. 10145. Springer, 521–538.Google ScholarCross Ref
- Qiwen Xu, Willem P. de Roever, and Jifeng He. 1997. The Rely-Guarantee Method for Verifying Shared Variable Concurrent Programs. Formal Asp. Comput. 9, 2 (1997), 149–174.Google ScholarCross Ref
- He Zhu, Stephen Magill, and Suresh Jagannathan. 2018. A data-driven CHC solver. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018. ACM, 707–721. Google ScholarDigital Library
- He Zhu, Aditya V. Nori, and Suresh Jagannathan. 2015. Learning Refinement Types. In ICFP 2015. ACM, 400–411. Google ScholarDigital Library
- He Zhu, Gustavo Petri, and Suresh Jagannathan. 2016. Automatically Learning Shape Specifications. In PLDI (2016). ACM, New York, NY, USA, 491–507. Google ScholarDigital Library
Index Terms
- Horn-ICE learning for synthesizing invariants and contracts
Recommendations
Learning invariants using decision trees and implication counterexamples
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesInductive invariants can be robustly synthesized using a learning model where the teacher is a program verifier who instructs the learner through concrete program configurations, classified as positive, negative, and implications. We propose the first ...
Learning invariants using decision trees and implication counterexamples
POPL '16Inductive invariants can be robustly synthesized using a learning model where the teacher is a program verifier who instructs the learner through concrete program configurations, classified as positive, negative, and implications. We propose the first ...
Higher-order constrained horn clauses for verification
Motivated by applications in automated verification of higher-order functional programs, we develop a notion of constrained Horn clauses in higher-order logic and a decision problem concerning their satisfiability. We show that, although satisfiable ...
Comments