References

  1. Rajeev Alur, Rastislav Bodík, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak & Abhishek Udupa (2013): Syntax-guided synthesis. In: FMCAD. IEEE, pp. 1–17.
  2. Rajeev Alur, Dana Fisman, Rishabh Singh & Armando Solar-Lezama (2015): Results and Analysis of SyGuS-Comp'15. In: Proceedings Fourth Workshop on Synthesis, SYNT 2015, San Francisco, CA, USA, 18th July 2015., pp. 3–26, doi:10.4204/EPTCS.202.3.
  3. Rajeev Alur, Dana Fisman, Rishabh Singh & Armando Solar-Lezama (2016): SyGuS-Comp 2016: Results and Analysis. In: Proceedings Fifth Workshop on Synthesis, SYNT@CAV 2016, Toronto, Canada, July 17-18, 2016., pp. 178–202, doi:10.4204/EPTCS.229.13.
  4. Rajeev Alur, Arjun Radhakrishna & Abhishek Udupa (2017): Scaling Enumerative Program Synthesis via Divide and Conquer. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 319–336, doi:10.1007/978-3-319-21690-4_26.
  5. Kshitij Bansal, Andrew Reynolds, Clark W. Barrett & Cesare Tinelli (2016): A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. In: Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings, pp. 82–98, doi:10.1007/978-3-319-40229-1_7.
  6. Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds & Cesare Tinelli (2011): CVC4. In: Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, pp. 171–177, doi:10.1007/978-3-642-22110-1_14.
  7. Clark Barrett, Igor Shikanian & Cesare Tinelli (2007): An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types. Electr. Notes Theor. Comput. Sci. 174(8), pp. 23–37, doi:10.1016/j.entcs.2006.11.037.
  8. Nikolaj Bjørner (2010): Linear Quantifier Elimination as an Abstract Decision Procedure. In: Jürgen Giesl & Reiner Hähnle: IJCAR, LNCS 6173. Springer, pp. 316–330, doi:10.1007/978-3-642-14203-1_27.
  9. Nikolaj Bjørner & Mikolás Janota (2015): Playing with Quantified Satisfaction. In: 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning - Short Presentations, LPAR 2015, Suva, Fiji, November 24-28, 2015., pp. 15–27. Available at http://www.easychair.org/publications/paper/252316.
  10. Martin Brain, Vijay D’Silva, Alberto Griggio, Leopold Haller & Daniel Kroening (2014): Deciding Floating-point Logic with Abstract Conflict Driven Clause Learning. Formal Methods in System Design 45(2), pp. 213–245, doi:10.1007/s10703-013-0203-7.
  11. D. C. Cooper (1972): Theorem Proving in Arithmetic without Multiplication. In: Machine Intelligence, pages 91–100.
  12. Bruno Dutertre (2015): Solving Exists/Forall Problems With Yices. In: Workshop on Satisfiability Modulo Theories.
  13. Azadeh Farzan & Zachary Kincaid (2016): Linear Arithmetic Satisfiability via Strategy Improvement. In: Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9-15 July 2016, pp. 735–743. Available at http://www.ijcai.org/Abstract/16/110.
  14. Grigory Fedyukovich, Arie Gurfinkel & Natasha Sharygina (2015): Automated Discovery of Simulation Between Programs. In: Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings, pp. 606–621, doi:10.1007/978-3-662-48899-7_42.
  15. Jeanne Ferrante & Charles W. Rackoff (1979): The Computational Complexity of Logical Theories. Lecture Notes in Mathematics 718. Springer, doi:10.1007/BFb0062845.
  16. Harald Ganzinger & Konstantin Korovin (2003): New directions in instantiation-based theorem proving. In: Logic in Computer Science, 2003.. IEEE, doi:10.1109/LICS.2003.1210045.
  17. Sumit Gulwani (2011): Automating string processing in spreadsheets using input-output examples. In: Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pp. 317–330, doi:10.1145/1926385.1926423.
  18. Sumit Gulwani, Susmit Jha, Ashish Tiwari & Ramarathnam Venkatesan (2011): Synthesis of loop-free programs. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011, pp. 62–73, doi:10.1145/1993498.1993506.
  19. Anvesh Komuravelli, Arie Gurfinkel & Sagar Chaki (2014): SMT-based Model Checking for Recursive Programs. In: Computer Aided Verification. Springer International Publishing, doi:10.1007/978-3-319-08867-9_2.
  20. Viktor Kuncak, Mikaël Mayer, Ruzica Piskac & Philippe Suter (2010): Complete functional synthesis. In: Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010, Toronto, Ontario, Canada, June 5-10, 2010, pp. 316–329, doi:10.1145/1806596.1806632.
  21. Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark Barrett & Morgan Deters (2014): A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions. In: Computer Aided Verification - 26th International Conference, CAV 2014, pp. 646–662, doi:10.1007/978-3-319-08867-9_43.
  22. Rüdiger Loos & Volker Weispfenning (1993): Applying Linear Quantifier Elimination. Comput. J. 36(5), pp. 450–462, doi:10.1093/comjnl/36.5.450.
  23. David Monniaux (2010): Quantifier Elimination by Lazy Model Enumeration. In: Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, pp. 585–599, doi:10.1007/978-3-642-14295-6_51.
  24. Leonardo Mendonça de Moura & Nikolaj Bjørner (2007): Efficient E-Matching for SMT Solvers. In: Frank Pfenning: CADE, LNCS 4603. Springer, pp. 183–198, doi:10.1007/978-3-540-73595-3_13.
  25. Robert Nieuwenhuis, Albert Oliveras & Cesare Tinelli (2006): Solving SAT and SAT Modulo Theories: From an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T). J. ACM 53(6), pp. 937–977, doi:10.1145/1217856.1217859.
  26. Mathias Preiner, Aina Niemetz & Armin Biere (2017): Counterexample-Guided Model Synthesis. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 264–280, doi:10.1007/978-3-662-48899-7_42.
  27. Markus N. Rabe & Sanjit A. Seshia (2016): Incremental Determinization. In: Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, pp. 375–392, doi:10.1007/978-3-319-40970-2_23.
  28. Andrew Reynolds & Jasmin Christian Blanchette (2016): A Decision Procedure for (Co)datatypes in SMT Solvers. In: Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9-15 July 2016, pp. 4205–4209. Available at http://www.ijcai.org/Abstract/16/631.
  29. Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli & Clark W. Barrett (2015): Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. In: Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II, pp. 198–216, doi:10.1007/978-3-319-21668-3_12.
  30. Andrew Reynolds, Tim King & Viktor Kuncak (2017): Solving quantified linear arithmetic by counterexample-guided instantiation. Formal Methods in System Design, doi:10.1007/s10703-017-0290-y.
  31. Andrew Reynolds, Viktor Kuncak, Cesare Tinelli, Clark Barrett & Morgan Deters (2017): Refutation-based synthesis in SMT. Formal Methods in System Design, doi:10.1007/978-3-540-30142-4_22.
  32. Andrew Reynolds, Maverick Woo, Clark Barrett, David Brumley, Tianyi Liang & Cesare Tinelli (2017): Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification. In: Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II, pp. 453–474, doi:10.1007/978-3-319-63390-9_24.
  33. Armando Solar-Lezama (2013): Program sketching. STTT 15(5-6), pp. 475–495, doi:10.1007/s10009-012-0249-7.
  34. Thomas Sturm & Ashish Tiwari (2011): Verification and synthesis using real quantifier elimination. In: Symbolic and Algebraic Computation, International Symposium, ISSAC 2011 (co-located with FCRC 2011), San Jose, CA, USA, June 7-11, 2011, Proceedings, pp. 329–336, doi:10.1145/1993886.1993935.
  35. Ashish Tiwari, Adrià Gascón & Bruno Dutertre (2015): Program Synthesis Using Dual Interpretation. In: Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, pp. 482–497, doi:10.1007/978-3-319-21401-6_33.
  36. Abhishek Udupa, Arun Raghavan, Jyotirmoy V. Deshmukh, Sela Mador-Haim, Milo M. K. Martin & Rajeev Alur (2013): TRANSIT: specifying protocols with concolic snippets. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '13, Seattle, WA, USA, June 16-19, 2013, pp. 287–296, doi:10.1145/2462156.2462174.
  37. Yue Wang, Neil T. Dantam, Swarat Chaudhuri & Lydia E. Kavraki (2016): Task and Motion Policy Synthesis as Liveness Games. In: Proceedings of the Twenty-Sixth International Conference on Automated Planning and Scheduling, ICAPS 2016, London, UK, June 12-17, 2016., pp. 536.
  38. Christoph M Wintersteiger, Youssef Hamadi & Leonardo De Moura (2013): Efficiently Solving Quantified Bit-vector Formulas. Formal Methods in System Design 42(1), pp. 3–23, doi:10.1007/s10703-012-0156-2.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org