# 2022

## Journal Articles

Scalable Verification Of Gnn-based Job Schedulers . Haoze Wu, Clark Barrett, Mahmood Sharif, Nina Narodytska and Gagandeep Singh. In Proceedings of the ACM on Programming Languages, vol. 6, pp. 1036-1065, . (2022)

Counterexample-guided Prophecy For Model Checking Modulo The Theory Of Arrays . Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon and Clark Barrett. In Logical Methods in Computer Science, vol. 18, . (2022)

Polite Combination Of Algebraic Datatypes . Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine and Clark Barrett. In Journal of Automated Reasoning, vol. 66, pp. 331-335, Springer. (2022)

**Aha: An Agile Approach To The Design Of Course-grained Reconfigurable Accelerators And Compilers ** . Kalhan Koul, Jackson Melchert, Kavya Sreedhar, Leonard Truong, Gedeon Nyengele, Keyi Zhang, Qiaoyi Liu, Jeff Setter, Po-Han Chen, Yuchen Mei, Maxwell Strange, Ross Daly, Caleb Donovick, Alex Carsello, Taeyoung Kong, Kathleen Feng, Dillon Huff, Ankita Nayak, Rajsekhar Setaluri, James Thomas, Nikhil Bhagdikar, David Durst, Zachary Myers, Nestan Tsiskaridze, Stephen Richardson, Rick Bahr, Kayvon Fatahalian, Pat Hanrahan, Clark Barrett, Mark Horowitz, Christopher Torng, Fredrik Kjolstad and Priyanka Raina. In ACM Transactions on Embedded Computing Systems, . (2022)

## Conference Papers

An abstraction-refinement approach to verifying convolutional neural networks. Matan Ostrovsky, Clark Barrett and Guy Katz. In Proceedings of the 20^{th} international symposium on automated technology for verification and analysis (ATVA’22), vol. 13505, Lecture notes in computer science, pp. 391-396, Springer International Publishing. (2022)

Synthesizing instruction selection rewrite rules from RTL using SMT. Ross Daly, Caleb Donovick, Jackson Melchert, Rajsekhar Setaluri, Nestan Tsiskaridze, Priyanka Raina, Clark Barrett and Pat Hanrahan. In Proceedings of the 22^{nd} international conference on formal methods in computer-aided design (FMCAD’22), pp. 139-150, TU Wien Academic Press. (2022)

Reconstructing fine-grained proofs of rewrites using a domain-specific language. Andres Nötzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett and Cesare Tinelli. In Proceedings of the 22^{nd} international conference on formal methods in computer-aided design (FMCAD’22), pp. 65-74, TU Wien Academic Press. (2022)

Proof-stitch: Proof combination for divide-and-conquer SAT solvers. Abhishek Nair, Saranyu Chattopadhyay, Haoze Wu, Alex Ozdemir and Clark Barrett. In Proceedings of the 22^{nd} international conference on formal methods in computer-aided design (FMCAD’22), pp. 84-88, TU Wien Academic Press. (2022)

On optimizing back-substitution methods for neural network verification. Tom Zelazny, Haoze Wu, Clark Barrett and Guy Katz. In Proceedings of the 22^{nd} international conference on formal methods in computer-aided design (FMCAD’22), pp. 17-26, TU Wien Academic Press. (2022)

Neural network verification with proof production. Omri Isac, Clark Barrett, Min Zhang and Guy Katz. In Proceedings of the 22^{nd} international conference on formal methods in computer-aided design (FMCAD’22), pp. 38-48, TU Wien Academic Press. (2022)

Reasoning about vectors using an SMT theory of sequences. Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark Barrett and Cesare Tinelli. In Proceedings of the 11^{th} international joint conference on automated reasoning (IJCAR’22), vol. 13385, Lecture notes in computer science, pp. 125-143, Springer Nature. (2022)

Cooperating techniques for solving nonlinear real arithmetic in the cvc5 SMT solver (system description). Gereon Kremer, Andrew Reynolds, Clark Barrett and Cesare Tinelli. In Proceedings of the 11^{th} international joint conference on automated reasoning (IJCAR’22), vol. 13385, Lecture notes in computer science, pp. 95-105, Springer Nature. (2022)

Flexible proof production in an industrial-strength SMT solver. Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli and Clark Barrett. In Proceedings of the 11^{th} international joint conference on automated reasoning (IJCAR’22), vol. 13385, Lecture notes in computer science, pp. 15-35, Springer Nature. (2022)

Even faster conflicts and lazier reductions for string solvers. Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Clark Barrett and Cesare Tinelli. In Proceedings of the 34^{th} international conference on computer aided verification (CAV’22), vol. 13372, Lecture notes in computer science, pp. 205-226, Springer. (2022)

Murxla: A modular and highly extensible API fuzzer for SMT solvers. Aina Niemetz, Mathias Preiner and Clark Barrett. In Proceedings of the 34^{th} international conference on computer aided verification (CAV’22), vol. 13372, Lecture notes in computer science, pp. 92-106, Springer. (2022)

cvc5: A versatile and industrial-strength SMT solver. Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli and Yoni Zohar. In Proceedings of the 28^{th} international conference on tools and algorithms for the construction and analysis of systems (TACAS’22), vol. 13243, Lecture notes in computer science, pp. 415-442, Springer. (2022)
**Best SCP Tool Paper Award.**

Efficient neural network analysis with sum-of-infeasibilities. Haoze Wu, Aleksandar Zeljić, Guy Katz and Clark Barrett. In Proceedings of the 28^{th} international conference on tools and algorithms for the construction and analysis of systems (TACAS’22), vol. 13243, Lecture notes in computer science, pp. 143-163, Springer. (2022)

Bit-precise reasoning via int-blasting. Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Clark Barrett and Cesare Tinelli. In Proceedings of the 23^{rd} international conference on verification, model checking, and abstract interpretion (VMCAI ‘22), vol. 13182, Lecture notes in computer science, pp. 496-518, Springer. (2022)

# 2021

## Books and Book Chapters

Satisfiability Modulo Theories . Clark Barrett, Roberto Sebastiani, Sanjit Seshia and Cesare Tinelli. In Handbook of satisfiability, second edition, vol. 336, Frontiers in artificial intelligence and applications, (Armin Biere, Marijn J. H. Heule, Hans Maaren and Toby Walsh, eds.), pp. 825-885, IOS Press. (2021)

## Journal Articles

Towards Satisfiability Modulo Parametric Bit-vectors . Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark Barrett and Cesare Tinelli. In Journal of Automated Reasoning, vol. 65, pp. 1001-1025, Springer. (2021)

Global Optimization Of Objective Functions Represented By Relu Networks . Christopher A. Strong, Haoze Wu, Aleksandar Zeljić, Kyle D. Julian, Guy Katz, Clark Barrett and Mykel J. Kochenderfer. In Machine Learning, Springer. (2021)

Reluplex: A Calculus For Reasoning About Deep Neural Networks . Guy Katz, Clark Barrett, David L. Dill, Kyle Julian and Mykel J. Kochenderfer. In Formal Methods in System Design, Springer. (2021)

Algorithms For Verifying Deep Neural Networks . Changliu Liu, Tomer Arnon, Christopher Lazarus, Christopher Strong, Clark Barrett and Mykel J. Kochenderfer. In Foundations and Trends in Optimization, vol. 4, pp. 244-404, now publishers. (2021)

On Solving Quantified Bit-vectors Using Invertibility Conditions . Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett and Cesare Tinelli. In Formal Methods in System Design, vol. 57, pp. 87-115, Springer US. (2021)

## Conference Papers

Automating system configuration. Nestan Tsiskaridze, Maxwell Strange, Makai Mann, Kavya Sreedhar, Qiaoyi Liu, Mark Horowitz and Clark Barrett. In Proceedings of the 21^{st} international conference on formal methods in computer-aided design (FMCAD’21), pp. 102-111, TU Wien Academic Press. (2021)

Scaling up hardware accelerator verification using A-QED with functional decomposition. Saranyu Chattopadhyay, Florian Lonsing, Luca Piccolboni, Deepraj Soni, Peng Wei, Xiaofan Zhang, Yuan Zhou, Luca Carloni, Deming Chen, Jason Cong, Ramesh Karri, Zhiru Zhang, Caroline Trippel, Clark Barrett and Subhasish Mitra. In Proceedings of the 21^{st} international conference on formal methods in computer-aided design (FMCAD’21), pp. 42-52, TU Wien Academic Press. (2021)

SAT solving in the serverless cloud. Alex Ozdemir, Haoze Wu and Clark Barrett. In Proceedings of the 21^{st} international conference on formal methods in computer-aided design (FMCAD’21), pp. 241-245, TU Wien Academic Press. (2021)

DeepCert: Verification of contextually relevant robustness for neural network image classifiers. Colin Paterson, Haoze Wu, John Grese, Radu Calinescu, Corina S. Păsăreanu and Clark Barrett. In Computer safety, reliability, and security (SAFECOMP ‘21), vol. 12852, Lecture notes in computer science, pp. 3-17, Springer International Publishing. (2021)

Pono: A flexible and extensible SMT-based model checker. Makai Mann, Ahmed Irfan, Florian Lonsing, Yahan Yang, Hongce Zhang, Kristopher Brown, Aarti Gupta and Clark Barrett. In Proceedings of the 33^{rd} international conference on computer aided verification (CAV’21), vol. 12760, Lecture notes in computer science, pp. 461-474, Springer International Publishing. (2021)

Politeness and stable infiniteness: Stronger together. Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark Barrett and Cesare Tinelli. In Proceedings of the 28^{th} international conference on automated deduction (CADE’21), vol. 12699, Lecture notes in artificial intelligence, pp. 148-165, Springer. (2021)

Smt-switch: A solver-agnostic C++ API for SMT solving. Makai Mann, Amalee Wilson, Yoni Zohar, Lindsey Stuntz, Ahmed Irfan, Kristopher Brown, Caleb Donovick, Allison Guman, Cesare Tinelli and Clark Barrett. In Proceedings of the 24^{th} international conference on theory and applications of satisfiability testing (SAT’21), vol. 12831, Lecture notes in computer science, pp. 377-386, Springer. (2021)

ddSMT 2.0: Better delta debugging for the SMT-LIBv2 language and friends. Gereon Kremer, Aina Niemetz and Mathias Preiner. In Computer aided verification - 33rd international conference, CAV 2021, virtual event, july 20-23, 2021, proceedings, part II, vol. 12760, Lecture notes in computer science, pp. 231-242, Springer. (2021)

MachSMT: A machine learning-based algorithm selector for SMT solvers. Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati and Vijay Ganesh. In Tools and algorithms for the construction and analysis of systems - 27th international conference, TACAS 2021, held as part of the european joint conferences on theory and practice of software, ETAPS 2021, luxembourg city, luxembourg, march 27 - april 1, 2021, proceedings, part II, vol. 12652, Lecture notes in computer science, pp. 303-325, Springer. (2021)

Counterexample-guided prophecy for model checking modulo the theory of arrays. Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon and Clark Barrett. In Proceedings of the 27^{th} international conference on tools and algorithms for the construction and analysis of systems (TACAS’21), vol. 12651, Lecture notes in computer science, pp. 113-132, Springer. (2021)

Syntax-guided quantifier instantiation. Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett and Cesare Tinelli. In Proceedings of the 27^{th} international conference on tools and algorithms for the construction and analysis of systems (TACAS’21), vol. 12652, Lecture notes in computer science, pp. 145-163, Springer. (2021)

An SMT-based approach for verifying binarized neural networks. Guy Amir, Haoze Wu, Clark Barrett and Guy Katz. In Proceedings of the 27^{th} international conference on tools and algorithms for the construction and analysis of systems (TACAS’21), vol. 12652, Lecture notes in computer science, pp. 203-222, Springer. (2021)

## Reports

Effective Pre-silicon Verification Of Processor Cores By Breaking The Bounds Of Symbolic Quick Error Detection . Karthik Ganesan, Florian Lonsing, Srinivasa Shashank Nuthakki, Eshan Singh, Mohammad Rahmani Fadiheh, Wolfgang Kunz, Dominik Stoffel, Clark Barrett and Subhasish Mitra. (2021)

## Theses

Augmenting Transition Systems For Scalable Symbolic Model Checking . Makai Mann. PhD thesis, Stanford University. (2021)

Towards Better Simplifications In Smt Solvers With Applications In String Solving . Andres Nötzli. PhD thesis, Stanford University. (2021)

# 2020

## Conference Papers

Towards verification of neural networks for small unmanned aircraft collision avoidance. 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), . (2020)

Verifying recurrent neural networks using invariant inference. Yuval Jacoby, Clark Barrett and Guy Katz. In Proceedings of the 18^{th} international symposium on automated technology for verification and analysis (ATVA’20), vol. 12302, Lecture notes in computer science, pp. 57-74, Springer International Publishing. (2020)

Reductions for strings and regular expressions revisited. 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), pp. 225-235, TU Wien Academic Press. (2020)

Parallelization techniques for verifying neural networks. Haoze Wu, Alex Ozdemir, Aleksandar Zeljić, 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), pp. 128-137, TU Wien Academic Press. (2020)

A theoretical framework for symbolic quick error detection. Florian Lonsing, Subhasish Mitra and Clark Barrett. In Proceedings of the 20^{th} international conference on formal methods in computer-aided design (FMCAD’20), pp. 26-35, TU Wien Academic Press. (2020)

Ternary propagation-based local search for more bit-precise reasoning. Aina Niemetz and Mathias Preiner. In 2020 formal methods in computer aided design, FMCAD 2020, haifa, israel, september 21-24, 2020, pp. 214-224, IEEE. (2020)

Fault: A python embedded domain-specific language for metaprogramming portable hardware verification components. Lenny Truong, Steven Herbst, Rajsekhar Setaluri, Makai Mann, Ross Daly, Keyi Zhang, Caleb Donovick, Daniel Stanley, Mark Horowitz, Clark Barrett and Pat Hanrahan. In Proceedings of the 32^{nd} international conference on computer aided verification (CAV’20), vol. 12224, Lecture notes in computer science, pp. 403-414, Springer International Publishing. (2020)

The move prover. 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), vol. 12224, Lecture notes in computer science, pp. 137-150, Springer International Publishing. (2020)

Creating an agile hardware design flow. 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), Association for Computing Machinery. (2020)

A-QED verification of hardware accelerators. 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), Association for Computing Machinery. (2020)

Politeness for the theory of algebraic datatypes. 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), vol. 12166, Lecture notes in computer science, pp. 238-255, Springer International Publishing. (2020)
**Best paper award.**

A decision procedure for string to code point conversion. Andrew Reynolds, Andres Nötzli, Clark Barrett and Cesare Tinelli. In Proceedings of the 9^{th} international joint conference on automated reasoning (IJCAR’20), vol. 12166, Lecture notes in computer science, pp. 218-237, Springer International Publishing. (2020)

Smt-switch: A solver-agnostic c++ API for SMT solving (extended abstract). Makai Mann, Amalee Wilson, Cesare Tinelli and Clark Barrett. In Proceedings of the 18^{th} international workshop on satisfiability modulo theories (SMT’20), . (2020)

Simplifying neural networks using formal verification. Sumathi Gokulanathan, Alexander Feldsher, Adi Malca, Clark Barrett and Guy Katz. In NASA formal methods: 12th international symposium, (NFM’20), Lecture notes in computer science, pp. 85-93, Springer. (2020)

Partial order reduction for deep bug finding in synchronous hardware. 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), vol. 12078, Lecture notes in computer science, pp. 367-386, Springer. (2020)

Gap-free processor verification by S$^2$QED and property generation. Keerthikumara Devarajegowda, Mohammad Rahmani Fadiheh, Eshan Singh, Clark Barrett, Subhasish Mitra, Wolfgang Ecker, Dominik Stoffel and Wolfgang Kunz. In Proceedings of the 2020 design, automation and test in europe (DATE’20), pp. 526-531, IEEE. (2020)

## Reports

Global Optimization Of Objective Functions Represented By Relu Networks . Christopher A. Strong, Haoze Wu, Aleksandar Zeljić, Kyle D. Julian, Guy Katz, Clark Barrett and Mykel J. Kochenderfer. (2020)

Resources: A Safe Language Abstraction For Money . Sam Blackshear, David L. Dill, Shaz Qadeer, Clark W. Barrett, John C. Mitchell, Oded Padon and Yoni Zohar. (2020)

# 2019

## Books and Book Chapters

Special Issue: Linearity And Special Issue: Selected Extended Papers Of Nfm 2017 . Edited by Iliano Cervesato, Maribel Fernandez, Clark Barrett and Temesghen Kahsai. Journal of automated reasoning, vol. 63, Springer. (2019)

Proceedings Of Formal Methods In Computer-aided Design, Fmcad 2019 . Edited by Clark Barrett and Jin Yang. FMCAD Inc.. (2019)

## Journal Articles

Refutation-based Synthesis In Smt . Andrew Reynolds, Viktor Kuncak, Cesare Tinelli, Clark Barrett and Morgan Deters. In Formal Methods in System Design, vol. 55, pp. 73-102, Springer US. (2019)

## Conference Papers

Agile SMT-based mapping for CGRAs with restricted routing networks. Caleb Donovick, Makai Mann, Clark Barrett and Pat Hanrahan. In Proceedings of the international conference on ReConFigurable computing and FPGAs (ReConFig ‘19), IEEE. (2019)

G2SAT: Learning to generate SAT formulas. Jiaxuan You, Haoze Wu, Clark Barrett, Raghuram Ramanujan and Jure Leskovec. In Advances in neural information processing systems 32 (NeurIPS’19), pp. 10552-10563, Curran Associates, Inc.. (2019)

Unlocking the power of formal hardware verification with CoSA and symbolic QED: Invited paper. 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), IEEE. (2019)

Integration and flight test of small UAS detect and avoid on a miniaturized avionics platform. 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)

Towards bit-width-independent proofs in SMT solvers. 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), vol. 11716, Lecture notes in artificial intelligence, pp. 366-384, Springer. (2019)

Extending SMT solvers to higher-order logic. 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), vol. 11716, Lecture notes in artificial intelligence, pp. 35-54, Springer. (2019)

Verifying bit-vector invertibility conditions in coq (extended abstract). 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), vol. 301, Electronic proceedings in theoretical computer science, pp. 18-26, . (2019)

Verifying deep-RL-driven systems. Yafim Kazak, Clark Barrett, Guy Katz and Michael Schapira. In Proceedings of the 2019 workshop on network meets AI & ML (NetAI’19), pp. 83-89, Association for Computing Machinery. (2019)

Syntax-guided rewrite rule enumeration for SMT solvers. 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), vol. 11628, Lecture notes in computer science, pp. 279-297, Springer. (2019)

DRAT-based bit-vector proofs in CVC4. 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), vol. 11628, Lecture notes in computer science, pp. 298-305, Springer. (2019)

High-level abstractions for simplifying extended string constraints in SMT. Andrew Reynolds, Andres Nötzli, Clark Barrett and Cesare Tinelli. In Proceedings of the 31^{st} international conference on computer aided verification (CAV’19), vol. 11561, Lecture notes in computer science, pp. 23-42, Springer International Publishing. (2019)

CVC4SY: Smart and fast term enumeration for syntax-guided synthesis. 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), vol. 11561, Lecture notes in computer science, pp. 74-83, Springer International Publishing. (2019)

Invertibility conditions for floating-point formulas. 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), vol. 11561, Lecture notes in computer science, pp. 116-136, Springer International Publishing. (2019)

The marabou framework for verification and analysis of deep neural networks. Guy Katz, Derek A. Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljić, David L. Dill, Mykel J. Kochenderfer and Clark Barrett. In Proceedings of the 31^{st} international conference on computer aided verification (CAV’19), vol. 11561, Lecture notes in computer science, pp. 443-452, Springer International Publishing. (2019)

Processor hardware security vulnerabilities and their detection by unique program execution checking. 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), pp. 994-999, IEEE. (2019)

Symbolic QED pre-silicon verification for automotive microcontroller cores: Industrial case study. 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), pp. 1000-1005, IEEE. (2019)

# 2018

## Books and Book Chapters

Satisfiability Modulo Theories . Clark Barrett and Cesare Tinelli. In Handbook of model checking, (Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith and Roderick Bloem, eds.), pp. 305-343, Springer International Publishing. (2018)

## Journal Articles

Reasoning With Finite Sets And Cardinality Constraints In Smt . Kshitij Bansal, Clark Barrett, Andrew Reynolds and Cesare Tinelli. In Logical Methods in Computer Science, vol. 14, . (2018)

Logic Bug Detection And Localization Using Symbolic Quick Error Detection . Eshan Singh, David Lin, Clark Barrett and Subhasish Mitra. In IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, IEEE. (2018)

## Conference Papers

CoSA: Integrated verification for agile hardware design. 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), pp. 7-11, FMCAD Inc.. (2018)

DeepSafe: A data-driven approach for assessing robustness of neural networks. Divya Gopinath, Guy Katz, Corina S. Păsăreanu and Clark Barrett. In Proceedings of the 16^{th} international symposium on automated technology for verification and analysis (ATVA’18), vol. 11138, Lecture notes in computer science, pp. 3-19, Springer. (2018)

Solving quantified bit-vectors using invertibility conditions. 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), vol. 10982, Lecture notes in computer science, pp. 236-255, Springer. (2018)

Rewrites for SMT solvers using syntax-guided enumeration. Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Andres Nötzli, Mathias Preiner, Clark Barrett and Cesare Tinelli. In Proceedings of the 16^{th} international workshop on satisfiability modulo theories (SMT’18), . (2018)

Btor2 , BtorMC and boolector 3.0. Aina Niemetz, Mathias Preiner, Clifford Wolf and Armin Biere. In Computer aided verification - 30th international conference, CAV 2018, held as part of the federated logic conference, FloC 2018, oxford, UK, july 14-17, 2018, proceedings, part I, vol. 10981, Lecture notes in computer science, pp. 587-595, Springer. (2018)

Datatypes with shared selectors. 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), vol. 10900, Lecture notes in computer science, pp. 591-608, Springer International Publishing. (2018)

EMME: A formal tool for ECMAScript memory model evaluation. 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), vol. 10806, Lecture notes in computer science, pp. 55-71, Springer. (2018)

Symbolic quick error detection using symbolic initial state for pre-silicon verification. 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), pp. 55-60, IEEE. (2018)

p4pktgen: Automated test case generation for P4 programs. Andres Nötzli, Jehandad Khan, Andy Fingerhut, Clark Barrett and Peter Athanas. In Proceedings of the ACM symposium on SDN research (SOSR’18), pp. 5:1-5:7, ACM. (2018)

## Reports

Toward Scalable Verification For Safety-critical Deep Networks . Lindsey Kuper, Guy Katz, Justin Gottschlich, Kyle Julian, Clark Barrett and Mykel Kochenderfer. (2018)

Provably Minimally-distorted Adversarial Examples . Nicholas Carlini, Guy Katz, Clark Barrett and David L. Dill. (2018)

# 2017

## Books and Book Chapters

Nasa Formal Methods: 9th International Symposium, Nfm 2017 . Edited by Clark Barrett, Misty Davies and Temesghen Kahsai. Lecture notes in computer science, vol. 10227, Springer. (2017)

## Journal Articles

Constraint Solving For Finite Model Finding In Smt Solvers . Andrew Reynolds, Cesare Tinelli and Clark Barrett. In Theory and Practice of Logic Programming, vol. 17, pp. 516-558, Cambridge University Press. (2017)

## Conference Papers

Designing theory solvers with extensions. Andrew Reynolds, Cesare Tinelli, Dejan Jovanović and Clark Barrett. In Proceedings of the 11^{th} international symposium on frontiers of combining systems (FroCoS’17), vol. 10483, Lecture notes in artificial intelligence, pp. 22-40, Springer. (2017)

Towards proving the adversarial robustness of deep neural networks. 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), vol. 257, Electronic proceedings in theoretical computer science, pp. 19-26, . (2017)

Relational constraint solving in SMT. Baoluo Meng, Andrew Reynolds, Cesare Tinelli and Clark Barrett. In Proceedings of the 26^{th} international conference on automated deduction (CADE’17), vol. 10395, Lecture notes in artificial intelligence, pp. 148-165, Springer. (2017)

Reluplex: An efficient SMT solver for verifying deep neural networks. 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), vol. 10426, Lecture notes in computer science, pp. 97-117, Springer. (2017)

E-QED: Electrical bug localization during post-silicon validation enabled by quick error detection and formal methods. Eshan Singh, Clark Barrett and Subhasish Mitra. In Proceedings of the 29^{th} international conference on computer aided verification (CAV’17), vol. 10426, Lecture notes in computer science, pp. 104-125, Springer. (2017)

SMTCoq: A plug-in for integrating SMT solvers into Coq. 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), vol. 10426, Lecture notes in computer science, pp. 126-136, Springer. (2017)

Scaling up DPLL(T) string solvers using context-dependent simplification. 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), vol. 10426, Lecture notes in computer science, pp. 453-474, Springer. (2017)

Partitioned memory models for program analysis. Wei Wang, Clark Barrett and Thomas Wies. In Proceedings of the 18^{th} international conference on verification, model checking, and abstract interpretion (VMCAI ‘17), pp. 539-558, Springer International Publishing. (2017)

# 2016

## Journal Articles

Symbolic Quick Error Detection For Pre-silicon And Post-silicon Validation: Frequently Asked Questions . Eshan Singh, David Lin, Clark Barrett and Subhasish Mitra. In IEEE Design & Test, vol. 33, pp. 55-62, IEEE. (2016)

An Efficient Smt Solver For String Constraints . Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze, Cesare Tinelli, Clark Barrett and Morgan Deters. In Formal Methods in System Design, vol. 48, pp. 206-234, Springer US. (2016)

## Conference Papers

Lazy proofs for DPLL(T)-based SMT solvers. 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), pp. 93-100, FMCAD Inc.. (2016)
**Best paper award.**

A new decision procedure for finite sets and cardinality constraints in SMT. Kshitij Bansal, Andrew Reynolds, Clark Barrett and Cesare Tinelli. In Proceedings of the 8^{th} international joint conference on automated reasoning (IJCAR’16), vol. 9706, Lecture notes in computer science, pp. 82-98, Springer International Publishing. (2016)