Publications 

2024

Conference Papers

Marabou 2.0: A versatile formal analyzer of neural networks. Haoze Wu, Omri Isac, Aleksandar Zeljić, Teruhiro Tagomori, Matthew Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, Pei Huang, Ori Lahav, Min Wu, Min Zhang, Ekaterina Komendantskaya, Guy Katz and Clark Barrett. In Proceedings of the 36th international conference on computer aided verification (CAV’24), vol. 14681, Lecture notes in computer science, pp. 249-264, Springer. (2024)

Split gröbner bases for satisfiability modulo finite fields. Alex Ozdemir, Shankara Pailoor, Alp Bassa, Kostas Ferles, Clark Barrett and Işil Dillig. In Proceedings of the 36th international conference on computer aided verification (CAV’24), vol. 14681, Lecture notes in computer science, pp. 3-25, Springer. (2024)

Generalized optimization modulo theories. Nestan Tsiskaridze, Clark Barrett and Cesare Tinelli. In Proceedings of the 12th international joint conference on automated reasoning (IJCAR’24), vol. 14739, Lecture notes in computer science, pp. 458-479, Springer. (2024)

Scalable bit-blasting with abstractions. Aina Niemetz, Mathias Preiner and Yoni Zohar. In Computer aided verification - 36th international conference, CAV 2024, montreal, QC, canada, july 24-27, 2024, proceedings, part I, vol. 14681, Lecture notes in computer science, pp. 178-200, Springer. (2024)

Lemur: Integrating large language models in automated program verification. Haoze Wu, Clark Barrett and Nina Narodytska. In The twelfth international conference on learning representations (ICLR’24), . (2024)

Verifying SQL queries using theories of tables and relations. Mudathir Mahgoub Yahia Mohamed, Andrew Reynolds, Cesare Tinelli and Clark Barrett. In Proceedings of 25th conference on logic for programming, artificial intelligence and reasoning (LPAR’24), vol. 100, EPiC series in computing, pp. 445-463, EasyChair. (2024)

IsaRare: Automatic verification of SMT rewrites in Isabelle/HOL. Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark Barrett and Cesare Tinelli. In Proceedings of the 30th international conference on tools and algorithms for the construction and analysis of systems (TACAS’24), vol. 14570, Lecture notes in computer science, pp. 311-330, Springer. (2024)

Towards efficient verification of quantized neural networks. Pei Huang, Haoze Wu, Yuting Yang, Ieva Daukantas, Min Wu, Yedi Zhang and Clark Barrett. In Proceedings of the AAAI conference on artificial intelligence (AAAI-24), vol. 38, pp. 21152-21160, . (2024)

2023

Journal Articles

Generating And Exploiting Automated Reasoning Proof Certificates . Haniel Barbosa, Clark Barrett, Byron Cook, Bruno Dutertre, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Cesare Tinelli and Yoni Zohar. In Communications of the Association for Computing Machinery (CACM), vol. 66, pp. 86-95, Association for Computing Machinery. (2023)

Reasoning About Vectors: Satisfiability Modulo A 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 Journal of Automated Reasoning, vol. 67, Springer. (2023)

Combining Stable Infiniteness And (strong) Politeness . Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark Barrett and Cesare Tinelli. In Journal of Automated Reasoning, vol. 67, Springer. (2023)

Synthesising Programs With Non-trivial Constants . Alessandro Abate, Haniel Barbosa, Clark Barrett, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, Andrew Reynolds and Cesare Tinelli. In Journal of Automated Reasoning, vol. 67, Springer. (2023)

Algorithm Selection For Smt . Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati and Vijay Ganesh. In Int. J. Softw. Tools Technol. Transf., vol. 25, pp. 219-239, . (2023)

Identifying And Mitigating The Security Risks Of Generative Ai . Clark Barrett, Brad Boyd, Elie Bursztein, Nicholas Carlini, Brad Chen, Jihye Choi, Amrita Roy Chowdhury, Mihai Christodorescu, Anupam Datta, Soheil Feizi, Kathleen Fisher, Tatsunori Hashimoto, Dan Hendrycks, Somesh Jha, Daniel Kang, Florian Kerschbaum, Eric Mitchell, John Mitchell, Zulfikar Ramzan, Khawaja Shams, Dawn Song, Ankur Taly and Diyi Yang. In Foundations and Trends in Privacy and Security, vol. 6, pp. 1-52, now publishers inc.. (2023)

Conference Papers

VeriX: Towards verified explainability of deep neural networks. Min Wu, Haoze Wu and Clark Barrett. In Advances in neural information processing systems 36 (NeurIPS 2023), vol. 36, pp. 22247-22268, Curran Associates, Inc.. (2023)

Towards optimal caching and model selection for large model inference. Banghua Zhu, Ying Sheng, Lianmin Zheng, Clark Barrett, Michael Jordan and Jiantao Jiao. In Advances in neural information processing systems 36 (NeurIPS 2023), vol. 36, pp. 59062-59094, Curran Associates, Inc.. (2023)

H2o: Heavy-hitter oracle for efficient generative inference of large language models. Zhenyu Zhang, Ying Sheng, Tianyi Zhou, Tianlong Chen, Lianmin Zheng, Ruisi Cai, Zhao Song, Yuandong Tian, Christopher Ré, Clark Barrett, Zhangyang "Atlas" Wang and Beidi Chen. In Advances in neural information processing systems 36 (NeurIPS 2023), vol. 36, pp. 34661-34710, Curran Associates, Inc.. (2023)

A procedure for SyGuS solution fitting via matching and rewrite rule discovery. Abdalrhman Mohamed, Andrew Reynolds, Clark Barrett and Cesare Tinelli. In Proceedings of the 23rd international conference on formal methods in computer-aided design (FMCAD’23), pp. 189-198, TU Wien Academic Press. (2023)

Lightweight online learning for sets of related problems in automated reasoning. Haoze Wu, Christopher Hahn, Florian Matthias Lonsing, Makai Mann, Raghuram Ramanujan and Clark Barrett. In Proceedings of the 23rd international conference on formal methods in computer-aided design (FMCAD’23), pp. 23-33, TU Wien Academic Press. (2023)

Partitioning strategies for distributed SMT solving. Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli and Clark Barrett. In Proceedings of the 23rd international conference on formal methods in computer-aided design (FMCAD’23), pp. 199-208, TU Wien Academic Press. (2023)

Soy: An efficient MILP solver for piecewise-affine systems. Haoze Wu, Min Wu, Dorsa Sadigh and Clark Barrett. In 2023 IEEE/RSJ international conference on intelligent robots and systems (IROS’23), pp. 6281-6288, IEEE. (2023)

Combining finite combination properties: Finite models and busy beavers. Guilherme V. Toledo, Yoni Zohar and Clark Barrett. In Proceedings of the 14th international symposium on frontiers of combining systems (FroCoS’23), vol. 14279, Lecture notes in artificial intelligence, pp. 159-175, Springer. (2023)

Formal verification of bit-vector invertibility conditions in coq. Burak Ekici, Arjun Viswanathan, Yoni Zohar, Cesare Tinelli and Clark Barrett. In Proceedings of the 14th international symposium on frontiers of combining systems (FroCoS’23), vol. 14279, Lecture notes in artificial intelligence, pp. 41-59, Springer. (2023)

DNN verification, reachability, and the exponential function problem. Omri Isac, Yoni Zohar, Clark Barrett and Guy Katz. In 34th international conference on concurrency theory (CONCUR’23), vol. 279, Leibniz international proceedings in informatics (LIPIcs), pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik. (2023)

G-QED: Generalized QED pre-silicon verification beyond non-interfering hardware accelerators. Saranyu Chattopadhyay, Keerthikumara Devarajegowda, Bihan Zhao, Florian Lonsing, Brandon A. D’Agostino, Ioanna Vavelidou, Vijay D. Bhatt, Sebastian Prebeck, Wolfgang Ecker, Caroline Trippel, Clark Barrett and Subhasish Mitra. In Proceedings of the 60th design automation conference (DAC’23), IEEE. (2023)

Bounded verification for finite-field-blasting. Alex Ozdemir, Riad S. Wahby, Fraser Brown and Clark Barrett. In Proceedings of the 35th international conference on computer aided verification (CAV’23), vol. 13965, Lecture notes in computer science, pp. 154-175, Springer. (2023)

Satisfiability modulo finite fields. Alex Ozdemir, Gereon Kremer, Cesare Tinelli and Clark Barrett. In Proceedings of the 35th international conference on computer aided verification (CAV’23), vol. 13965, Lecture notes in computer science, pp. 163-186, Springer. (2023)

Combining combination properties: An analysis of stable infiniteness, convexity, and politeness. Guilherme V. Toledo, Yoni Zohar and Clark Barrett. In Proceedings of the 29th international conference on automated deduction (CADE’23), vol. 14132, Lecture notes in artificial intelligence, pp. 522-541, Springer. (2023)

Bitwuzla. Aina Niemetz and Mathias Preiner. In Computer aided verification - 35th international conference, CAV 2023, paris, france, july 17-22, 2023, proceedings, part II, vol. 13965, Lecture notes in computer science, pp. 3-17, Springer. (2023)
Distinguished Paper Award

IPASIR-UP: User propagators for CDCL. Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider and Armin Biere. In 26th international conference on theory and applications of satisfiability testing, SAT 2023, july 4-8, 2023, alghero, italy, vol. 271, LIPIcs, pp. 8:1-8:13, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. (2023)
Highlighted Paper

Convex bounds on the softmax function with applications to robustness verification. Dennis Wei, Haoze Wu, Min Wu, Pin-Yu Chen, Clark Barrett and Eitan Farchi. In Proceedings of the 26th international conference on artificial intelligence and statistics (AISTATS’23), vol. 206, Proceedings of machine learning research, pp. 6853-6878, PMLR. (2023)

APEX: A framework for automated processing element design space exploration using frequent subgraph analysis. Jackson Melchert, Kathleen Feng, Caleb Donovick, Ross Daly, Ritvik Sharma, Clark Barrett, Mark A. Horowitz, Pat Hanrahan and Priyanka Raina. In Proceedings of the 28th ACM international conference on architectural support for programming languages and operating systems (ASPLOS), volume 3, ASPLOS 2023, pp. 33-45, Association for Computing Machinery. (2023)

Tighter abstract queries in neural network verification. Elazar Cohen, Yizhak Yisrael Elboher, Clark Barrett and Guy Katz. In Proceedings of 24th international conference on logic for programming, artificial intelligence and reasoning (LPAR ‘23), vol. 94, EPiC series in computing, pp. 124-143, EasyChair. (2023)

An interactive SMT tactic in coq using abductive reasoning. Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli and Clark Barrett. In Proceedings of 24th international conference on logic for programming, artificial intelligence and reasoning (LPAR ‘23), vol. 94, EPiC series in computing, pp. 11-22, EasyChair. (2023)

Toward certified robustness against real-world distribution shifts. Haoze Wu, Teruhiro Tagomori, Alexander Robey, Fengjun Yang, Nikolai Matni, George Pappas, Hamed Hassani, Corina Păsăreanu and Clark Barrett. In Proceedings of the 2023 IEEE conference on secure and trustworthy machine learning (SaTML), pp. 537-553, IEEE. (2023)

Reports

Flexgen: High-throughput Generative Inference Of Large Language Models With A Single Gpu . Ying Sheng, Lianmin Zheng, Binhang Yuan, Zhuohan Li, Max Ryabinin, Daniel Y. Fu, Zhiqiang Xie, Beidi Chen, Clark Barrett, Joseph E. Gonzalez, Percy Liang, Christopher Ré, Ion Stoica and Ce Zhang. (2023)

Peak: A Single Source Of Truth For Hardware Design And Verification . Caleb Donovick, Ross Daly, Jackson Melchert, Lenny Truong, Priyanka Raina, Pat Hanrahan and Clark Barrett. (2023)

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)

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, vol. 60, pp. 87-116, Springer. (2022)

Conference Papers

An abstraction-refinement approach to verifying convolutional neural networks. Matan Ostrovsky, Clark Barrett and Guy Katz. In Proceedings of the 20th 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 22nd 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 22nd 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 22nd 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 22nd 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 22nd 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 11th 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 11th 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 11th 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 34th 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 34th 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 28th 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)
SCP Best Tool Paper Award

Efficient neural network analysis with sum-of-infeasibilities. Haoze Wu, Aleksandar Zeljić, Guy Katz and Clark Barrett. In Proceedings of the 28th 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 23rd 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)

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 21st 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 21st 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 21st 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 33rd 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 28th 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 24th 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 27th 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 27th 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)
Nominated for the EATCS Best ETAPS Theory Paper Award

An SMT-based approach for verifying binarized neural networks. Guy Amir, Haoze Wu, Clark Barrett and Guy Katz. In Proceedings of the 27th 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 39th 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 18th 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 20th 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 20th 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 20th 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 32nd 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 32nd 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 57th 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 57th 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 10th 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 9th 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 18th 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 26th 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 38th 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 27th 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 27th 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 22nd 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 22nd 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 31st 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 31st 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 31st 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 31st 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 18th 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 16th 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 30th 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 16th 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 9th 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 24th 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)
Distinguished Artifact Award

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 11th 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 26th 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 29th 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 29th 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 29th 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 29th 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 18th 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 16th 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 8th international joint conference on automated reasoning (IJCAR’16), vol. 9706, Lecture notes in computer science, pp. 82-98, Springer International Publishing. (2016)