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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
D. C. Cooper (1972):
Theorem Proving in Arithmetic without Multiplication.
In: Machine Intelligence, pages 91–100.
Bruno Dutertre (2015):
Solving Exists/Forall Problems With Yices.
In: Workshop on Satisfiability Modulo Theories.
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.
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.
Jeanne Ferrante & Charles W. Rackoff (1979):
The Computational Complexity of Logical Theories.
Lecture Notes in Mathematics 718.
Springer,
doi:10.1007/BFb0062845.
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.
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.
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.
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.
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.
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.
Rüdiger Loos & Volker Weispfenning (1993):
Applying Linear Quantifier Elimination.
Comput. J. 36(5),
pp. 450–462,
doi:10.1093/comjnl/36.5.450.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
Armando Solar-Lezama (2013):
Program sketching.
STTT 15(5-6),
pp. 475–495,
doi:10.1007/s10009-012-0249-7.
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.
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.
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.
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.
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.