Refutation-based synthesis in SMT

Aloul FA, Ramani A, Markov IL, Sakallah KA (2002) Solving difficult sat instances in the presence of symmetry. In: Proceedings of the 39th annual design automation conference. ACM, pp 731–736 Alur R, Bodik R, Dallal E, Fisman D, Garg P, Juniwal G, Kress-Gazit H, Madhusudan P, Martin MMK, Raghothaman M, Saha S, Seshia SA, Singh R, Solar-Lezama A, Torlak E, Udupa A (2014) Syntax-guided synthesis. In: Marktoberdrof NATO proceedings (to appear). http://sygus.seas.upenn.edu/files/sygus_extended.pdf, retrieved 2015-02-06 Alur R, Bodík R, Juniwal G, Martin MMK, Raghothaman M, Seshia SA, Singh R, Solar-Lezama A, Torlak E, Udupa A (2013) Syntax-guided synthesis. In: FMCAD. IEEE, pp 1–17 Alur R, Martin MMK, Raghothaman M, Stergiou C, Tripakis S, Udupa A (2014) Synthesizing finite-state protocols from scenarios and requirements. In: Yahav E (ed) Haifa verification conference, LNCS, vol 8855, pp 75–91. Springer. doi:10.1007/978-3-319-13338-6_7 Barrett C, Conway C, Deters M, Hadarean L, Jovanovic D, King T, Reynolds A, Tinelli C (2011) CVC4. In: Proceedings of CAV’11, LNCS, vol 6806. Springer, pp 171–177 Barrett C, Deters M, de Moura LM, Oliveras A, Stump A (2013) 6 years of SMT-COMP. JAR 50(3):243–277. doi:10.1007/s10817-012-9246-5 Barrett C, Shikanian I, Tinelli C (2007) An abstract decision procedure for satisfiability in the theory of inductive data types. J Satisf Boolean Model Comput 3:21–46 Bjørner N (2010) Linear quantifier elimination as an abstract decision procedure. In: Giesl J, Hähnle R (eds) IJCAR, LNCS, vol 6173, pp 316–330. Springer. doi:10.1007/978-3-642-14203-1_27 Bloem R, Jobstmann B, Piterman N, Pnueli A, Sa’ar Y (2012) Synthesis of reactive(1) designs. J Comput Syst Sci 78(3):911–938. doi:10.1016/j.jcss.2011.08.007 Constable RL, Allen SF, Bromley M, Cleaveland R, Cremer JF, Harper RW, Howe DJ, Knoblock TB, Mendler NP, Panangaden P, Sasaki JT, Smith SF (1986) Implementing mathematics with the Nuprl proof development system. Prentice Hall, Englewood Cliffs Cousot P (2005) Proving program invariance and termination by parametric abstraction, Lagrangian relaxation and semidefinite programming. In: Cousot R (ed) VMCAI, LNCS, vol 3385. Springer, pp 1–24. doi:10.1007/978-3-540-30579-8_1 Déharbe D, Fontaine P, Merz S, Paleo BW (2011) Exploiting symmetry in SMT problems. In: Automated deduction—CADE-23. Springer, pp 222–236 Detlefs D, Nelson G, Saxe, JB (2003) Simplify: a theorem prover for program checking. Technical report. J ACM Dutertre B (2015) Solving exists/forall problems with yices. In: Workshop on satisfiability modulo theories Finkbeiner B, Schewe S (2013) Bounded synthesis. STTT 15(5–6):519–539. doi:10.1007/s10009-012-0228-z Ge Y, Barrett C, Tinelli C (2007) Solving quantified verification conditions using satisfiability modulo theories. In: Pfenning F (ed) CADE, LNCS, vol 4603. Springer, pp 167–182. doi:10.1007/978-3-540-73595-3_12 Ge Y, de Moura L (2009) Complete instantiation for quantified formulas in satisfiability modulo theories. In: Proceedings of CAV’09, LNCS, vol 5643. Springer, pp 306–320. doi:10.1007/978-3-642-02658-4_25 Green CC (1969) Application of theorem proving to problem solving. In: Walker DE, Norton LM (eds) IJCAI. William Kaufmann, Los Altos, pp 219–240 Jacobs S, Kuncak V (2011) Towards complete reasoning about axiomatic specifications. Verification, model checking, and abstract interpretation. Springer, Berlin, pp 278–293 Janota M, Klieber W, Marques-Silva J, Clarke E (2012) Solving QBF with counterexample guided refinement. In: International conference on theory and applications of satisfiability testing. Springer Berlin, pp 114–128 (2012) Janota M, Silva JPM (2011) Abstraction-based algorithm for 2qbf. In: Theory and applications of satisfiability testing—SAT 2011—14th international conference, SAT 2011, Proceedings, pp 230–244, Ann Arbor, MI, USA, 19–22 June 2011 Jha S, Gulwani S, Seshia SA, Tiwari A (2010) Oracle-guided component-based program synthesis. In: Kramer J, Bishop J, Devanbu PT, Uchitel S (eds) ICSE. ACM, pp 215–224. doi:10.1145/1806799.1806833 Kneuss E, Koukoutos M, Kuncak V (2015) Deductive program repair. In: Kroening D, Pasareanu CS (eds) CAV, LNCS, vol 9207. Springer, pp 217–233. doi:10.1007/978-3-319-21668-3_13 Kneuss E, Kuraj I, Kuncak V, Suter P (2013) Synthesis modulo recursive functions. In: Hosking AL, Eugster PT, Lopes CV(eds) OOPSLA. ACM, pp 407–426. doi:10.1145/2509136.2509555 Komuravelli A, Gurfinkel A, Chaki S (2014) SMT-based model checking for recursive programs. In: Computer aided verification. Springer Kuncak V, Mayer M, Piskac R, Suter P (2010)Complete functional synthesis. In: Zorn BG, Aiken A (eds) PLDI, pp 316–329. ACM. doi:10.1145/1806596.1806632 Kuncak V, Mayer M, Piskac R, Suter P (2012) Software synthesis procedures. CACM 55(2):103–111. doi:10.1145/2076450.2076472 Kuncak V, Mayer M, Piskac R, Suter P (2013) Functional synthesis for linear arithmetic and sets. STTT 15(5–6):455–474. doi:10.1007/s10009-011-0217-7 Madhavan R, Kuncak V (2014) Symbolic resource bound inference for functional programs. In: Biere A, Bloem R (eds) CAV, LNCS, vol 8559. Springer, pp 762–778. doi:10.1007/978-3-319-08867-9_51 Manna Z, Waldinger RJ (1980) A deductive approach to program synthesis. TOPLAS 2(1):90–121. doi:10.1145/357084.357090 Monniaux D (2010) Quantifier elimination by lazy model enumeration. In: Touili T, Cook B, Jackson P (eds) CAV, LNCS, vol 6174. Springer, pp 585–599. doi:10.1007/978-3-642-14295-6_51 de Moura LM, Bjørner N (2007) Efficient e-matching for SMT solvers. In: F. Pfenning (ed) CADE, LNCS, vol 4603. Springer, pp 183–198. doi:10.1007/978-3-540-73595-3_13 Nieuwenhuis R, Oliveras A, Tinelli C (2006) Solving SAT and SAT modulo theories: from an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T). J ACM 53(6):937–977 Perelman D, Gulwani S, Grossman D, Provost P (2010) Test-driven synthesis. In: O’Boyle MFP, Pingali K (eds) PLDI. ACM, p 43. doi:10.1145/2594291.2594297 Pnueli A, Rosner R (1989) On the synthesis of a reactive module. In: Conference record of the sixteenth annual ACM symposium on principles of programming languages, pp 179–190, Austin, TX, USA, 11–13 Jan 1989. doi:10.1145/75277.75293 Presburger M (1929) Über die Vollständigkeit eines gewissen Systems der Aritmethik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Comptes Rendus du premier Congrès des Mathématiciens des Pays slaves, Warsawa, pp 92–101 Raghothaman M., Udupa A (2014) Language to specify syntax-guided synthesis problems. CoRR arXiv:1405.5590 Reynolds A, Deters M, Kuncak V, Tinelli C, Barrett CW (2015) Counterexample-guided quantifier instantiation for synthesis in SMT. In: Computer aided verification—27th international conference, CAV 2015, Proceedings, Part II, pp 198–216, San Francisco, CA, USA, 18–24 July 2015 Reynolds A, King T, Kuncak V (2015) An instantiation-based approach for solving quantified linear arithmetic. CoRR arXiv:1510.02642 Reynolds A, Tinelli C, Goel A, Krstić S, Deters M, Barrett C (2013) Quantifier instantiation techniques for finite model finding in SMT. In: Bonacina MP (ed) Proceedings of the 24th international conference on automated deduction, Lake Placid, NY, USA, Lecture notes in computer science, vol 7898. Springer, pp 377–391 Reynolds A, Tinelli C, Moura LD (2014) Finding conflicting instances of quantified formulas in SMT. In: Formal methods in computer-aided design (FMCAD) Ryzhyk L, Walker A, Keys J, Legg A, Raghunath A, Stumm M, Vij M (2014) User-guided device driver synthesis. In: Flinn J, Levy H (eds) OSDI. USENIX Association, pp 661–676 Saha S, Garg P, Madhusudan P (2015) Alchemist: learning guarded affine functions. In: Kroening D, Psreanu CS (eds) Computer aided verification, Lecture notes in computer science, vol 9206, pp 440–446. Springer. doi:10.1007/978-3-319-21690-4_26 Schkufza E, Sharma R, Aiken A (2013) Stochastic superoptimization. SIGPLAN Not 48(4):305–316. doi:10.1145/2499368.2451150 Solar-Lezama A (2013) Program sketching. STTT 15(5–6):475–495. doi:10.1007/s10009-012-0249-7 Solar-Lezama A, Tancau L, Bodík R, Seshia SA, Saraswat VA (2006) Combinatorial sketching for finite programs. In: Shen JP, Martonosi M (eds) ASPLOS. ACM, pp 404–415. doi:10.1145/1168857.1168907 Srivastava S, Gulwani S, Foster JS (2013) Template-based program verification and program synthesis. STTT 15(5–6):497–518. doi:10.1007/s10009-012-0223-4 Stump A, Sutcliffe G, Tinelli C (2014) Starexec: a cross-community infrastructure for logic solving. In: Proceedings of the 7th international joint conference on automated reasoning, Lecture notes in artificial intelligence. Springer Svenningsson J, Axelsson E (2012) Combining deep and shallow embedding for EDSL. In: Trends in functional programming—13th international symposium, TFP 2012, Revised selected papers, pp 21–36, St. Andrews, UK, 12–14 June 2012. doi:10.1007/978-3-642-40447-4_2 Tiwari A, Gascón A, Dutertre B (2015) Program synthesis using dual interpretation. In: Automated deduction—CADE-25—25th international conference on automated deduction, Proceedings, Berlin, Germany, 1–7 Aug 2015, pp 482–497 Udupa A, Raghavan A, Deshmukh JV, Mador-Haim S, Martin MM, Alur R (2013) Transit: specifying protocols with concolic snippets. In: PLDI. ACM, pp 287–296. doi:10.1145/2491956.2462174 Wildmoser M, Nipkow T (2004) Certifying machine code safety: shallow versus deep embedding. In: Theorem proving in higher order logics, 17th international conference, TPHOLs 2004, Proceedings, pp 305–320, Park City, UT, USA, 14–17 Sept 2004. doi:10.1007/978-3-540-30142-4_22 Wintersteiger CM, Hamadi Y, De Moura L (2013) Efficiently solving quantified bit-vector formulas. Form Methods Syst Des 42(1):3–23