SpringerLink
Log in

Multiple Query Satisfiability of Constrained Horn Clauses

  • Conference paper
  • First Online:
Practical Aspects of Declarative Languages (PADL 2023)

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

Included in the following conference series:

  • 350 Accesses

Abstract

We address the problem of checking the satisfiability of a set of constrained Horn clauses (CHCs) possibly including more than one query. We propose a transformation technique that takes as input a set of CHCs, including a set of queries, and returns as output a new set of CHCs, such that the transformed CHCs are satisfiable if and only if so are the original ones, and the transformed CHCs incorporate in each new query suitable information coming from the other ones so that the CHC satisfiability algorithm is able to exploit the relationships among all queries. We show that our proposed technique is effective on a non trivial benchmark of sets of CHCs that encode many verification problems for programs manipulating algebraic data types such as lists and trees.

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.

    Experiments have been performed on an Intel Xeon CPU E5-2640 2.00 GHz with 64GB RAM under CentOS with a time limit of 300 s per problem.

References

  1. Albert, E., Genaim, S., Gutiérrez, R., Martin-Martin, E.: A transformational approach to resource analysis with typed-norms inference. Theory Pract. Log. Program. 20(3), 310–357 (2020). https://doi.org/10.1017/S1471068419000401

    Article  MathSciNet  MATH  Google Scholar 

  2. Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 825–885. IOS Press (2009). https://doi.org/10.3233/978-1-58603-929-5-825

  3. Bjørner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II. LNCS, vol. 9300, pp. 24–51. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23534-9_2

    Chapter  Google Scholar 

  4. Blicha, M., Fedyukovich, G., Hyvärinen, A.E.J., Sharygina, N.: Transition power abstractions for deep counterexample detection. In: TACAS 2022. LNCS, vol. 13243, pp. 524–542. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-99524-9_29

    Chapter  Google Scholar 

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

  6. Bruynooghe, M., Codish, M., Gallagher, J.P., Genaim, S., Vanhoof, W.: Termination analysis of logic programs through combination of type-based norms. ACM Trans. Program. Lang. Syst. 29(2), 10-es (2007). https://doi.org/10.1145/1216374.1216378

  7. De Angelis, E., Fioravanti, F., Gallagher, J.P., Hermenegildo, M.V., Pettorossi, A., Proietti, M.: Analysis and transformation of constrained Horn clauses for program verification. Theory Pract. Log. Program. 22(6), 974–1042 (2022). https://doi.org/10.1017/S1471068421000211

    Article  MathSciNet  Google Scholar 

  8. De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: VeriMAP: A tool for verifying programs through transformations. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 568–574. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_47

    Chapter  Google Scholar 

  9. De Angelis, E., Govind, V.K.H.: CHC-COMP 2022: Competition report. In: Proceedings 9th Workshop on Horn Clauses for Verification and Synthesis and 10th International Workshop on Verification and Program Transformation. EPTCS, vol. 373, pp. 44–62. Open Publishing Association (2022). https://doi.org/10.4204/EPTCS.373.5

  10. De Angelis, E., Proietti, M., Fioravanti, F., Pettorossi, A.: Multiple query satisfiability of constrained Horn clauses. In: ar**v, Computing Research Repository (2022). https://doi.org/10.48550/ARXIV.2211.15207

  11. De Angelis, E., Proietti, M., Fioravanti, F., Pettorossi, A.: Verifying catamorphism-based contracts using constrained Horn clauses. Theory Pract. Log. Program. 22(4), 555–572 (2022). https://doi.org/10.1017/S1471068422000175

    Article  MathSciNet  MATH  Google Scholar 

  12. Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Generalization strategies for the verification of infinite state systems. Theory Pract. Log. Program. 13(2), 175–199 (2013). https://doi.org/10.1017/S1471068411000627

    Article  MathSciNet  MATH  Google Scholar 

  13. Govind, V.K.H., Shoham, S., Gurfinkel, A.: Solving constrained Horn clauses modulo algebraic data types and recursive functions. In: Proceedings of the ACM on Programming Languages, POPL 2022, vol. 6, pp. 1–29 (2022). https://doi.org/10.1145/3498722

  14. Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: 33rd ACM SIGPLAN Conf. Programming Language Design and Implementation, PLDI 2012, pp. 405–416 (2012). https://doi.org/10.1145/2345156.2254112

  15. Hermenegildo, M.V., Puebla, G., Bueno, F., López-García, P.: Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor). Sci. Comput. Program. 58(1–2), 115–140 (2005). https://doi.org/10.1016/j.scico.2005.02.006

    Article  MathSciNet  MATH  Google Scholar 

  16. Hinze, R., Wu, N., Gibbons, J.: Unifying structured recursion schemes. In: International Conference on Functional Programming, ICFP 2013, pp. 209–220. ACM (2013). https://doi.org/10.1145/2500365.2500578

  17. Hojjat, H., Rümmer, P.: The ELDARICA Horn solver. In: Formal Methods in Computer Aided Design, FMCAD 2018, pp. 1–7. IEEE (2018). https://doi.org/10.23919/FMCAD.2018.8603013

  18. Jaffar, J., Maher, M.: Constraint logic programming: a survey. J. Log. Program. 19(20), 503–581 (1994). https://doi.org/10.1016/0743-1066(94)90033-7

    Article  MathSciNet  MATH  Google Scholar 

  19. Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. Formal Methods Syst. Des. 48(3), 175–205 (2016). https://doi.org/10.1007/s10703-016-0249-4

    Article  MATH  Google Scholar 

  20. Kostyukov, Y., Mordvinov, D., Fedyukovich, G.: Beyond the elementary representations of program invariants over algebraic data types. In: Conference on Programming Language Design and Implementation, PLDI 2021, pp. 451–465. ACM (2021). https://doi.org/10.1145/3453483.3454055

  21. Leuschel, M.: A framework for the integration of partial evaluation and abstract interpretation of logic programs. ACM Trans. Program. Lang. Syst. 26(3), 413–463 (2004). https://doi.org/10.1145/982158.982159

    Article  Google Scholar 

  22. Meijer, E., Fokkinga, M., Paterson, R.: Functional programming with bananas, lenses, envelopes and barbed wire. In: Hughes, J. (ed.) FPCA 1991. LNCS, vol. 523, pp. 124–144. Springer, Heidelberg (1991). https://doi.org/10.1007/3540543961_7

    Chapter  Google Scholar 

  23. Pham, T.-H., Gacek, A., Whalen, M.W.: Reasoning about algebraic data types with abstractions. J. Autom. Reason. 57(4), 281–318 (2016). https://doi.org/10.1007/s10817-016-9368-2

    Article  MathSciNet  MATH  Google Scholar 

  24. Suter, P., Dotta, M., Kuncak, V.: Decision procedures for algebraic data types with abstractions. In: Symposium on Principles of Programming Languages, POPL 2010, pp. 199–210. ACM (2010). https://doi.org/10.1145/1706299.1706325

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

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

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

Download references

Acknowledgement

The authors warmly thank the anonymous reviewers for their helpful comments and suggestions. The authors are members of the INdAM Research Group GNCS.

Author information

Authors and Affiliations

  1. IASI-CNR, Rome, Italy

    Emanuele De Angelis, Alberto Pettorossi & Maurizio Proietti

  2. DEc, University ‘G. d’Annunzio’, Chieti-Pescara, Italy

    Fabio Fioravanti

  3. DICII, University of Rome ‘Tor Vergata’, Rome, Italy

    Alberto Pettorossi

Authors
  1. Emanuele De Angelis
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Fabio Fioravanti
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alberto Pettorossi
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Maurizio Proietti
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Emanuele De Angelis , Fabio Fioravanti , Alberto Pettorossi or Maurizio Proietti .

Editor information

Editors and Affiliations

  1. University of Kiel, Kiel, Germany

    Michael Hanus

  2. Miami University, Oxford, OH, USA

    Daniela Inclezan

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

De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M. (2023). Multiple Query Satisfiability of Constrained Horn Clauses. In: Hanus, M., Inclezan, D. (eds) Practical Aspects of Declarative Languages. PADL 2023. Lecture Notes in Computer Science, vol 13880. Springer, Cham. https://doi.org/10.1007/978-3-031-24841-2_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-24841-2_9

  • Published:

  • Publisher Name: Springer, Cham

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

  • Online ISBN: 978-3-031-24841-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation