SpringerLink
Log in

Solving Constrained Horn Clauses over Algebraic Data Types

  • Conference paper
  • First Online:
Verification, Model Checking, and Abstract Interpretation (VMCAI 2023)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 13881))

  • 517 Accesses

Abstract

Safety verification problems are often reduced to solving the satisfiability of Constrained Horn Clauses (CHCs), a set of constraints in first-order logic involving uninterpreted predicates. Synthesis of interpretations for the predicates, also known as inductive invariants synthesis, is challenging in the presence of Algebraic Data Types (ADTs). Defined inductively, ADTs describe possibly unbounded chunks of data, thus they often require synthesizing recursive invariants. We present a novel approach to this problem based on functional synthesis: it attempts to extract recursive functions from constraints that capture the semantics of unbounded computation over the chunks of data encoded in CHCs. Recursive function calls are beneficial since they allow rewriting the constraints and introducing equalities that further can be simplified away. This largely simplifies the problem of generating invariants and lets them have simple interpretations that are recursion-free at the highest level and have function calls. We have implemented the approach in a new CHC solver called AdtChc. Our algorithm relies on an external automated theorem prover to conduct proofs by structural induction, as opposed to a black-box constrained solver. With two alternative solvers of choice, AdtInd and Vampire, the new toolset has been evaluated on a range of public benchmarks, and it exhibited its strengths against state-of-the-art CHC solvers on particular benchmarks that require recursive invariants.

The second author is currently employed at JetBrains N.V., The Netherlands.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 64.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 84.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    Although it is conventional in practice to compute the length and the sum in different traversals, it is not necessarily more efficient to do it this way. Also, combining traversals might be needed in verification purposes, see e.g. [42].

  2. 2.

    version 2.0.6.

  3. 3.

    https://github.com/hiroshi-unno/coar.

  4. 4.

    https://github.com/hgvk94/z3/tree/racer.

References

  1. Alur, R., et al.: Syntax-guided synthesis. In: FMCAD, pp. 1–17. IEEE (2013)

    Google Scholar 

  2. Bakhirkin, A., Monniaux, D.: Combining forward and backward abstract interpretation of horn clauses. In: Ranzato, F. (ed.) SAS 2017. LNCS, vol. 10422, pp. 23–45. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66706-5_2

    Chapter  Google Scholar 

  3. Barrett, C., Shikanian, I., Tinelli, C.: An abstract decision procedure for a theory of inductive data types. J. Satisfiability, Boolean Model. Comput. 3, 21–46 (2007)

    Article  MathSciNet  Google Scholar 

  4. Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_14

    Chapter  Google Scholar 

  5. Beyene, T.A., Popeea, C., Rybalchenko, A.: Solving existentially quantified horn clauses. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 869–882. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_61

    Chapter  Google Scholar 

  6. Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70–87. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-18275-4_7

    Chapter  Google Scholar 

  7. Champion, A., Chiba, T., Kobayashi, N., Sato, R.: ICE-based refinement type discovery for higher-order functional programs. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 365–384. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89960-2_20

    Chapter  Google Scholar 

  8. Champion, A., Kobayashi, N., Sato, R.: HoIce: an ICE-based non-linear horn clause solver. In: Ryu, S. (ed.) APLAS 2018. LNCS, vol. 11275, pp. 146–156. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-02768-1_8

    Chapter  Google Scholar 

  9. Chen, Y.-F., Hsieh, C., Tsai, M.-H., Wang, B.-Y., Wang, F.: Verifying recursive programs using intraprocedural analyzers. In: Müller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol. 8723, pp. 118–133. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10936-7_8

    Chapter  Google Scholar 

  10. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000). https://doi.org/10.1007/10722167_15

    Chapter  Google Scholar 

  11. De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Solving horn clauses on inductive data types without induction. TPLP 18(3–4), 452–469 (2018)

    MathSciNet  Google Scholar 

  12. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  13. Dietsch, D., Heizmann, M., Hoenicke, J., Nutz, A., Podelski, A.: Ultimate TreeAutomizer. In: HCVS/PERR, vol. 296 of EPTCS, pp. 42–47 (2019)

    Google Scholar 

  14. Eén, N., Mishchenko, A., Brayton, R.K.: Efficient implementation of property directed reachability. In: FMCAD, pp. 125–134. IEEE (2011)

    Google Scholar 

  15. Fedyukovich, G., Ahmad, M.B.S., Bodík, R.: Gradual synthesis for static parallelization of single-pass array-processing programs. In: PLDI, pp. 572–585. ACM (2017)

    Google Scholar 

  16. Fedyukovich, G., Ernst, G.: Bridging arrays and ADTs in recursive proofs. In: TACAS 2021. LNCS, vol. 12652, pp. 24–42. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-72013-1_2

    Chapter  Google Scholar 

  17. Garoche, P., Gurfinkel, A., Kahsai, T.: Synthesizing modular invariants for synchronous code. In: HCVS, vol. 169 of EPTCS, pp. 19–30 (2014)

    Google Scholar 

  18. Garoche, P. Kahsai, T., Thirioux, X.: Hierarchical state machines as modular horn clauses. In: HCVS, vol. 219 of EPTCS, pp. 15–28 (2016)

    Google Scholar 

  19. Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI, pp. 405–416. ACM (2012)

    Google Scholar 

  20. Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The seahorn verification framework. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343–361. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_20

    Chapter  Google Scholar 

  21. Hoare, C.A.R.: Recursive data structures. Int. J. Parallel Program. 4(2), 105–132 (1975)

    Google Scholar 

  22. Hojjat, H., Konečný, F., Garnier, F., Iosif, R., Kuncak, V., Rümmer, P.: A verification toolkit for numerical transition systems. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 247–251. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32759-9_21

    Chapter  Google Scholar 

  23. Hojjat, H., Rümmer, P.: Deciding and interpolating algebraic data types by reduction. In: SYNASC, pp. 145–152. IEEE (2017)

    Google Scholar 

  24. Hojjat, H., Rümmer, P.: The ELDARICA horn solver. In: FMCAD, pp. 158–164. IEEE (2018)

    Google Scholar 

  25. Hojjat, H., Rümmer, P., Shamakhi, A.: On strings in software model checking. In: Lin, A.W. (ed.) APLAS 2019. LNCS, vol. 11893, pp. 19–30. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-34175-6_2

    Chapter  Google Scholar 

  26. Ireland, A., Bundy, A.: Productive use of failure in inductive proof. In: Zhang, H. (ed.) Automated Mathematical Induction, pp. 79–111. Springer, Cham (1996). https://doi.org/10.1007/978-94-009-1675-3_3

    Chapter  Google Scholar 

  27. Hari Govind, V.K., Shoham, S., Gurfinkel, A.: Solving constrained horn clauses modulo algebraic data types and recursive functions. Proc. ACM Program. Lang. 6(POPL), 1–29 (2022)

    Google Scholar 

  28. Kafle, B., Gallagher, J.P., Ganty, P.: Solving non-linear Horn clauses using a linear Horn clause solver. In: HCVS, vol. 219 of EPTCS, pp. 33–48 (2016)

    Google Scholar 

  29. Kafle, B., Gallagher, J.P., Morales, J.F.: Rahft: a tool for verifying horn clauses using abstract interpretation and finite tree automata. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 261–268. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41528-4_14

    Chapter  Google Scholar 

  30. Kahsai, T., Kersten, R., Rümmer, P., Schäf, M.: Quantified heap invariants for object-oriented programs. In: LPAR, vol. 46 of EPiC Series in Computing, pp. 368–384. EasyChair (2017)

    Google Scholar 

  31. Kahsai, T., Rümmer, P., Sanchez, H., Schäf, M.: JayHorn: a framework for verifying java programs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 352–358. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41528-4_19

    Chapter  Google Scholar 

  32. Kim, J., Hu, Q., D’Antoni, L., Reps, T.: Semantics-guided synthesis. Proc. ACM on Program. Lang. 5(POPL), 1–32 (2021)

    Google Scholar 

  33. Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: ACM, pp. 222–233. ACM (2011)

    Google Scholar 

  34. Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 17–34. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_2

    Chapter  Google Scholar 

  35. Kostyukov, Y., Mordvinov, D., Fedyukovich, G.: Beyond the elementary representations of program invariants over algebraic data types. In: PLDI, pp. 451–465 (2021)

    Google Scholar 

  36. Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1–35. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_1

    Chapter  Google Scholar 

  37. Vediramana Krishnan, H.G., Chen, Y.T., Shoham, S., Gurfinkel, A.: Global guidance for local generalization in model checking. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 101–125. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53291-8_7

    Chapter  Google Scholar 

  38. Krishnan, H.G.V., Fedyukovich, G., Gurfinkel, A.: Word level property directed reachability. In: ICCAD, pp. 1–9. IEEE (2020)

    Google Scholar 

  39. Matsushita, Y., Tsukada, T., Kobayashi, N.: RustHorn: CHC-based verification for rust programs. In: ESOP 2020. LNCS, vol. 12075, pp. 484–514. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-44914-8_18

    Chapter  Google Scholar 

  40. McMillan, K.L.: Lazy annotation revisited. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 243–259. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_16

    Chapter  Google Scholar 

  41. McMillan, K.L., Rybalchenko, A.: Solving constrained Horn clauses using interpolation. In Technical report MSR-TR-2013-6 (2013)

    Google Scholar 

  42. Mordvinov, D., Fedyukovich, G.: Synchronizing constrained horn clauses. In: LPAR, vol. 46 of EPiC Series in Computing, pp. 338–355. EasyChair (2017)

    Google Scholar 

  43. Mordvinov, D., Fedyukovich, G.: Verifying safety of functional programs with rosette/unbound. CoRR, abs/1704.04558 (2017). https://github.com/dvvrd/rosette

  44. Mordvinov, D., Fedyukovich, G.: Property directed inference of relational invariants. In: FMCAD, pp. 152–160. IEEE (2019)

    Google Scholar 

  45. Oppen, D.C.: Reasoning about recursively defined data structures. J. ACM (JACM) 27(3), 403–411 (1980)

    Article  MathSciNet  Google Scholar 

  46. Pham, T., Gacek, A., Whalen, M.W.: Reasoning about algebraic data types with abstractions. J. Autom. Reason. 57(4), 281–318 (2016)

    Article  MathSciNet  Google Scholar 

  47. Reynolds, A., Blanchette, J.C.: A decision procedure for (co) datatypes in SMT solvers. J. Autom. Reason. 58(3), 341–362 (2017)

    Article  MathSciNet  Google Scholar 

  48. Reynolds, A., Kuncak, V.: Induction for SMT solvers. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 80–98. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46081-8_5

    Chapter  Google Scholar 

  49. Rümmer, P.: A constraint sequent calculus for first-order logic with linear integer arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 274–289. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89439-1_20

    Chapter  Google Scholar 

  50. Fedyukovich, G., Rümmer, P.: Competition report: CHC-COMP-21. In: Hojjat, H., Kafle, B. (eds.) Proceedings 8th Workshop on Horn Clauses for Verification and Synthesis, HCVS@ETAPS 2021, Virtual, 28th March 2021. EPTCS, vol. 344, pp. 91–108 (2021). https://doi.org/10.4204/EPTCS.344.7

  51. Rümmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolants for horn-clause verification. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 347–363. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_24

    Chapter  Google Scholar 

  52. Satake, Y., Unno, H., Yanagi, H.: Probabilistic inference for predicate constraint satisfaction. In: AAAI, pp. 1644–1651. AAAI Press (2020)

    Google Scholar 

  53. Sharma, R., Aiken, A.: From invariant checking to invariant inference using randomized search. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 88–105. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_6

    Chapter  Google Scholar 

  54. Solar-Lezama, A., Tancau, L., Bodík, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: ASPLOS, pp. 404–415. ACM (2006)

    Google Scholar 

  55. Suter, P., Dotta, M., Kuncak, V.: Decision procedures for algebraic data types with abstractions. ACM Sigplan Not. 45(1), 199–210 (2010)

    Article  Google Scholar 

  56. Suter, P., Köksal, A.S., Kuncak, V.: Satisfiability modulo recursive programs. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 298–315. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-23702-7_23

    Chapter  Google Scholar 

  57. Unno, H., Terauchi, T.: Inferring simple solutions to recursion-free horn clauses via sampling. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 149–163. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_10

    Chapter  Google Scholar 

  58. Unno, H., Torii, S., Sakamoto, H.: Automating induction for solving horn clauses. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 571–591. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63390-9_30

    Chapter  Google Scholar 

  59. Yang, W., Fedyukovich, G., Gupta, A.: Lemma synthesis for automating induction over algebraic data types. In: Schiex, T., de Givry, S. (eds.) CP 2019. LNCS, vol. 11802, pp. 600–617. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30048-7_35

    Chapter  Google Scholar 

  60. Zhang, T., Sipma, H.B., Manna, Z.: Decision procedures for recursive data structures with integer constraints. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 152–167. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-25984-8_9

    Chapter  Google Scholar 

  61. Zhu, H., Magill, S., Jagannathan, S.: A data-driven CHC solver. In: PLDI, pp. 707–721. ACM (2018)

    Google Scholar 

Download references

Acknowledgments

The work is supported in parts by a gift from Amazon Web Services.

Author information

Authors and Affiliations

  1. Florida State University, Tallahassee, FL, USA

    Lucas Zavalía, Lidiia Chernigovskaia & Grigory Fedyukovich

Authors
  1. Lucas Zavalía
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Lidiia Chernigovskaia
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Grigory Fedyukovich
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Grigory Fedyukovich .

Editor information

Editors and Affiliations

  1. Inria, Amazon Web Services, Courbevoie, France

    Cezara Dragoi

  2. Amazon Web Services, Seattle, WA, USA

    Michael Emmi

  3. University of Southern California, Los Angeles, CA, USA

    **gbo Wang

Rights and permissions

Reprints and permissions

Copyright information

© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Zavalía, L., Chernigovskaia, L., Fedyukovich, G. (2023). Solving Constrained Horn Clauses over Algebraic Data Types. In: Dragoi, C., Emmi, M., Wang, J. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2023. Lecture Notes in Computer Science, vol 13881. Springer, Cham. https://doi.org/10.1007/978-3-031-24950-1_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-24950-1_16

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-24949-5

  • Online ISBN: 978-3-031-24950-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation