CoChat
Sign Up
Cited by 53

Counterexample Guided Inductive Synthesis Modulo Theories

Abate, Alessandro, David, Cristina, Kesseli, Pascal, Kroening, Daniel, Polgreen, Elizabeth·2018·Lecture Notes in Computer Science
DOI 10.1007/978-3-319-96145-3_15
Open this paper in CoChat — free account

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Integrity signals

Registry

Crossref · 10.1007/978-3-319-96145-3_15

Cites

1 of 1 references verified0 citation errors · 0 not checkable

Statistics

Claims the paper makes

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

  • CEGIS is an iterative algorithm commonly used in Program Synthesis and Formal Methods to construct programs or solutions that satisfy a given specification.

    “CEGIS is an iterative algorithm commonly used in Program Synthesis and Formal Methods to construct programs or solutions that satisfy a given specification (Abate et al. 2018; Jha et al. 2010; Solar-Lezama et al. 2005).”

    From Counterexample Guided Program Repair Using Zero-Shot Learning and MaxSAT-based Fault Localization (2025) · cites this paper as Abate et al. 2018

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

The self-check needs the paper’s full text.

Cites

Flagged first, then by citations

Research works printed but not linked: 29

  1. Albarghouthi, A., Gulwani, S., Kincaid, Z.: Recursive program synthesis. In: Shary- gina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 934-950. Springer, Hei- delberg (2013). https://doi.org/10.1007/978-3-642-39799-8 67 · DOI
  2. Alur, R., Černý, P., Radhakrishna, A.: Synthesis through unification. In: Kroening, D., Pȃsȃreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 163-179. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21668-3 10 · DOI
  3. Alur, R., Fisman, D., Singh, R., Solar-Lezama, A.: SyGuS-Comp 2017: results and analysis. CoRR abs/1711.11438 (2017) · arXiv
  4. Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: 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 · DOI
  5. Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168-176. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24730-2 15 · DOI · Paper page
  6. Collins, G.E.: Hauptvortrag: quantifier elimination for real closed fields by cylin- drical algebraic decompostion. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134-183. Springer, Heidelberg (1975). https://doi.org/10.1007/3-540- 07407-4 17 · DOI
  7. David, C., Kesseli, P., Kroening, D., Lewis, M.: Danger invariants. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 182-198. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-48989-6 12 · DOI
  8. David, C., Kroening, D., Lewis, M.: Using program synthesis for program analysis. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 483-498. Springer, Heidelberg (2015). https://doi.org/10.1007/978- 3-662-48899-7 34 · DOI
  9. Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502-518. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24605-3 37 · DOI
  10. Feng, Y., Bastani, O., Martins, R., Dillig, I., Anand, S.: Automated synthesis of semantic malware signatures using maximum satisfiability. In: NDSS. The Internet Society (2017)
  11. Feng, Y., Martins, R., Geffen, J.V., Dillig, I., Chaudhuri, S.: Component-based synthesis of table consolidation and transformation tasks from examples. In: PLDI, pp. 422-436. ACM (2017)
  12. Feng, Y., Martins, R., Wang, Y., Dillig, I., Reps, T.W.: Component-based synthesis for complex APIs. In: POPL, pp. 599-612. ACM (2017)
  13. Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T ): fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175-188. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3- 540-27813-9 14 · DOI
  14. Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: PLDI, pp. 62-73. ACM (2011)
  15. Gulwani, S., Korthikanti, V.A., Tiwari, A.: Synthesizing geometry constructions. In: PLDI, pp. 50-61. ACM (2011)
  16. Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: ICSE, no. 1, pp. 215-224. ACM (2010)
  17. Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View, 1st edn. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-74105-3 · DOI
  18. Manna, Z., Waldinger, R.: A deductive approach to program synthesis. In: IJCAI. pp. 542-551.
  19. 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 · DOI · Paper page
  20. Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937-977 (2006)
  21. Padhi, S., Millstein, T.D.: Data-driven loop invariant inference with automatic feature synthesis. CoRR abs/1707.02029 (2017) · arXiv
  22. Perelman, D., Gulwani, S., Grossman, D., Provost, P.: Test-driven synthesis. In: PLDI, pp. 408-418. ACM (2014)
  23. Raghothaman, M., Udupa, A.: Language to specify syntax-guided synthesis prob- lems. CoRR abs/1405.5590 (2014) · arXiv
  24. Reynolds, A., Deters, M., Kuncak, V., Tinelli, C., Barrett, C.: Counterexample- guided quantifier instantiation for synthesis in SMT. In: Kroening, D., Pȃsȃreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 198-216. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21668-3 12 · DOI
  25. Rosen, E.: An existential fragment of second order logic. Arch. Math. Log. 38(4-5), 217-234 (1999)
  26. Solar-Lezama, A.: Program sketching. STTT 15(5-6), 475-495 (2013)
  27. Solar-Lezama, A., Rabbah, R.M., Bodík, R., Ebcioglu, K.: Programming by sketch- ing for bit-streaming programs. In: PLDI, pp. 281-294. ACM (2005)
  28. Solar-Lezama, A., Tancau, L., Bodík, R., Seshia, S.A., Saraswat, V.A.: Combina- torial sketching for finite programs. In: ASPLOS, pp. 404-415. ACM (2006)
  29. Strichman, O.: On solving Presburger and linear arithmetic with SAT. In: Aagaard, M.D., O'Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 160-170. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-36126-X 10 · DOI

Cited by

Sorted by citations

Authors
Abate, A., David, C., Kesseli, P., Kroening, D., & Polgreen, E.
ORCID
Venue
Lecture Notes in Computer Science
Publisher
Springer International Publishing
Published
2018
Pages
270-288
ISSN
  • 0302-9743
  • 1611-3349
DOI
10.1007/978-3-319-96145-3_15
Cited by
53
References
1
Licence
creativecommons.org/licenses/by/4.0 (unspecified)

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review