Logo PTI Logo FedCSIS

Proceedings of the 20th Conference on Computer Science and Intelligence Systems (FedCSIS)

Annals of Computer Science and Information Systems, Volume 43

While-guard Synthesis by Abstract Static Analysis and CHC Solving

DOI: http://dx.doi.org/10.15439/2025F8874

Citation: Proceedings of the 20th Conference on Computer Science and Intelligence Systems (FedCSIS), M. Bolanowski, M. Ganzha, L. Maciaszek, M. Paprzycki, D. Ślęzak (eds). ACSIS, Vol. 43, pages 519–530 ()

Full text

Abstract. This paper introduces a novel technique for automatically synthesizing assertion- safe while-guards in imperative programs. Given a partial program (sketch) with missing while-guards, the proposed algorithm synthesizes complete Boolean expressions for the missing ones, such that the obtained complete program satisfies the given assertions. To solve this problem, our technique uses forward and backward abstract static analyses of programs to generate (logical) constraints with unknown predicates that are subsequently solved by employing the logical Constraint Horn Clause (CHC) solvers. We have implemented our synthesis algorithm in a proof-of-concept tool, and evaluated it on a set of C programs with missing while-guards. By experiments we prove the effectiveness of the proposed technique for synthesizing arbitrary Boolean expressions defined over program variables for some interesting program sketches written in C.

References

  1. A. Pnueli and R. Rosner, “On the synthesis of a reactive module,” in Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages. ACM Press, 1989, pp. 179–190. [Online]. Available: https://doi.org/10.1145/75277.75293
  2. A. Solar-Lezama, “Program sketching,” STTT, vol. 15, no. 5-6, pp. 475–495, 2013. [Online]. Available: https://doi.org/10.1007/s10009-012-0249-7
  3. A. Solar-Lezama, R. M. Rabbah, R. Bodík, and K. Ebcioglu, “Programming by sketching for bit-streaming programs,” in Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation. ACM, 2005, pp. 281–294. [Online]. Available: https://doi.org/10.1145/1065010.1065045
  4. A. Dimovski, S. Apel, and A. Legay, “Program sketching using lifted analysis for numerical program families,” in NASA Formal Methods, NFM 2021, ser. LNCS, vol. 12673. Springer, 2021, pp. 95–112. [Online]. Available: https://doi.org/10.1007/978-3-030-76384-8_7
  5. A. S. Dimovski, “Generalized program sketching by abstract interpretation and logical abduction,” in Static Analysis - 30th International Symposium, SAS 2023, Proceedings, ser. LNCS, vol. 14284. Springer, 2023, pp. 212–230. [Online]. Available: https://doi.org/10.1007/978-3-031-44245-2_11
  6. P. Cousot and R. Cousot, “Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints,” in POPL’77. ACM, 1977, pp. 238–252. [Online]. Available: http://doi.acm.org/10.1145/512950.512973
  7. A. Miné, “Tutorial on static inference of numeric invariants by abstract interpretation,” Foundations and Trends in Programming Languages, vol. 4, no. 3-4, pp. 120–372, 2017. [Online]. Available: https://doi.org/10.1561/2500000034
  8. C. Urban and A. Miné, “A decision tree abstract domain for proving conditional termination,” in Static Analysis - 21st International Symposium, SAS 2014. Proceedings, ser. LNCS, vol. 8723. Springer, 2014, pp. 302–318. [Online]. Available: https://doi.org/10.1007/978-3-319-10936-7_19
  9. I. Dillig and T. Dillig, “Explain: A tool for performing abductive inference,” in Computer Aided Verification - 25th International Conference, CAV 2013. Proceedings, ser. LNCS, vol. 8044. Springer, 2013, pp. 684–689. [Online]. Available: https://doi.org/10.1007/978-3-642-39799-8_46
  10. A. Komuravelli, A. Gurfinkel, and S. Chaki, “Smt-based model checking for recursive programs,” in Computer Aided Verification - 26th International Conference, CAV 2014. Proceedings, ser. LNCS, vol. 8559. Springer, 2014, pp. 17–34. [Online]. Available: https://doi.org/10.1007/978-3-319-08867-9_2
  11. H. Hojjat and P. Rümmer, “The ELDARICA horn solver,” in 2018 Formal Methods in Computer Aided Design, FMCAD 2018. IEEE, 2018, pp. 1–7. [Online]. Available: https://doi.org/10.23919/FMCAD. 2018.8603013
  12. C. A. R. Hoare and N. Wirth, “An axiomatic definition of the programming language PASCAL,” Acta Informatica, vol. 2, pp. 335–355, 1973.
  13. A. Miné, “The octagon abstract domain,” Higher-Order and Symbolic Computation, vol. 19, no. 1, pp. 31–100, 2006. [Online]. Available: https://doi.org/10.1007/s10990-006-8609-1
  14. P. Cousot and N. Halbwachs, “Automatic discovery of linear restraints among variables of a program,” in Conference Record of the Fifth Annual ACM Symposium on POPL’78. ACM Press, 1978, pp. 84–96. [Online]. Available: https://doi.org/10.1145/512760.512770
  15. N. S. Bjørner, K. L. McMillan, and A. Rybalchenko, “On solving universally quantified horn clauses,” in Static Analysis - 20th International Symposium, SAS 2013. Proceedings, ser. LNCS, vol. 7935. Springer, 2013, pp. 105–125. [Online]. Available: https://doi.org/10.1007/978-3-642-38856-9_8
  16. G. Fedyukovich, S. Prabhu, K. Madhukar, and A. Gupta, “Quantified invariants via syntax-guided synthesis,” in Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings, Part I, ser. LNCS, vol. 11561. Springer, 2019, pp. 259–277. [Online]. Available: https://doi.org/10.1007/978-3-030-25540-4_14
  17. B. Jeannet and A. Miné, “Apron: A library of numerical abstract domains for static analysis,” in 21st Int. Conf., CAV 2009. Proceedings, ser. LNCS, vol. 5643. Springer, 2009, pp. 661–667. [Online]. Available: https://doi.org/10.1007/978-3-642-02658-4_52
  18. L. M. de Moura and N. Bjørner, “Z3: an efficient SMT solver,” in 14th International Conference, TACAS 2008. Proceedings, ser. LNCS, vol. 4963. Springer, 2008, pp. 337–340. [Online]. Available: https://doi.org/10.1007/978-3-540-78800-3_24
  19. 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, OOPSLA 2013. ACM, 2013, pp. 443–456. [Online]. Available: https://doi.org/10.1145/2509136.2509511
  20. A. S. Dimovski, “Quantitative program sketching using lifted static analysis,” in 25th Int. Conf. FASE 2022, Proceedings, ser. LNCS, vol. 13241. Springer, 2022, pp. 102–122. [Online]. Available: https://doi.org/10.1007/978-3-030-99429-7_6
  21. A. Dimovski, “Quantitative program sketching using decision tree-based lifted analysis,” J. Comput. Lang., vol. 75, p. 101206, 2023. [Online]. Available: https://doi.org/10.1016/j.cola.2023.101206
  22. A. S. Dimovski, “A binary decision diagram lifted domain for analyzing program families,” J. Comput. Lang., vol. 63, p. 101032, 2021. [Online]. Available: https://doi.org/10.1016/j.cola.2021.101032
  23. A. S. Dimovski, S. Apel, and A. Legay, “Several lifted abstract domains for static analysis of numerical program families,” Sci. Comput. Program., vol. 213, p. 102725, 2022. [Online]. Available: https://doi.org/10.1016/j.scico.2021.102725
  24. A. S. Dimovski, C. Brabrand, and A. Wasowski, “Finding suitable variability abstractions for family-based analysis,” in FM 2016: Formal Methods - 21st International Symposium, Proceedings, ser. LNCS, vol. 9995. Springer, 2016, pp. 217–234. [Online]. Available: https://doi.org/10.1007/978-3-319-48989-6_14
  25. A. S. Dimovski and A. Wasowski, “From transition systems to variability models and from lifted model checking back to UPPAAL,” in Models, Algorithms, Logics and Tools, ser. LNCS, vol. 10460. Springer, 2017, pp. 249–268. [Online]. Available: https://doi.org/10.1007/978-3-319-63121-9_13
  26. B. Atanasovski, M. Bogdanovic, G. Velinov, L. Stoimenov, A. S. Dimovski, B. Koteska, D. Jankovic, I. Skrceska, M. Kon-Popovska, and B. Jakimovski, “On defining a model driven architecture for an enterprise e-health system,” Enterp. Inf. Syst., vol. 12, no. 8-9, pp. 915–941, 2018. [Online]. Available: https://doi.org/10.1080/17517575.2018.1521996
  27. T. Dillig, I. Dillig, and S. Chaudhuri, “Optimal guard synthesis for memory safety,” in Computer Aided Verification - 26th International Conference, CAV 2014. Proceedings, ser. LNCS, vol. 8559. Austria: Springer, 2014, pp. 491–507. [Online]. Available: https://doi.org/10.1007/978-3-319-08867-9_32
  28. A. S. Dimovski, “On synthesizing presence conditions in numerical software product lines,” in Proceedings of the 29th ACM International Systems and Software Product Line Conference - Volume A, SPLC 2025. ACM, 2025. [Online]. Available: https://doi.org/10.1145/3744915.3748474
  29. A. Albarghouthi, I. Dillig, and A. Gurfinkel, “Maximal specification synthesis,” in Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016. St. Petersburg: ACM, 2016, pp. 789–801. [Online]. Available: https://doi.org/10.1145/2837614.2837628
  30. A. S. Dimovski, “Weakest safe context synthesis by symbolic game semantics and logical abduction,” in Proceedings of the 40th ACM/SIGAPP Symposium on Applied Computing, SAC 2025. ACM, 2025, pp. 1990–1997. [Online]. Available: https://doi.org/10.1145/3672608.3707849
  31. F. Bourdoncle, “Abstract debugging of higher-order imperative languages,” in Proceedings of the ACM SIGPLAN’93 Conference on Programming Language Design and Implementation (PLDI). ACM, 1993, pp. 46–55. [Online]. Available: https://doi.org/10.1145/155090.155095
  32. A. Miné, “Backward under-approximations in numeric abstract domains to automatically infer sufficient program conditions,” Sci. Comput. Program., vol. 93, pp. 154–182, 2014. [Online]. Available: https://doi.org/10.1016/j.scico.2013.09.014
  33. P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival, “The astreé analyzer,” in Programming Languages and Systems, 14th European Symposium on Programming, ESOP 2005, Proceedings, ser. LNCS, vol. 3444. Springer, 2005, pp. 21–30. [Online]. Available: https://doi.org/10.1007/978-3-540-31987-0_3
  34. M. Greitschus, D. Dietsch, M. Heizmann, A. Nutz, C. Schätzle, C. Schilling, F. Schüssele, and A. Podelski, “Ultimate taipan: Trace abstraction and abstract interpretation - (competition contribution),” in 23rd International Conference, TACAS 2017, Proceedings, Part II, ser. LNCS, vol. 10206, 2017, pp. 399–403. [Online]. Available: https://doi.org/10.1007/978-3-662-54580-5_31
  35. J. Henry, D. Monniaux, and M. Moy, “PAGAI: A path sensitive static analyser,” Electron. Notes Theor. Comput. Sci., vol. 289, pp. 15–25, 2012. [Online]. Available: https://doi.org/10.1016/j.entcs.2012.11.003
  36. X. Rival, “Understanding the origin of alarms in astrée,” in Static Analysis, 12th International Symposium, SAS 2005, Proceedings, ser. LNCS, vol. 3672. Springer, 2005, pp. 303–319. [Online]. Available: https://doi.org/10.1007/11547662_21
  37. A. S. Dimovski and A. Legay, “Computing program reliability using forward-backward precondition analysis and model counting,” in Fundamental Approaches to Software Engineering - 23rd International Conference, FASE 2020, Proceedings, ser. LNCS, vol. 12076. Springer, 2020, pp. 182–202. [Online]. Available: https://doi.org/10.1007/978-3-030-45234-6_9
  38. R. Alur, R. Bodík, G. Juniwal, M. M. K. Martin, M. Raghothaman, S. A. Seshia, R. Singh, A. Solar-Lezama, E. Torlak, and A. Udupa, “Syntax-guided synthesis,” in Formal Methods in Computer-Aided Design, FMCAD 2013. IEEE, 2013, pp. 1–8. [Online]. Available: http://ieeexplore.ieee.org/document/6679385/
  39. Y. Gu, T. Tsukada, and H. Unno, “Optimal CHC solving via termination proofs,” Proc. ACM Program. Lang., vol. 7, no. POPL, pp. 604–631, 2023. [Online]. Available: https://doi.org/10.1145/3571214
  40. T. A. Beyene, C. Popeea, and A. Rybalchenko, “Solving existentially quantified horn clauses,” in Computer Aided Verification - 25th International Conference, CAV 2013. Proceedings, ser. LNCS, vol. 8044. Springer, 2013, pp. 869–882. [Online]. Available: https://doi.org/10.1007/978-3-642-39799-8_61
  41. T. Kuwahara, R. Sato, H. Unno, and N. Kobayashi, “Predicate abstraction and CEGAR for disproving termination of higherorder functional programs,” in Computer Aided Verification - 27th International Conference, CAV 2015, Proceedings, Part II, ser. LNCS, vol. 9207. Springer, 2015, pp. 287–303. [Online]. Available: https://doi.org/10.1007/978-3-319-21668-3_17
  42. A. Gurfinkel, T. Kahsai, A. Komuravelli, and J. A. Navas, “The seahorn verification framework,” in Computer Aided Verification - 27th International Conference, CAV 2015, Proceedings, Part I, ser. LNCS, vol. 9206. Springer, 2015, pp. 343–361. [Online]. Available: https://doi.org/10.1007/978-3-319-21690-4_20
  43. T. Kahsai, P. Rümmer, H. Sanchez, and M. Schäf, “Jayhorn: A framework for verifying java programs,” in Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings, Part I, ser. LNCS, vol. 9779. Springer, 2016, pp. 352–358. [Online]. Available: https://doi.org/10.1007/978-3-319-41528-4_19
  44. K. Hashimoto and H. Unno, “Refinement type inference via horn constraint optimization,” in Static Analysis - 22nd International Symposium, SAS 2015, Saint-Malo, France, September 9-11, 2015, Proceedings, ser. Lecture Notes in Computer Science, vol. 9291. Springer, 2015, pp. 199–216. [Online]. Available: https://doi.org/10.1007/978-3-662-48288-9_12
  45. J. Leroux, P. Rümmer, and P. Subotic, “Guiding craig interpolation with domain-specific abstractions,” Acta Informatica, vol. 53, no. 4, pp. 387–424, 2016. [Online]. Available: https://doi.org/10.1007/s00236-015-0236-z
  46. T. A. Beyene, S. Chaudhuri, C. Popeea, and A. Rybalchenko, “A constraint-based approach to solving games on infinite graphs,” in The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14. ACM, 2014, pp. 221–234. [Online]. Available: https://doi.org/10.1145/2535838.2535860
  47. J. Kim, Q. Hu, L. D’Antoni, and T. W. Reps, “Semantics-guided synthesis,” Proc. ACM Program. Lang., vol. 5, no. POPL, pp. 1–32, 2021. [Online]. Available: https://doi.org/10.1145/3434311
  48. K. J. C. Johnson, A. Reynolds, T. W. Reps, and L. D’Antoni, “The semgus toolkit,” in Computer Aided Verification - 36th International Conference, CAV 2024, Proceedings, Part III, ser. LNCS, vol. 14683. Springer, 2024, pp. 27–40. [Online]. Available: https://doi.org/10.1007/978-3-031-65633-0_2
  49. S. So and H. Oh, “Synthesizing imperative programs from examples guided by static analysis,” in Static Analysis - 24th International Symposium, SAS 2017, Proceedings, ser. LNCS, vol. 10422. Springer, 2017, pp. 364–381. [Online]. Available: https://doi.org/10.1007/978-3-319-66706-5_18
  50. A. S. Dimovski, “Imperative program synthesis by abstract static analysis and SMT mutations,” in Proceedings of the 24th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, GPCE 2025, Bergen, Norway, July 3-4, 2025. ACM, 2025, pp. 27–40. [Online]. Available: https://doi.org/10.1145/3742876.3742884
  51. A. Dimovski, “Mutation-based lifted repair of software product lines,” in 38th European Conference on Object-Oriented Programming, ECOOP 2024, ser. LIPIcs, vol. 313. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, pp. 12:1–12:24. [Online]. Available: https://doi.org/10.4230/LIPIcs.ECOOP.2024.12