Publications

2017
[25] Designing Theory Solvers with Extensions (Andrew Reynolds, Cesare Tinelli, Dejan Jovanović, Clark Barrett), In Proceedings of the 11th International Symposium on Frontiers of Combining Systems (FroCoS '17) (Clare Dixon, Marcelo Finger, eds.), Springer, volume 10483, 2017. (Brasilia, Brazil) [bibtex] [pdf]
[24] Relational Constraint Solving in SMT (Baoluo Meng, Andrew Reynolds, Cesare Tinelli, Clark Barrett), In Proceedings of the 26th International Conference on Automated Deduction (CADE '17) (Leonardo de Moura, ed.), Springer, volume 10395, 2017. (Gothenburg, Sweden) [bibtex] [pdf]
[23] SMTCoq: A Plug-In for Integrating SMT Solvers into Coq (Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, Clark Barrett), In Proceedings of the 29th International Conference on Computer Aided Verification (CAV '17) (Rupak Majumdar, Viktor Kuncak, eds.), Springer, volume 10426, 2017. (Heidelberg, Germany) [bibtex] [pdf]
[22] Scaling up DPLL(T) String Solvers Using Context-Dependent Simplification (Andrew Reynolds, Maverick Woo, Clark Barrett, David Brumley, Tianyi Liang, Cesare Tinelli), In Proceedings of the 29th International Conference on Computer Aided Verification (CAV '17) (Rupak Majumdar, Viktor Kuncak, eds.), Springer, volume 10426, 2017. (Heidelberg, Germany) [bibtex] [pdf]
[21] Solving quantified linear arithmetic by counterexample-guided instantiation (Andrew Reynolds, Tim King, Viktor Kuncak), In Formal Methods in System Design, Springer US, 2017. [bibtex] [pdf] [doi]
[20] Refutation-based synthesis in SMT (Andrew Reynolds, Viktor Kuncak, Cesare Tinelli, Clark Barrett, Morgan Deters), In Formal Methods in System Design, Springer US, 2017. [bibtex] [pdf]
[19] Constraint solving for finite model finding in SMT solvers (Andrew Reynolds, Cesare Tinelli, Clark Barrett), In TPLP, volume 17, 2017. [bibtex] [pdf] [doi]
[18] A Decision Procedure for (Co)datatypes in SMT Solvers (Andrew Reynolds, Jasmin Christian Blanchette), In J. Autom. Reasoning, volume 58, 2017. [bibtex] [pdf] [doi]
2016
[17] Lazy Proofs for DPLL(T)-Based SMT Solvers (Guy Katz, Clark Barrett, Cesare Tinelli, Andrew Reynolds, Liana Hadarean), In Proceedings of the 16th International Conference on Formal Methods In Computer-Aided Design (FMCAD '16) (Ruzica Piskac, Muralidhar Talupur, eds.), FMCAD Inc., 2016. (Mountain View, CA. Best paper award.) [bibtex] [pdf]
[16] An Efficient SMT Solver for String Constraints (Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze, Cesare Tinelli, Clark Barrett, Morgan Deters), In Formal Methods in System Design, Springer US, volume 48, 2016. [bibtex] [pdf] [doi]
[15] A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT (Kshitij Bansal, Andrew Reynolds, Clark Barrett, Cesare Tinelli), In Proceedings of the 8th International Joint Conference on Automated Reasoning (IJCAR '16) (Nicola Olivetti, Ashish Tiwari, eds.), Springer International Publishing, volume 9706, 2016. (Coimbra, Portugal) [bibtex] [pdf] [doi]
2015
[14] Fine-grained SMT Proofs for the Theory of Fixed-width Bit-vectors (Liana Hadarean, Clark Barrett, Andrew Reynolds, Cesare Tinelli, Morgan Deters), In Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '15) (Martin Davis, Ansgar Fehnker, Annabelle McIver, Andrei Voronkov, eds.), Springer, volume 9450, 2015. (Suva, Fiji) [bibtex] [pdf]
[13] A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings (Tianyi Liang, Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli, Clark Barrett), In Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FroCoS '15) (Carsten Lutz, Silvio Ranise, eds.), Springer, volume 9322, 2015. (Wroclaw, Poland) [bibtex] [pdf] [doi]
[12] Counterexample Guided Quantifier Instantiation for Synthesis in SMT (Andrew Reynolds, Morgan Deters, Viktor Kuncak, Clark Barrett, Cesare Tinelli), In Proceedings of the 27th International Conference on Computer Aided Verification (CAV '15) (Daniel Kroening, Corina S. P\uas\uareanu, eds.), Springer, volume 9206, 2015. (San Francisco, CA) [bibtex] [pdf]
[11] Deciding Local Theory Extensions via E-matching (Kshitij Bansal, Andrew Reynolds, Tim King, Clark Barrett, Thomas Wies), In Proceedings of the 27th International Conference on Computer Aided Verification (CAV '15) (Daniel Kroening, Corina S. P\uas\uareanu, eds.), Springer, volume 9206, 2015. (San Francisco, CA) [bibtex] [pdf]
2014
[10] Leveraging Linear and Mixed Integer Programming for SMT (Tim King, Clark Barrett, Cesare Tinelli), In Proceedings of the 14th International Conference on Formal Methods In Computer-Aided Design (FMCAD '14), FMCAD Inc., 2014. (Lausanne, Switzerland) [bibtex] [pdf]
[9] A Tale of Two Solvers: Eager and Lazy Approaches to Bit-vectors (Liana Hadarean, Clark Barrett, Dejan Jovanović, Cesare Tinelli, Kshitij Bansal), In Proceedings of the 26th International Conference on Computer Aided Verification (CAV '14) (Armin Biere, Roderick Bloem, eds.), Springer, volume 8559, 2014. (Vienna, Austria) [bibtex] [pdf]
[8] A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions (Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark Barrett, Morgan Deters), In Proceedings of the 26th International Conference on Computer Aided Verification (CAV '14) (Armin Biere, Roderick Bloem, eds.), Springer, volume 8559, 2014. (Vienna, Austria) [bibtex] [pdf]
2013
[7] Simplex with Sum of Infeasibilities for SMT (Timothy King, Clark Barrett, Bruno Dutertre), In Proceedings of the 13th International Conference on Formal Methods In Computer-Aided Design (FMCAD '13), FMCAD Inc., 2013. (Portland, Oregon) [bibtex] [pdf]
[6] The Design and Implementation of the Model Constructing Satisfiability Calculus (Dejan Jovanović, Clark Barrett, Leonardo de Moura), In Proceedings of the 13th International Conference on Formal Methods In Computer-Aided Design (FMCAD '13), FMCAD Inc., 2013. (Portland, Oregon) [bibtex] [pdf]
[5] Being Careful about Theory Combination (Dejan Jovanović, Clark Barrett), In Formal Methods in System Design, Springer US, volume 42, 2013. [bibtex] [pdf] [doi]
[4] Quantifier Instantiation Techniques for Finite Model Finding in SMT (Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic, Morgan Deters, Clark Barrett), In Proceedings of the 24th International Conference on Automated Deduction (CADE '13) (Maria Paola Bonacina, ed.), Springer Berlin Heidelberg, volume 7898, 2013. (Lake Placid, NY) [bibtex] [pdf] [doi]
2011
[3] Sharing is Caring: Combination of Theories (Dejan Jovanović, Clark Barrett), In Proceedings of the 8th International Symposium on Frontiers of Combining Systems (FroCoS '11) (Cesare Tinelli, Viorica Sofronie-Stokkermans, eds.), Springer, volume 6989, 2011. (Saarbrücken, Germany) [bibtex] [pdf]
[2] CVC4 (Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, Cesare Tinelli), In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV '11) (Ganesh Gopalakrishnan, Shaz Qadeer, eds.), Springer, volume 6806, 2011. (Snowbird, Utah) [bibtex] [pdf]
2010
[1] Polite Theories Revisited (Dejan Jovanović, Clark Barrett), In Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '10) (Christian G. Fermüller, Andrei Voronkov, eds.), Springer, volume 6397, 2010. (Yogyakarta, Indonesia) [bibtex] [pdf]
Fork me on GitHub