Abstract
Condition synthesis takes a program in which some of the conditions in conditional branches are missing, and a specification, and automatically infers conditions to fill-in the holes such that the program meets the specification.
In this paper, we propose CoSyn, an algorithm for determining the realizability of a condition synthesis problem, with an emphasis on proving unrealizability efficiently. We use the novel concept of a doomed initial state, which is an initial state that can reach an error state along every run of the program. For a doomed initial state \(\sigma \), there is no way to make the program safe by forcing \(\sigma \) (via conditions) to follow one computation or another. CoSyn checks for the existence of a doomed initial state via a reduction to Constrained Horn Clauses (CHC).
We implemented CoSyn in SeaHorn using Spacer as the CHC solver and evaluated it on multiple examples. Our evaluation shows that CoSyn outperforms the state-of-the-art syntax-guided tool Cvc5 in proving both realizability and unrealizability. We also show that joining forces of CoSyn and Cvc5 outperforms Cvc5 alone, allowing to solve more instances, faster.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Where CoSyn is executed, and Cvc5 is then invoked on the given grammar and implication \(\varPsi ^f(l) \implies \varPsi (l)\implies \varPsi ^t(l)\).
- 2.
We emphasize that a deterministic CFG can still contain non-deterministic assignments. In the context of CFG, non-determinisim only refers to the form/structure of the CFG.
- 3.
For readability, in this section we omit s from \(l_s,l^f_{s},l^t_{s}\) and their corresponding predicates.
- 4.
We emphasize that the implications in the different locations are independent, thus allowing synthesis of the conditions separately, one by one. Separate synthesis of conditions cannot be done trivially in regular SyGuS, due to the dependency between conditions in the synthesized program.
- 5.
Its predecessor, Cvc4, won the competition in most categories: https://sygus.org/comp/2019/results-slides.pdf.
- 6.
- 7.
We used Cvc5 ’s default configuration, except for the addition of sygus-add-const-grammar flag, following the advice of Cvc5 ’s developers.
- 8.
G1 is a standard grammar allowing comparisons (e.g. \(=\), \(\le \), etc.), using arrays, Integer and Boolean variables.
References
Alur, R., et al.: Syntax-guided synthesis. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, 20–23 October 2013, pp. 1–8. IEEE (2013)
Beyer, D.: Competition on software verification. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 504–524. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28756-5_38
Bhatia, S., Padhi, S., Natarajan, N., Sharma, R., Jain, P.: OASIS: ILP-guided synthesis of loop invariants. CoRR (2019)
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
Bloem, R., et al.: FoREnSiC– an automatic debugging environment for C programs. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 260–265. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39611-3_24
DeMarco, F., Xuan, J., Le Berre, D., Monperrus, M.: Automatic repair of buggy if conditions and missing preconditions with SMT. In: Proceedings of the 6th International Workshop on Constraints in Software Testing, Verification, and Analysis, pp. 30–39. ACM (2014)
Do, H., Elbaum, S., Rothermel, G.: Supporting controlled experimentation with testing techniques: an infrastructure and its potential impact. Empir. Softw. Eng. 10(4), 405–435 (2005)
Farzan, A., Lette, D., Nicolet, V.: Recursion synthesis with unrealizability witnesses. In: Jhala, R., Dillig, I. (eds.) PLDI 2022: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, 13–17 June 2022, pp. 244–259. ACM (2022)
Fedyukovich, G., Gupta, A.: Functional synthesis with examples. In: Schiex, T., de Givry, S. (eds.) CP 2019. LNCS, vol. 11802, pp. 547–564. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30048-7_32
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
Hu, Q., Breck, J., Cyphert, J., D’Antoni, L., Reps, T.W.: Proving unrealizability for syntaxguided synthesis. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification - 31st International Conference, CAV 2019. LNCS, vol. 11561, pp. 335–352. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-25540-4_18
Hu, Q., D’Antoni, L., Cyphert, J., Reps, T.: Exact and approximate unrealizability of syntax-guided synthesis problems. In: PLDI (2020)
Hu, Q., Evavold, I., Samanta, R., Singh, R., D’Antoni, L.: Program repair via direct state manipulation (2018)
Huang, K., Qiu, X., Shen, P., Wang, Y.: Reconciling enumerative and deductive program synthesis. In: PLDI, pp. 1159–1174 (2020)
Kim, J., D’Antoni, L., Reps, T.W.: Unrealizability logic. In: POPL 2023: Proceedings of the 50th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM (2023)
Kim, J., Hu, Q., D’Antoni, L., Reps, T.W.: Semantics guided synthesis. In: POPL (2020)
Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. Formal Methods Syst. Des. 48(3), 175–205 (2016)
Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Complete functional synthesis. In: PLDI (2010)
Long, F., Rinard, M.: Staged program repair with condition synthesis. In: ESEC/FSE, pp. 166–178. ACM (2015)
Nguyen, T.-T., Ta, Q.-T., Chin, W.-N.: Automatic program repair using formal verification and expression templates. In: Enea, C., Piskac, R. (eds.) VMCAI 2019. LNCS, vol. 11388, pp. 70–91. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-11245-5_4
Padhi, S., Sharma, R., Millstein, T.: LoopInvGen: a loop invariant generator based on precondition inference. arXiv (2017)
Polozov, O., Gulwani, S.: FlashMeta: a framework for inductive program synthesis. In: OOPSLA, vol. 25–30-Oct-, pp. 107–126 (2015)
Reynolds, A., Barbosa, H., Nötzli, A., Barrett, C., Tinelli, C.: cvc4sy: smart and fast term enumeration for syntax-guided synthesis. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 74–83. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-25543-5_5
Si, X., Lee, W., Zhang, R., Albarghouthi, A., Koutris, P., Naik, M.: Syntax-guided synthesis of datalog programs. In: ESEC/FSE, pp. 515–527 (2018)
So, S., Oh, H.: Synthesizing imperative programs from examples guided by static analysis. In: Ranzato, F. (ed.) SAS 2017. LNCS, vol. 10422, pp. 364–381. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66706-5_18
Solar-Lezama, A., Tancau, L., Bodik, R., Saraswat, V., Seshia, S., Saraswat, V.: Combinatorial sketching for finite programs. In: ACM Sigplan Notices, vol. 41, pp. 404–415. ACM (2006)
Srivastava, S., Gulwani, S., Foster, J.S.: From program verification to program synthesis. In: POPL (2010)
Wang, X., Dillig, I., Singh, R.: Program synthesis using abstraction refinement. arXiv, 2(January 2018) (2017)
Xiong, Y., et al.: Precise condition synthesis for program repair. In: ICSE (2017)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Rothenberg, BC., Grumberg, O., Vizel, Y., Singher, E. (2023). Condition Synthesis Realizability via Constrained Horn Clauses. In: Rozier, K.Y., Chaudhuri, S. (eds) NASA Formal Methods. NFM 2023. Lecture Notes in Computer Science, vol 13903. Springer, Cham. https://doi.org/10.1007/978-3-031-33170-1_23
Download citation
DOI: https://doi.org/10.1007/978-3-031-33170-1_23
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-33169-5
Online ISBN: 978-3-031-33170-1
eBook Packages: Computer ScienceComputer Science (R0)