Also see publications by category

**“E-QED: Electrical Bug Localization during Post-Silicon Validation Enabled by Quick Error Detection and Formal Methods”**

by Eshan Singh, Clark Barrett, and Subhasish Mitra.

*IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems*, 2020, IEEE. under review.

Details.

**“On Solving Quantified Bit-Vectors using Invertibility Conditions”**

by Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli.

*Formal Methods in System Design*, 2020, Springer US. to appear.

Details.

**“Counterexample Guided Inductive Synthesis Modulo Theories” by Alessandro Abate, Haniel Barbosa, Clark Barrett, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, Andrew Reynolds, and Cesare Tinelli, 2020. under review.
Details.
**

**“Verifying Recurrent Neural Networks Using Invariant Inference”**

by Yuval Jacoby, Clark Barrett, and Guy Katz.

In *Proceedings of the 18^th International Symposium on Automated Technology for Verification and Analysis (ATVA '20)*, (Dang Van Hung and Oleg Sokolsky, eds.), Oct. 2020, pp. 57-74.

Details.

**“Towards Verification of Neural Networks for Small Unmanned Aircraft Collision Avoidance”**

by Ahmed Irfan, Kyle D. Julian, Haoze Wu, Clark Barrett, Mykel J. Kochenderfer, Baoluo Meng, and James Lopez.

In *Proceedings of the 39^th Digital Avionics Systems Conference (DASC '20)*, Oct. 2020.

Details.

**“Reductions for Strings and Regular Expressions Revisited”**

by Andrew Reynolds, Andres Nötzli, Clark Barrett, and Cesare Tinelli.

In *Proceedings of the 20^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '20)*, (Alexander Ivrii and Ofer Strichman, eds.), Sep. 2020, pp. 225-235.

Details.

**“Parallelization Techniques for Verifying Neural Networks”**

by Haoze Wu, Alex Ozdemir, Aleksandar Zeljic, Kyle Julian, Ahmed Irfan, Divya Gopinath, Sadjad Fouladi, Guy Katz, Corina Pasareanu, and Clark Barrett.

In *Proceedings of the 20^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '20)*, (Alexander Ivrii and Ofer Strichman, eds.), Sep. 2020, pp. 128-137.

Details.

**“A Theoretical Framework for Symbolic Quick Error Detection”**

by Florian Lonsing, Subhasish Mitra, and Clark Barrett.

In *Proceedings of the 20^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '20)*, (Alexander Ivrii and Ofer Strichman, eds.), Sep. 2020, pp. 26-35.

Details.

**“A-QED Verification of Hardware Accelerators”**

by Eshan Singh, Florian Lonsing, Saranyu Chattopadhyay, Max Strange, Peng Wei, Xiaofan Zhang, Yuan Zhao, Jason Cong, Deming Chen, Zhiru Zhang, Priyankja Raina, Clark Barrett, and Subhasish Mitra.

In *Proceedings of the 57^th Design Automation Conference (DAC '20)*, July 2020.

Details.

**“The Move Prover”**

by Jingyi Emma Zhong, Kevin Cheang, Shaz Qadeer, Wolfgang Grieskamp, Sam Blackshear, Junkil Park, Yoni Zohar, Clark Barrett, and David L. Dill.

In *Proceedings of the 32^nd International Conference on Computer Aided Verification (CAV '20)*, (Shuvendu K. Lahiri and Chao Wang, eds.), July 2020, pp. 137-150.

Details.

**“Politeness for the Theory of Algebraic Datatypes”**

by Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, and Clark Barrett.

In *Proceedings of the 10^th International Joint Conference on Automated Reasoning (IJCAR '20)*, (Nicolas Peltier and Viorica Sofronie-Stokkermans, eds.), July 2020, pp. 238-255.

Details.

**“Creating an Agile Hardware Design Flow”**

by R. Bahr, C. Barrett, N. Bhagdikar, A. Carsello, R. Daly, C. Donovick, D. Durst, K. Fatahalian, K. Feng, P. Hanrahan, T. Hofstee, M. Horowitz, D. Huff, F. Kjolstad, T. Kong, Q. Liu, M. Mann, J. Melchert, A. Nayak, A. Niemetz, G. Nyengele, P. Raina, S. Richardson, R. Setaluri, J. Setter, K. Sreedhar, M. Strange, J. Thomas, C. Torng, L. Truong, N. Tsiskaridze, and K. Zhang.

In *Proceedings of the 57^th Design Automation Conference (DAC '20)*, July 2020.

Details.

**“A Decision Procedure for String to Code Point Conversion”**

by Andrew Reynolds, Andres Nötzli, Clark Barrett, and Cesare Tinelli.

In *Proceedings of the 9^th International Joint Conference on Automated Reasoning (IJCAR '20)*, (Nicolas Peltier and Viorica Sofronie-Stokkermans, eds.), July 2020, pp. 218-237.

Details.

**“Simplifying Neural Networks using Formal Verification”**

by Sumathi Gokulanathan, Alexander Feldsher, Adi Malca, Clark Barrett, and Guy Katz.

In *NASA Formal Methods: 12th International Symposium, (NFM '20)*, (Ritchie Lee, Susmit Jha, and Anastasia Mavridou, eds.), May 2020, pp. 85-93. Moffet Field, California, to appear.

Details.

**“Partial Order Reduction for Deep Bug Finding in Synchronous Hardware”**

by Makai Mann and Clark Barrett.

In *Proceedings of the 26^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '20)*, (Armin Biere and David Parker, eds.), Apr. 2020, pp. 367-386.

Details.

**“Gap-Free Processor Verification by S ^2QED and Property Generation”**

by Keerthikumara Devarajegowda, Mohammad Rahmani Fadiheh, Eshan Singh, Clark Barrett, Subhasish Mitra, Wolfgang Ecker, Dominik Stoffel, and Wolfgang Kunz.

In

Details.

**“Post-silicon validation and debug using symbolic quick error detection”**

by Subhasish Mitra, Clark Barrett, David Lin, and Eshan Singh.

Jan. 2020. Patent No. 10528448.

Details.

**“Integration and Flight Test of Small UAS Detect and Avoid on A Miniaturized Avionics Platform”**

by J. G. Lopez, L. Ren, B. Meng, R. Fisher, J. Markham, M. Figard, R. Evans, R. Evans, R. Spoelhof, M. Rubenstahl, S. Edwards, I. Pedan, and C. Barrett.

In *Proceedings of the 38^th Digital Avionics Systems Conference (DASC '19)*, 2019.

Details.

**“G2SAT: Learning to Generate SAT Formulas”**

by Jiaxuan You, Haoze Wu, Clark Barrett, Raghuram Ramanujan, and Jure Leskovec.

In *Advances in Neural Information Processing Systems 32 (NeurIPS '19)*, (H. Wallach, H. Larochelle, A. Beygelzimer, F. d'Alché-Buc, E. Fox, and R. Garnett, eds.), Dec. 2019, pp. 10552-10563. Vancouver, Canada.

Details.

*Special Issue: Linearity and Special Issue: Selected Extended Papers of NFM 2017* edited by Iliano Cervesato, Maribel Fernandez, Clark Barrett, and Temesghen Kahsai, vol. 63, Springer, Dec. 2019.

Details.

**“Refutation-Based Synthesis in SMT”**

by Andrew Reynolds, Viktor Kuncak, Cesare Tinelli, Clark Barrett, and Morgan Deters.

*Formal Methods in System Design*, vol. 55, no. 2, Dec. 2019, pp. 73-102, Springer US.

Details.

**“Agile SMT-Based Mapping for CGRAs with Restricted Routing Networks”**

by Caleb Donovick, Makai Mann, Clark Barrett, and Pat Hanrahan.

In *Proceedings of the International Conference on ReConFigurable Computing and FPGAs (ReConFig '19)*, (David Andrews, René Cumplido, Claudia Feregrino, and Marco Platzner, eds.), Dec. 2019. Cancun, Mexico.

Details.

**“Unlocking the Power of Formal Hardware Verification with CoSA and Symbolic QED: Invited Paper”**

by Florian Lonsing, Karthik Ganesan, Makai Mann, Srinivasa Shashank Nuthakki, Eshan Singh, Mario Srouji, Yahan Yang, Subhasish Mitra, and Clark Barrett.

In *Proceedings of the International Conference on Computer-Aided Design (ICCAD '19)*, (David Pan, ed.), Nov. 2019. Westminster, Colorado.

Details.

**“Verifying Deep-RL-Driven Systems”**

by Yafim Kazak, Clark Barrett, Guy Katz, and Michael Schapira.

In *Proceedings of the 2019 Workshop on Network Meets AI & ML (NetAI '19)*, Aug. 2019, pp. 83-89. Beijing, China.

Details.

**“Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)”**

by Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark Barrett, and Cesare Tinelli.

In *Proceedings of the Sixth Workshop on Proof eXchange for Theorem Proving (PxTP '19)*, (Giselle Reis and Haniel Barbosa, eds.), Aug. 2019, pp. 18-26. Natal, Brazil.

Details.

**“Towards Bit-Width-Independent Proofs in SMT Solvers”**

by Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark Barrett, and Cesare Tinelli.

In *Proceedings of the 27^th International Conference on Automated Deduction (CADE '19)*, (Pascal Fontaine, ed.), Aug. 2019, pp. 366-384. Natal, Brazil.

Details.

**“Extending SMT Solvers to Higher-Order Logic”**

by Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, and Clark Barrett.

In *Proceedings of the 27^th International Conference on Automated Deduction (CADE '19)*, (Pascal Fontaine, ed.), Aug. 2019, pp. 35-54. Natal, Brazil.

Details.

**“DRAT-based Bit-Vector Proofs in CVC4”**

by Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, and Clark Barrett.

In *Proceedings of the 22^nd International Conference on Theory and Applications of Satisfiability Testing (SAT '19)*, (Mikolá\u{s} Janota and Inês Lynce, eds.), July 2019, pp. 298-305. Lisbon, Portugal.

Details.

**“CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis”**

by Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Cesare Tinelli, and Clark Barrett.

In *Proceedings of the 31^st International Conference on Computer Aided Verification (CAV '19)*, (Isil Dillig and Serdar Tasiran, eds.), July 2019, pp. 74-83. New York, New York.

Details.

**“The Marabou Framework for Verification and Analysis of Deep Neural Networks”**

by Guy Katz, Derek A. Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljic, David L. Dill, Mykel J. Kochenderfer, and Clark Barrett.

In *Proceedings of the 31^st International Conference on Computer Aided Verification (CAV '19)*, (Isil Dillig and Serdar Tasiran, eds.), July 2019, pp. 443-452. New York, New York.

Details.

**“Syntax-Guided Rewrite Rule Enumeration for SMT Solvers”**

by Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark Barrett, and Cesare Tinelli.

In *Proceedings of the 22^nd International Conference on Theory and Applications of Satisfiability Testing (SAT '19)*, (Mikolá\u{s} Janota and Inês Lynce, eds.), July 2019, pp. 279-297. Lisbon, Portugal.

Details.

**“Invertibility Conditions for Floating-Point Formulas”**

by Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli.

In *Proceedings of the 31^st International Conference on Computer Aided Verification (CAV '19)*, (Isil Dillig and Serdar Tasiran, eds.), July 2019, pp. 116-136. New York, New York.

Details.

**“High-Level Abstractions for Simplifying Extended String Constraints in SMT”**

by Andrew Reynolds, Andres Nötzli, Clark Barrett, and Cesare Tinelli.

In *Proceedings of the 31^st International Conference on Computer Aided Verification (CAV '19)*, (Isil Dillig and Serdar Tasiran, eds.), July 2019, pp. 23-42. New York, New York.

Details.

**“Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores: Industrial Case Study”**

by E. Singh, K. Devarajegowda, S. Simon, R. Schnieder, K. Ganesan, M. Fadiheh, D. Stoffel, W. Kunz, C. Barrett, W. Ecker, and S. Mitra.

In *Proceedings of the 2019 Design, Automation and Test in Europe (DATE '19)*, Mar. 2019, pp. 1000-1005. Florence, Italy.

Details.

**“Processor Hardware Security Vulnerabilities and their Detection by Unique Program Execution Checking”**

by M. R. Fadiheh, D. Stoffel, C. Barrett, S. Mitra, and W. Kunz.

In *Proceedings of the 2019 Design, Automation and Test in Europe (DATE '19)*, Mar. 2019, pp. 994-999. Florence, Italy.

Details.

**“Satisfiability Modulo Theories”**

by Clark Barrett and Cesare Tinelli.

In *Handbook of Model Checking*, (Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, eds.), 2018, pp. 305-343.

Details.

**“Logic Bug Detection and Localization Using Symbolic Quick Error Detection”**

by Eshan Singh, David Lin, Clark Barrett, and Subhasish Mitra.

*IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems*, 2018, IEEE.

Details.

**“Reasoning with Finite Sets and Cardinality Constraints in SMT”**

by Kshitij Bansal, Clark Barrett, Andrew Reynolds, and Cesare Tinelli.

*Logical Methods in Computer Science*, vol. 14, no. 4, Nov. 2018.

Details.

**“CoSA: Integrated Verification for Agile Hardware Design”**

by Cristian Mattarei, Makai Mann, Clark Barrett, Ross G. Daly, Dillon Huff, and Pat Hanrahan.

In *Proceedings of the 18^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '18)*, (Nikolaj Bjørner and Arie Gurfinkel, eds.), Oct. 2018, pp. 7-11. Austin, Texas.

Details.

**“DeepSafe: A Data-driven Approach for Assessing Robustness of Neural Networks”**

by Divya Gopinath, Guy Katz, Corina S. P\u{a}s\u{a}reanu, and Clark Barrett.

In *Proceedings of the 16^th International Symposium on Automated Technology for Verification and Analysis (ATVA '18)*, (Shuvendu Lahiri and Chao Wang, eds.), Oct. 2018, pp. 3-19. Los Angeles, California.

Details.

**“Solving Quantified Bit-Vectors using Invertibility Conditions”**

by Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli.

In *Proceedings of the 30^th International Conference on Computer Aided Verification (CAV '18)*, (Hana Chockler and Georg Weissenbacher, eds.), July 2018, pp. 236-255. Oxford, United Kingdom.

Details.

**“Rewrites for SMT Solvers using Syntax-Guided Enumeration”**

by Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Andres Nötzli, Mathia Preiner, Clark Barrett, and Cesare Tinelli.

In *Proceedings of the 26^th International Workshop on Satisfiability Modulo Theories (SMT '18)*, July 2018. Oxford, United Kingdom.

Details.

**“Datatypes with Shared Selectors”**

by Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, and Clark Barrett.

In *Proceedings of the 9^th International Joint Conference on Automated Reasoning (IJCAR '18)*, (Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, eds.), June 2018, pp. 591-608. Oxford, United Kingdom.

Details.

**“EMME: a formal tool for ECMAScript Memory Model Evaluation”**

by Cristian Mattarei, Clark Barrett, Shu-yu Guo, Bradley Nelson, and Ben Smith.

In *Proceedings of the 24^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '18)*, (Dirk Beyer and Marieke Huisman, eds.), Apr. 2018, pp. 55-71. Thessaloniki, Greece.

Details.

**“p4pktgen: Automated Test Case Generation for P4 Programs”**

by Andres Nötzli, Jehandad Khan, Andy Fingerhut, Clark Barrett, and Peter Athanas.

In *Proceedings of the ACM Symposium on SDN Research (SOSR '18)*, Mar. 2018, pp. 5:1-5:7. Los Angeles, California.

Details.

**“Symbolic quick error detection using symbolic initial state for pre-silicon verification”**

by M. R. Fadiheh, J. Urdahl, S. S. Nuthakki, S. Mitra, C. Barrett, D. Stoffel, and W. Kunz.

In *Proceedings of the 2018 Design, Automation and Test in Europe (DATE '18)*, Mar. 2018, pp. 55-60. Dresden, Germany.

Details.

**“Towards Proving the Adversarial Robustness of Deep Neural Networks”**

by Guy Katz, Clark Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer.

In *Proceedings of the First Workshop on Formal Verification of Autonomous Vehicles (FVAV '17)*, (Lukas Bulwahn, Maryam Kamali, and Sven Linker, eds.), Sep. 2017, pp. 19-26. Turin, Italy.

Details.

**“Designing Theory Solvers with Extensions”**

by Andrew Reynolds, Cesare Tinelli, Dejan Jovanovic, and Clark Barrett.

In *Proceedings of the 11^th International Symposium on Frontiers of Combining Systems (FroCoS '17)*, (Clare Dixon and Marcelo Finger, eds.), Sep. 2017, pp. 22-40. Brasilia, Brazil.

Details.

**“Relational Constraint Solving in SMT”**

by Baoluo Meng, Andrew Reynolds, Cesare Tinelli, and Clark Barrett.

In *Proceedings of the 26^th International Conference on Automated Deduction (CADE '17)*, (Leonardo de Moura, ed.), Aug. 2017, pp. 148-165. Gothenburg, Sweden.

Details.

**“SMTCoq: A Plug-In for Integrating SMT Solvers into Coq”**

by Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, and Clark Barrett.

In *Proceedings of the 29^th International Conference on Computer Aided Verification (CAV '17)*, (Rupak Majumdar and Viktor Kuncak, eds.), July 2017, pp. 126-136. Heidelberg, Germany.

Details.

**“E-QED: Electrical Bug Localization During Post-Silicon Validation Enabled by Quick Error Detection and Formal Methods”**

by Eshan Singh, Clark Barrett, and Subhasish Mitra.

In *Proceedings of the 29^th International Conference on Computer Aided Verification (CAV '17)*, (Rupak Majumdar and Viktor Kuncak, eds.), July 2017, pp. 104-125. Heidelberg, Germany.

Details.

**“Scaling up DPLL(T) String Solvers Using Context-Dependent Simplification”**

by Andrew Reynolds, Maverick Woo, Clark Barrett, David Brumley, Tianyi Liang, and Cesare Tinelli.

In *Proceedings of the 29^th International Conference on Computer Aided Verification (CAV '17)*, (Rupak Majumdar and Viktor Kuncak, eds.), July 2017, pp. 453-474. Heidelberg, Germany.

Details.

**“Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks”**

by Guy Katz, Clark Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer.

In *Proceedings of the 29^th International Conference on Computer Aided Verification (CAV '17)*, (Rupak Majumdar and Viktor Kuncak, eds.), July 2017, pp. 97-117. Heidelberg, Germany.

Details.

**“Constraint solving for finite model finding in SMT solvers”**

by Andrew Reynolds, Cesare Tinelli, and Clark Barrett.

*Theory and Practice of Logic Programming*, vol. 17, no. 4, July 2017, pp. 516-558, Cambridge University Press.

Details.

**“NASA Formal Methods: 9th International Symposium, NFM 2017”**

edited by Clark Barrett, Misty Davies, and Temesghen Kahsai, Springer.

May 2017.

Details.

**“Partitioned Memory Models for Program Analysis”**

by Wei Wang, Clark Barrett, and Thomas Wies.

In *Proceedings of the 18^th International Conference on Verification, Model Checking, and Abstract Interpretion (VMCAI '17)*, (Ahmed Bouajjani and David Monniaux, eds.), Jan. 2017, pp. 539-558. Paris, France.

Details.

**“Symbolic Quick Error Detection for Pre-Silicon and Post-Silicon Validation: Frequently Asked Questions”**

by Eshan Singh, David Lin, Clark Barrett, and Subhasish Mitra.

*IEEE Design & Test*, vol. 33, no. 6, Dec. 2016, pp. 55-62, IEEE.

Details.

**“Lazy Proofs for DPLL(T)-Based SMT Solvers”**

by Guy Katz, Clark Barrett, Cesare Tinelli, Andrew Reynolds, and Liana Hadarean.

In *Proceedings of the 16^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '16)*, (Ruzica Piskac and Muralidhar Talupur, eds.), Oct. 2016, pp. 93-100. Mountain View, California.

Details.

**“An Efficient SMT Solver for String Constraints”**

by Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze, Cesare Tinelli, Clark Barrett, and Morgan Deters.

*Formal Methods in System Design*, vol. 48, no. 3, June 2016, pp. 206-234, Springer US.

Details.

**“A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT”**

by Kshitij Bansal, Andrew Reynolds, Clark Barrett, and Cesare Tinelli.

In *Proceedings of the 8^th International Joint Conference on Automated Reasoning (IJCAR '16)*, (Nicola Olivetti and Ashish Tiwari, eds.), June 2016, pp. 82-98. Coimbra, Portugal.

Details.

**“Fine-grained SMT Proofs for the Theory of Fixed-width Bit-vectors”**

by Liana Hadarean, Clark Barrett, Andrew Reynolds, Cesare Tinelli, and Morgan Deters.

In *Proceedings of the 20^th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '15)*, (Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov, eds.), Nov. 2015, pp. 340-355. Suva, Fiji.

Details.

**“A Structured Approach to Post-Silicon Validation and Debug using Symbolic Quick Error Detection”**

by David Lin, Eshan Singh, Clark Barrett, and Subhasish Mitra.

In *Proceedings of the 42^nd International Test Conference (ITC '15)*, Oct. 2015, pp. 1-10. Anaheim, California.

Details.

**“Theory-Aided Model Checking of Concurrent Transition Systems”**

by Guy Katz, Clark Barrett, and David Harel.

In *Proceedings of the 15^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '15)*, Sep. 2015, pp. 81-88. Austin, Texas.

Details.

**“A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings”**

by Tianyi Liang, Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli, and Clark Barrett.

In *Proceedings of the 10^th International Symposium on Frontiers of Combining Systems (FroCoS '15)*, (Carsten Lutz and Silvio Ranise, eds.), Sep. 2015, pp. 135-150. Wroclaw, Poland.

Details.

**“Deciding Local Theory Extensions via E-matching”**

by Kshitij Bansal, Andrew Reynolds, Tim King, Clark Barrett, and Thomas Wies.

In *Proceedings of the 27^th International Conference on Computer Aided Verification (CAV '15)*, (Daniel Kroening and Corina S. P\u{a}s\u{a}reanu, eds.), July 2015, pp. 87-105. San Francisco, California.

Details.

**“Counterexample Guided Quantifier Instantiation for Synthesis in SMT”**

by Andrew Reynolds, Morgan Deters, Viktor Kuncak, Clark Barrett, and Cesare Tinelli.

In *Proceedings of the 27^th International Conference on Computer Aided Verification (CAV '15)*, (Daniel Kroening and Corina S. P\u{a}s\u{a}reanu, eds.), July 2015, pp. 198-216. San Francisco, California.

Details.

**“Cascade (Competition Contribution)”**

by Wei Wang and Clark Barrett.

In *Proceedings of the 21^st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '15)*, (Christel Baier and Cesare Tinelli, eds.), Apr. 2015, pp. 420-422. London, United Kingdom.

Details.

**“Proofs in Satisfiability Modulo Theories”**

by Clark Barrett, Leonardo de Moura, and Pascal Fontaine.

In *All about Proofs, Proofs for All*, vol. 55 of Mathematical Logic and Foundations, (David Delahaye and Bruno Woltzenlogel Paleo, eds.), (London, UK), Jan. 2015, pp. 23-44.

Details.

**“Leveraging Linear and Mixed Integer Programming for SMT”**

by Tim King, Clark Barrett, and Cesare Tinelli.

In *Proceedings of the 14^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '14)*, Oct. 2014, pp. 139-146. Lausanne, Switzerland.

Details.

**“A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions”**

by Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark Barrett, and Morgan Deters.

In *Proceedings of the 26^th International Conference on Computer Aided Verification (CAV '14)*, (Armin Biere and Roderick Bloem, eds.), July 2014, pp. 646-662. Vienna, Austria.

Details.

**“A Tale of Two Solvers: Eager and Lazy Approaches to Bit-vectors”**

by Liana Hadarean, Clark Barrett, Dejan Jovanovic, Cesare Tinelli, and Kshitij Bansal.

In *Proceedings of the 26^th International Conference on Computer Aided Verification (CAV '14)*, (Armin Biere and Roderick Bloem, eds.), July 2014, pp. 680-695. Vienna, Austria.

Details.

**“Problem Solving for the 21st Century: Efficient Solvers for Satisfiability Modulo Theories”**

by Clark Barrett, Daniel Kroening, and Thomas Melham.

London Mathematical Society and Smith Institute for Industrial Mathematics and System Engineering technical report 3, June 2014. Knowledge Transfer Report.

Details.

**“Cascade 2.0”**

by Wei Wang, Clark Barrett, and Thomas Wies.

In *Proceedings of the 15^th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI '14)*, (Kenneth L. McMillan and Xavier Rival, eds.), Jan. 2014, pp. 142-160. San Diego, California.

Details.

**“Quantifier Instantiation Techniques for Finite Model Finding in SMT”**

by Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic, Morgan Deters, and Clark Barrett.

In *Proceedings of the 24^th International Conference on Automated Deduction (CADE '13)*, (Maria Paola Bonacina, ed.), 2013, pp. 377-391. Lake Placid, New York.

Details.

**““Decision Procedures:An Algorithmic Point of View,”**

by Daniel Kroening and Ofer Strichman, Springer-Verlag, 2008” by Clark Barrett.

*Journal of Automated Reasoning*, vol. 51, no. 4, Dec. 2013, pp. 453-456, Springer Netherlands.

Details.

**“The Design and Implementation of the Model Constructing Satisfiability Calculus”**

by Dejan Jovanovic, Clark Barrett, and Leonardo de Moura.

In *Proceedings of the 13^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '13)*, Oct. 2013, pp. 173-180. Portland, Oregon.

Details.

**“Simplex with Sum of Infeasibilities for SMT”**

by Timothy King, Clark Barrett, and Bruno Dutertre.

In *Proceedings of the 13^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '13)*, Oct. 2013, pp. 189-196. Portland, Oregon.

Details.

**“Witness Runs for Counter Machines”**

by Clark Barrett, Stephané Demri, and Morgan Deters.

In *Proceedings of the 9^th International Symposium on Frontiers of Combining Systems (FroCoS '13)*, (Pascal Fontaine, Christophe Ringeissen, and Renate A. Schmidt, eds.), Sep. 2013, pp. 120-150. Nancy, France.

Details.

**“6 Years of SMT-COMP”**

by Clark Barrett, Morgan Deters, Leonardo de Moura, Albert Oliveras, and Aaron Stump.

*Journal of Automated Reasoning*, vol. 50, no. 3, Mar. 2013, pp. 243-277, Springer Netherlands.

Details.

**“Being Careful about Theory Combination”**

by Dejan Jovanovic and Clark Barrett.

*Formal Methods in System Design*, vol. 42, no. 1, Feb. 2013, pp. 67-90, Springer US.

Details.

**“Sharing is Caring: Combination of Theories”**

by Dejan Jovanovic and Clark Barrett.

In *Proceedings of the 8^th International Symposium on Frontiers of Combining Systems (FroCoS '11)*, (Cesare Tinelli and Viorica Sofronie-Stokkermans, eds.), Oct. 2011, pp. 195-210. Saarbrücken, Germany.

Details.

**“Sharing is Caring: Combination of Theories”**

by Dejan Jovanovic and Clark Barrett, Depatrment of Computer Science.

New York University technical report TR2011-940, Oct. 2011.

Details.

**“CVC4”**

by Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, and Cesare Tinelli.

In *Proceedings of the 23^rd International Conference on Computer Aided Verification (CAV '11)*, (Ganesh Gopalakrishnan and Shaz Qadeer, eds.), July 2011, pp. 171-177. Snowbird, Utah.

Details.

**“Exploring and Categorizing Error Spaces using BMC and SMT”**

by Tim King and Clark Barrett.

In *Proceedings of the 9^th International Workshop on Satisfiability Modulo Theories (SMT '11)*, July 2011. Snowbird, Utah.

Details.

**“Polite Theories Revisited”**

by Dejan Jovanovic and Clark Barrett.

In *Proceedings of the 17^th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '10)*, (Christian G. Fermüller and Andrei Voronkov, eds.), Oct. 2010, pp. 402-416. Yogyakarta, Indonesia.

Details.

**“Verifying Low-Level Implementations of High-Level Datatypes”**

by Christopher L. Conway and Clark Barrett.

In *Proceedings of the 22^nd International Conference on Computer Aided Verification (CAV '10)*, (Tayssir Touili, Byron Cook, and Paul Jackson, eds.), July 2010, pp. 306-320. Edinburgh, Scotland.

Details.

**“The SMT-LIB Standard -- Version 2.0”**

by Clark Barrett, Aaron Stump, and Cesare Tinelli.

In *Proceedings of the 8^th International Workshop on Satisfiability Modulo Theories (SMT '10)*, July 2010. Edinburgh, Scotland.

Details.

**“Sharing is Caring”**

by Dejan Jovanovic and Clark Barrett.

In *Proceedings of the 8^th International Workshop on Satisfiability Modulo Theories (SMT '10)*, July 2010. Edinburgh, Scotland.

Details.

**“Design and Results of the 4^th Annual Satisfiability Modulo Theories Competition (SMT-COMP 2008)”**

by Clark Barrett, Morgan Deters, Albert Oliveras, and Aaron Stump, Depatrment of Computer Science.

New York University technical report TR2010-931, July 2010.

Details.

**“Comparing Proof Systems for Linear Real Arithmetic with LFSC”**

by Andrew Reynolds, Liana Hadarean, Cesare Tinelli, Yeting Ge, Aaron Stump, and Clark Barrett.

In *Proceedings of the 8^th International Workshop on Satisfiability Modulo Theories (SMT '10)*, July 2010. Edinburgh, Scotland.

Details.

**“Polite Theories Revisited”**

by Dejan Jovanovic and Clark Barrett, Depatrment of Computer Science.

New York University technical report TR2010-922, Jan. 2010.

Details.

**“Solving Quantified Verification Conditions using Satisfiability Modulo Theories”**

by Yeting Ge, Clark Barrett, and Cesare Tinelli.

*Annals of Mathematics and Artificial Intelligence*, vol. 55, no. 1-2, Feb. 2009, pp. 101-122, Springer.

Details.

**“Satisfiability Modulo Theories”**

by Clark Barrett, Roberto Sebastiani, Sanjit Seshia, and Cesare Tinelli.

In *Handbook of Satisfiability*, vol. 185 of Frontiers in Artificial Intelligence and Applications, (Armin Biere, Marijn J. H. Heule, Hans van Maaren, and Toby Walsh, eds.), Feb. 2009, pp. 825-885.

Details.

**“Design and Results of the 3^rd Annual Satisfiability Modulo Theories Competition (SMT-COMP 2007)”**

by Clark Barrett, Morgan Deters, Albert Oliveras, and Aaron Stump.

Details.

**“Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors”**

by Christopher L. Conway, Dennis Dams, Kedar S. Namjoshi, and Clark Barrett.

In *Proceedings of the 15^th International Static Analysis Symposium (SAS '08)*, (Mara Alpuente and Germán Vidal, eds.), July 2008, pp. 62-77. Valencia, Spain.

Details.

**“Points-to Analysis, Conditional Soundness, and Proving the Absence of Errors”**

by Christopher L. Conway, Dennis Dams, Kedar S. Namjoshi, and Clark Barrett, Depatrment of Computer Science.

New York University technical report TR2008-910, Mar. 2008.

Details.

**“An Abstract Decision Procedure for a Theory of Inductive Data Types”**

by Clark Barrett, Igor Shikanian, and Cesare Tinelli.

*Journal on Satisfiability, Boolean Modeling and Computation*, vol. 3, 2007, pp. 21-46, IOS Press.

Details.

**“Design and Results of the 2^nd Satisfiability Modulo Theories Competition (SMT-COMP 2006)”**

by Clark Barrett, Leonardo de Moura, and Aaron Stump.

Details.

**“CVC3”**

by Clark Barrett and Cesare Tinelli.

In *Proceedings of the 19^th International Conference on Computer Aided Verification (CAV '07)*, (Werner Damm and Holger Hermanns, eds.), July 2007, pp. 298-302. Berlin, Germany.

Details.

**“Solving Quantified Verification Conditions using Satisfiability Modulo Theories”**

by Yeting Ge, Clark Barrett, and Cesare Tinelli.

In *Proceedings of the 21^st International Conference on Automated Deduction (CADE '07)*, (Frank Pfenning, ed.), July 2007, pp. 167-182. Bremen, Germany.

Details.

**“An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types”**

by Clark Barrett, Igor Shikanian, and Cesare Tinelli.

In *Combined Proceedings of the 4^th Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR '06) and the 1^st International Workshop on Probabilistic Automata and Logics (PaUL '06)*, (Byron Cook and Roberto Sebastiani, eds.), June 2007, pp. 23-37. Seattle, Washington.

Details.

**“Splitting on Demand in SAT Modulo Theories”**

by Clark Barrett, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli.

In *Proceedings of the 13^th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '06)*, (Miki Hermann and Andrei Voronkov, eds.), Nov. 2006, pp. 512-526. Phnom Penh, Cambodia.

Details.

**“CASCADE: C Assertion Checker and Deductive Engine”**

by Nikhil Sethi and Clark Barrett.

In *Proceedings of the 18^th International Conference on Computer Aided Verification (CAV '06)*, (Thomas Ball and Robert B. Jones, eds.), Aug. 2006, pp. 166-169. Seattle, Washington.

Details.

**“Splitting on Demand in SAT Modulo Theories”**

by Clark Barrett, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli, Department of Computer Science.

University of Iowa technical report 06-05, Aug. 2006.

Details.

**“Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite”**

by Sean McLaughlin, Clark Barrett, and Yeting Ge.

In *Proceedings of the 3^rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR '05)*, (Alessandro Armando and Alessandro Cimatti, eds.), Jan. 2006, pp. 43-51. Edinburgh, Scotland.

Details.

**“Validating More Loop Optimizations”**

by Ying Hu, Clark Barrett, Benjamin Goldberg, and Amir Pnueli.

In *Proceedings of the 4^th International Workshop on Compiler Optimization meets Compiler Verificaiton (COCV '05)*, (J. Knoop, G.C. Necula, and W. Zimmermann, eds.), Dec. 2005, pp. 69-84. Edinburgh, Scotland.

Details.

**“Translation and Run-Time Validation of Loop Transformations”**

by Lenore Zuck, Amir Pnueli, Benjamin Goldberg, Clark Barrett, Yi Fang, and Ying Hu.

*Formal Methods in System Design*, vol. 27, no. 3, Nov. 2005, pp. 335-360, Springer Netherlands.

Details.

**“Design and Results of the 1^st Satisfiability Modulo Theories Competition (SMT-COMP 2005)”**

by Clark Barrett, Leonardo de Moura, and Aaron Stump.

Details.

**“An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types”**

by Clark Barrett, Igor Shikanian, and Cesare Tinelli, Department of Computer Science.

New York University technical report TR2005-878, Nov. 2005.

Details.

**“An Industrially Effective Environment for Formal Hardware Verification”**

by Carl-Johan H. Seger, Robert B. Jones, John W. O'Leary, Tom Melham, Mark D. Aagaard, Clark Barrett, and Don Syme.

*IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems*, vol. 24, no. 9, Sep. 2005, pp. 1381-1405.

Details.

**“TVOC: A Translation Validator for Optimizing Compilers”**

by Clark Barrett, Yi Fang, Ben Goldberg, Ying Hu, Amir Pnueli, and Lenore Zuck.

In *Proceedings of the 17^th International Conference on Computer Aided Verification (CAV '05)*, (Kousha Etessami and Sriram K. Rajamani, eds.), July 2005, pp. 291-295. Edinburgh, Scotland.

Details.

**“SMT-COMP: Satisfiability Modulo Theories Competition”**

by Clark Barrett, Leonardo de Moura, and Aaron Stump.

In *Proceedings of the 17^th International Conference on Computer Aided Verification (CAV '05)*, (Kousha Etessami and Sriram K. Rajamani, eds.), July 2005, pp. 20-23. Edinburgh, Scotland.

Details.

**“Combining SAT Methods with Non-Clausal Decision Heuristics”**

by Clark Barrett and Jacob Donham.

In *Selected Papers from the Workshops on Disproving and the Second International Workshop on Pragmatics of Decision Procedures (PDPAR '04)*, (Wolfgang Ahrendt, Peter Baumgartner, Hans de Nivelle, Silvio Ranise, and Cesare Tinelli, eds.), July 2005, pp. 3-12. Cork, Ireland.

Details.

**“A Practical Approach to Partial Functions in CVC Lite”**

by Sergey Berezin, Clark Barrett, Igor Shikanian, Marsha Chechik, Arie Gurfinkel, and David L. Dill.

In *Selected Papers from the Workshops on Disproving and the Second International Workshop on Pragmatics of Decision Procedures (PDPAR '04)*, (Wolfgang Ahrendt, Peter Baumgartner, Hans de Nivelle, Silvio Ranise, and Cesare Tinelli, eds.), July 2005, pp. 13-23. Cork, Ireland.

Details.

**“Into the Loops: Practical Issues in Translation Validation for Optimizing Compilers”**

by Benjamin Goldberg, Lenore Zuck, and Clark Barrett.

In *Proceedings of the 3^rd International Workshop on Compiler Optimization meets Compiler Verificaiton (COCV '04)*, (J. Knoop, G.C. Necula, and W. Zimmermann, eds.), May 2005, pp. 53-71. Barcelona, Spain.

Details.

**“Theory and Algorithms for the Generation and Validation of Speculative Loop Optimizations”**

by Ying Hu, Clark Barrett, and Benjamin Goldberg.

In *Proceedings of the 2^nd IEEE International Conference on Software Engineering and Formal Methods (SEFM '04)*, Sep. 2004, pp. 281-289. Beijing, China.

Details.

**“CVC Lite: A New Implementation of the Cooperating Validity Checker”**

by Clark Barrett and Sergey Berezin.

In *Proceedings of the 16^th International Conference on Computer Aided Verification (CAV '04)*, (Rajeev Alur and Doron A. Peled, eds.), July 2004, pp. 515-518. Boston, Massachusetts.

Details.

**“Run-Time Validation of Speculative Optimizations using CVC”**

by Clark Barrett, Benjamin Goldberg, and Lenore Zuck.

In *Proceedings of the 3^rd International Workshop on Run-time Verification (RV '03)*, (Oleg Sokolsky and Mahesh Viswanathan, eds.), Oct. 2003, pp. 89-107. Boulder, Colorado.

Details.

**“A Proof-Producing Boolean Search Engine”**

by Clark Barrett and Sergey Berezin.

In *Proceedings of the 1^st International Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR '03)*, July 2003. Miami, Florida.

Details.

**“Checking Validity of Quantifier-Free Formulas in Combinations of First-Order Theories”**

by Clark W. Barrett.

Ph.D. dissertation, Stanford University, Jan. 2003. Stanford, California.

Details.

**“CVC: A Cooperating Validity Checker”**

by Aaron Stump, Clark W. Barrett, and David L. Dill.

In *Proceedings of the 14^th International Conference on Computer Aided Verification (CAV '02)*, (Ed Brinksma and Kim Guldstrand Larsen, eds.), July 2002, pp. 500-504. Copenhagen, Denmark.

Details.

**“Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF”**

by Aaron Stump, Clark W. Barrett, and David L. Dill.

In *Proceedings of the 3^rd International Workshop on Logical Frameworks and Meta-Languages (LFM '02)*, (Frank Pfenning, ed.), July 2002, pp. 29-41. Copenhagen, Denmark.

Details.

**“Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT”**

by Clark W. Barrett, David L. Dill, and Aaron Stump.

In *Proceedings of the 14^th International Conference on Computer Aided Verification (CAV '02)*, (Ed Brinksma and Kim Guldstrand Larsen, eds.), July 2002, pp. 236-249. Copenhagen, Denmark.

Details.

**“A Generalization of Shostak's Method for Combining Decision Procedures”**

by Clark W. Barrett, David L. Dill, and Aaron Stump.

In *Proceedings of the 4^th International Workshop on Frontiers of Combining Systems (FroCoS '02)*, (Alessandro Armando, ed.), Apr. 2002, pp. 132-146. Santa Margherita Ligure, Italy.

Details.

**“A Decision Procedure for an Extensional Theory of Arrays”**

by Aaron Stump, Clark W. Barrett, David L. Dill, and Jeremy Levitt.

In *Proceedings of the 16^th IEEE Symposium on Logic in Computer Science (LICS '01)*, June 2001, pp. 29-37. Boston, Massachusetts.

Details.

**“A Framework for Cooperating Decision Procedures”**

by Clark W. Barrett, David L. Dill, and Aaron Stump.

In *Proceedings of the 17^th International Conference on Computer-Aided Deduction (CADE '00)*, (David McAllester, ed.), June 2000, pp. 79-97. Pittsburgh, Pennsylvania.

Details.

**“A Decision Procedure for Bit-vector Arithmetic”**

by Clark W. Barrett, David L. Dill, and Jeremy R. Levitt.

In *Proceedings of the 35^th Design Automation Conference (DAC '98)*, June 1998, pp. 522-527. San Francisco, California.

Details.

**“Validity Checking for Combinations of Theories with Equality”**

by Clark W. Barrett, David L. Dill, and Jeremy R. Levitt.

In *Proceedings of the 1^st International Conference on Formal Methods In Computer-Aided Design (FMCAD '96)*, (Mandayam Srivas and Albert Camilleri, eds.), Nov. 1996, pp. 187-201. Palo Alto, California.

Details.

**“Automatic Generation of Invariants in Processor Verification”**

by Jeffrey X. Su, David L. Dill, and Clark W. Barrett.

In *Proceedings of the 1^st International Conference on Formal Methods In Computer-Aided Design (FMCAD '96)*, (Mandayam Srivas and Albert Camilleri, eds.), Nov. 1996, pp. 377-388. Palo Alto, California.

Details.

(This webpage was created with bibtex2web.)