Document Open Access Logo

Inductive Predicate Synthesis Modulo Programs

Authors Scott Wesley , Maria Christakis , Jorge A. Navas , Richard Trefler , Valentin Wüstholz, Arie Gurfinkel

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2024.43.pdf
  • Filesize: 1.18 MB
  • 30 pages

Document Identifiers

Author Details

Scott Wesley
  • Dalhousie University, Halifax, Canada
Maria Christakis
  • TU Wien, Austria
Jorge A. Navas
  • Certora, Seattle, WA, USA
Richard Trefler
  • University of Waterloo, Canada
Valentin Wüstholz
  • ConsenSys, Vienna, Austria
Arie Gurfinkel
  • University of Waterloo, Canada

Funding

  • Christakis, Maria: supported by the Vienna Science and Technology Fund (WWTF) and the City of Vienna [Grant ID: 10.47379/ICT22007].
  • Trefler, Richard: supported, in part, by a Discovery Grant (Individual) from the Natural Sciences and Engineering Research Council of Canada.
  • Gurfinkel, Arie: supported, in part, by a Discovery Grant (Individual) from the Natural Sciences and Engineering Research Council of Canada.

Cite AsGet BibTex

Scott Wesley, Maria Christakis, Jorge A. Navas, Richard Trefler, Valentin Wüstholz, and Arie Gurfinkel. Inductive Predicate Synthesis Modulo Programs. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 43:1-43:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ECOOP.2024.43

Abstract

A growing trend in program analysis is to encode verification conditions within the language of the input program. This simplifies the design of analysis tools by utilizing off-the-shelf verifiers, but makes communication with the underlying solver more challenging. Essentially, the analysis tools operates at the level of input programs, whereas the solver operates at the level of problem encodings. To bridge this gap, the verifier must pass along proof-rules from the analysis tool to the solver. For example, an analysis tool for concurrent programs built on an inductive program verifier might need to declare Owicki-Gries style proof-rules for the underlying solver. Each such proof-rule further specifies how a program should be verified, meaning that the problem of passing proof-rules is a form of invariant synthesis. Similarly, many program analysis tasks reduce to the synthesis of pure, loop-free Boolean functions (i.e., predicates), relative to a program. From this observation, we propose Inductive Predicate Synthesis Modulo Programs (IPS-MP) which extends high-level languages with minimal synthesis features to guide analysis. In IPS-MP, unknown predicates appear under assume and assert statements, acting as specifications modulo the program semantics. Existing synthesis solvers are inefficient at IPS-MP as they target more general problems. In this paper, we show that IPS-MP admits an efficient solution in the Boolean case, despite being generally undecidable. Moreover, we show that IPS-MP reduces to the satisfiability of constrained Horn clauses, which is less general than existing synthesis problems, yet expressive enough to encode verification tasks. We provide reductions from challenging verification tasks - such as parameterized model checking - to IPS-MP. We realize these reductions with an efficient IPS-MP-solver based on SeaHorn, and describe a real-world application to smart-contract verification.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software verification
Keywords
  • Software Verification
  • Invariant Synthesis
  • Model-Checking

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. Aneesh Aggarwal and Keith H. Randall. Related field analysis. In PLDI, pages 214-220. ACM, 2001. Google Scholar
  2. Aws Albarghouthi, Isil Dillig, and Arie Gurfinkel. Maximal specification synthesis. In POPL, pages 789-801. ACM, 2016. Google Scholar
  3. Aws Albarghouthi, Yi Li, Arie Gurfinkel, and Marsha Chechik. Ufo: A framework for abstraction- and interpolation-based software verification. In CAV, volume 7358 of LNCS, pages 672-678. Springer Berlin Heidelberg, 2012. Google Scholar
  4. Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, and Albert Rubio. SAFEVM: a safety verifier for Ethereum smart contracts. In ISSTA, pages 386-389. ACM, 2019. Google Scholar
  5. Rajeev Alur, Rastislav Bodík, Eric Dallal, Dana Fisman, Pranav Garg, Garvit Juniwal, Hadas Kress-Gazit, P. Madhusudan, Milo M. K. Martin, Mukund Raghothaman, Shambwaditya Saha, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. Syntax-guided synthesis. In Maximilian Irlbeck, Doron A. Peled, and Alexander Pretschner, editors, Dependable Software Systems Engineering, volume 40 of NATO Science for Peace and Security Series, D: Information and Communication Security, pages 1-25. IOS Press, 2015. Google Scholar
  6. Rajeev Alur, Ahmed Bouajjani, and Javier Esparza. Model checking procedural programs. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 541-572. Springer Cham, 2018. Google Scholar
  7. Rajeev Alur, Dana Fisman, Rishabh Singh, and Armando Solar-Lezama. SyGuS-Comp 2016: Results and analysis. In SYNT@CAV, volume 229 of EPTCS, pages 178-202, 2016. Google Scholar
  8. Thomas Ball and Sriram K. Rajamani. Bebop: A path-sensitive interprocedural dataflow engine. In PASTE, pages 97-103. ACM, 2001. Google Scholar
  9. Jiri Barnat, Lubos Brim, Milan Češka, and Petr Ročkai. DiVinE: Parallel distributed model checker. In PDMC-HIBI, pages 4-7. IEEE, 2010. Google Scholar
  10. Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In FMCO, volume 4111 of LNCS, pages 364-387. Springer Berlin Heidelberg, 2005. Google Scholar
  11. Clark W. Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, and Cesare Tinelli. CVC4. In CAV, volume 6806 of LNCS, pages 171-177. Springer Berlin Heidelberg, 2011. Google Scholar
  12. Clark W. Barrett and Cesare Tinelli. Satisfiability modulo theories. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 305-343. Springer Cham, 2018. Google Scholar
  13. Sahil Bhatia, Sumer Kohli, Sanjit A. Seshia, and Alvin Cheung. Building code transpilers for domain-specific languages using program synthesis. In ECOOP, volume 263 of LIPIcs, pages 38:1-38:30. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. Google Scholar
  14. Nikolaj Bjørner, Arie Gurfinkel, Kenneth L. McMillan, and Andrey Rybalchenko. Horn clause solvers for program verification. In Fields of Logic and Computation II, volume 9300 of LNCS, pages 24-51. Springer Berlin Heidelberg, 2015. Google Scholar
  15. Roderick Bloem, Swen Jacobs, and Yakir Vizel. Efficient information-flow verification under speculative execution. In ATVA, pages 499-514. Springer Cham, 2019. Google Scholar
  16. James Bornholt, Emina Torlak, Dan Grossman, and Luis Ceze. Optimizing synthesis with Metasketches. In POPL, pages 775-788. ACM, 2016. Google Scholar
  17. Sagar Chaki and Arie Gurfinkel. BDD-based symbolic model checking. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 219-245. Springer Cham, 2018. Google Scholar
  18. Nishanth Chandran, Divya Gupta, Aseem Rastogi, Rahul Sharma, and Shardul Tripathi. EzPC: Programmable and efficient secure two-party computation for machine learning. In EuroS&P, pages 496-511. IEEE, 2019. Google Scholar
  19. K. Mani Chandy and Jayadev Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1989. Google Scholar
  20. Patrick Cousot, Radhia Cousot, and Francesco Logozzo. A parametric segmentation functor for fully automatic and scalable array content analysis. In POPL, pages 105-118. ACM, 2011. Google Scholar
  21. Ankush Das, Shuvendu K. Lahiri, Akash Lal, and Yi Li. Angelic verification: Precise verification modulo unknowns. In CAV, volume 9206 of LNCS, pages 324-342. Springer Berlin Heidelberg, 2015. Google Scholar
  22. Giorgio Delzanno and Andreas Podelski. Model checking in CLP. In TACAS, volume 1579 of LNCS, pages 223-239. Springer Berlin Heidelberg, 1999. Google Scholar
  23. Edsger Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM, 18(8):453-457, 1975. Google Scholar
  24. Michael D. Ernst. Dynamically Discovering Likely Program Invariants. PhD thesis, University of Washington, USA, 2002. Google Scholar
  25. Grigory Fedyukovich, Samuel J. Kaufman, and Rastislav Bodík. Sampling invariants from frequency distributions. In FMCAD, pages 100-107. IEEE, 2017. Google Scholar
  26. Jean-Christophe Filliâtre and Andrei Paskevich. Why3 - Where programs meet provers. In ESOP, volume 7792 of LNCS, pages 125-128. Springer Berlin Heidelberg, 2013. Google Scholar
  27. Pranav Garg, Christof Löding, P. Madhusudan, and Daniel Neider. ICE: A robust framework for learning invariants. In CAV, volume 8559 of LNCS, pages 69-87. Springer Berlin Heidelberg, 2014. Google Scholar
  28. Jeffrey Gennari, Arie Gurfinkel, Temesghen Kahsai, Jorge A. Navas, and Edward J. Schwartz. Executable counterexamples in software model checking. In VSTTE, volume 11294 of LNCS, pages 17-37. Springer, 2018. Google Scholar
  29. Denis Gopan, Thomas W. Reps, and Shmuel Sagiv. A framework for numeric analysis of array operations. In POPL, pages 338-350. ACM, 2005. Google Scholar
  30. Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko. Synthesizing software verifiers from proof rules. In PLDI, pages 405-416. ACM, 2012. Google Scholar
  31. Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A. Navas. The SeaHorn verification framework. In CAV, volume 9206 of LNCS, pages 343-361. Springer Berlin Heidelberg, 2015. Google Scholar
  32. Arie Gurfinkel and Jorge A. Navas. Abstract interpretation of LLVM with a region-based memory model. In Roderick Bloem, Rayna Dimitrova, Chuchu Fan, and Natasha Sharygina, editors, Software Verification, volume 13124 of LNCS, pages 122-144. Springer, 2022. Google Scholar
  33. Nicolas Halbwachs and Mathias Péron. Discovering properties about arrays in simple programs. In PLDI, pages 339-348. ACM, 2008. Google Scholar
  34. Hossein Hojjat and Philipp Rümmer. The ELDARICA Horn solver. In FMCAD, pages 1-7. IEEE, 2018. Google Scholar
  35. Kangjing Huang, Xiaokang Qiu, Peiyuan Shen, and Yanjun Wang. Reconciling enumerative and deductive program synthesis. In PLDI, pages 1159-1174. ACM, 2020. Google Scholar
  36. Kees Huizing and Ruurd Kuiper. Verification of object oriented programs using class invariants. In FASE, volume 1783 of LNCS, pages 208-221. Springer Berlin Heidelberg, 2000. Google Scholar
  37. Joxan Jaffar and Jean-Louis Lassez. Constraint logic programming. In POPL, pages 111-119. ACM, 1987. Google Scholar
  38. Joxan Jaffar, Andrew E. Santosa, and Razvan Voicu. A CLP proof method for timed automata. In RTSS, pages 175-186. IEEE Computer Society, 2004. Google Scholar
  39. Temesghen Kahsai, Rody Kersten, Philipp Rümmer, and Martin Schäf. Quantified heap invariants for object-oriented programs. In LPAR, volume 46 of EPiC Series in Computing, pages 368-384. EasyChair, 2017. Google Scholar
  40. Sukrit Kalra, Seep Goel, Mohan Dhawan, and Subodh Sharma. ZEUS: analyzing safety of smart contracts. In NDSS. The Internet Society, 2018. Google Scholar
  41. Jinwoo Kim, Qinheping Hu, Loris D'Antoni, and Thomas W. Reps. Semantics-Guided Synthesis. Proc. ACM Program. Lang., 5(POPL):1-32, 2021. Google Scholar
  42. Anvesh Komuravelli, Arie Gurfinkel, and Sagar Chaki. SMT-based model checking for recursive programs. In CAV, volume 8559 of LNCS, pages 17-34. Springer Berlin Heidelberg, 2014. Google Scholar
  43. Jakub Kuderski, Jorge A. Navas, and Arie Gurfinkel. Unification-based pointer analysis without oversharing. In FMCAD, pages 37-45. IEEE, 2019. Google Scholar
  44. Jérôme Leroux, Philipp Rümmer, and Pavle Subotic. Guiding Craig interpolation with domain-specific abstractions. Acta Informatica, 53(4):387-424, 2016. Google Scholar
  45. Francesco Logozzo. Automatic inference of class invariants. In VMCAI, volume 2937 of LNCS, pages 211-222. Springer Berlin Heidelberg, 2004. Google Scholar
  46. Sirui Lu and Rastislav Bodík. Grisette: Symbolic compilation as a functional programming library. Proc. ACM Program. Lang., 7(POPL), 2023. Google Scholar
  47. Kenneth McMillan. Interpolation and SAT-based model checking. In CAV, volume 2725 of LNCS, pages 1-13. Springer Berlin Heidelberg, 2003. Google Scholar
  48. Marvin Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, 1967. Google Scholar
  49. Kedar S. Namjoshi and Richard J. Trefler. Parameterized compositional model checking. In TACAS, volume 9636 of LNCS, pages 589-606. Springer Berlin Heidelberg, 2016. Google Scholar
  50. Hanne Riis Nielson and Flemming Nielson. Semantics with Applications: An Appetizer. Undergraduate Topics in Computer Science. Springer, 2007. Google Scholar
  51. Julio C. Peralta, John P. Gallagher, and Hüseyin Saglam. Analysis of imperative programs through analysis of constraint logic programs. In SAS, volume 1503 of LNCS, pages 246-261. Springer Berlin Heidelberg, 1998. Google Scholar
  52. Anton Permenev, Dimitar Dimitrov, Petar Tsankov, Dana Drachsler-Cohen, and Martin Vechev. VerX: Safety verification of smart contracts. In S&P, pages 1661-1677. IEEE, 2020. Google Scholar
  53. Sumanth Prabhu, Grigory Fedyukovich, Kumar Madhukar, and Deepak D'Souza. Specification synthesis with constrained Horn clauses. In PLDI, pages 1203-1217. ACM, 2021. Google Scholar
  54. Zvonimir Rakamarić and Michael Emmi. SMACK: Decoupling source language details from verifier implementations. In CAV, volume 8559 of LNCS, pages 106-113. Springer Cham, 2014. Google Scholar
  55. Dan Rasin, Orna Grumberg, and Sharon Shoham. Modular verification of concurrent programs via sequential model checking. In ATVA, pages 228-247. Springer Cham, 2018. Google Scholar
  56. Heinz Riener and Görschwin Fey. FAuST: A framework for formal verification, automated debugging, and software test generation. In SPIN, volume 13872 of LNCS, pages 234-240. Springer Berlin Heidelberg, 2012. Google Scholar
  57. Gabriel Ryan, Justin Wong, Jianan Yao, Ronghui Gu, and Suman Jana. CLN2INV: learning loop invariants with continuous logic networks. In ICLR. OpenReview.net, 2020. Google Scholar
  58. Malte Hermann Schwerhoff. Advancing Automated, Permission-Based Program Verification Using Symbolic Execution. PhD thesis, ETH Zurich, Switzerland, 2016. Google Scholar
  59. Xujie Si, Aaditya Naik, Hanjun Dai, Mayur Naik, and Le Song. Code2Inv: A deep learning framework for program verification. In CAV, volume 12225 of LNCS, pages 151-164. Springer Berlin Heidelberg, 2020. Google Scholar
  60. Carsten Sinz, Stephan Falke, and Florian Merz. A precise memory model for low-level bounded model checking. In SSV, page 7, USA, 2010. USENIX Association. Google Scholar
  61. Armando Solar-Lezama. Program sketching. Int. J. Softw. Tools Technol. Transf., 15(5-6):475-495, 2013. Google Scholar
  62. Armando Solar-Lezama, Christopher Grant Jones, and Rastislav Bodik. Sketching concurrent data structures. In PLDI, pages 136-148. ACM, 2008. Google Scholar
  63. Emina Torlak and Rastislav Bodík. A lightweight symbolic virtual machine for solver-aided host languages. In PLDI, pages 530-541. ACM, 2014. Google Scholar
  64. Moshe Y. Vardi. From verification to synthesis. In VSTTE, volume 5295 of LNCS, page 2. Springer Berlin Heidelberg, 2008. Google Scholar
  65. Hari Govind VK, Yuting Chen, Sharon Shoham, and Arie Gurfinkel. Global guidance for local generalization in model checking. In Shuvendu K. Lahiri and Chao Wang, editors, CAV, volume 12225 of LNCS, pages 101-125. Springer Berlin Heidelberg, 2020. Google Scholar
  66. Scott Wesley, Maria Christakis, Jorge A. Navas, Richard Trefler, Valentin Wüstholz, and Arie Gurfinkel. Compositional verification of smart contracts through communication abstraction. In Static Analysis, volume 12913 of LNCS, pages 429-452. Springer Berlin Heidelberg, 2021. Google Scholar
  67. Scott Wesley, Maria Christakis, Jorge A. Navas, Richard Trefler, Valentin Wüstholz, and Arie Gurfinkel. Verifying Solidity smart contracts via communication abstraction in SmartACE. In VMCAI, pages 425-449. Springer Cham, 2022. Google Scholar
  68. Scott Wesley, Maria Christakis, Jorge A. Navas, Richard Trefler, Valentin Wüstholz, and Arie Gurfinkel. Inductive predicate synthesis modulo programs (extended), 2024. Google Scholar
  69. Jianan Yao, Gabriel Ryan, Justin Wong, Suman Jana, and Ronghui Gu. Learning nonlinear loop invariants with gated continuous logic networks. In PLDI, pages 106-120. ACM, 2020. Google Scholar
  70. Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh, Suman Jana, and Gabriel Ryan. DistAI: Data-driven automated invariant learning for distributed protocols. In OSDI, pages 405-421. USENIX Association, 2021. Google Scholar
  71. He Zhu, Stephen Magill, and Suresh Jagannathan. A data-driven CHC solver. In PLDI, pages 707-721. ACM, 2018. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact