2026

Journal Articles

Peak: A Single Source Of Truth For Hardware Design And Verification . Caleb Donovick, Jackson Melchert, Ross Daly, Lenny Truong, Priyanka Raina, Pat Hanrahan and Clark Barrett. In ACM Transactions on Embedded Computing Systems, vol. 25, pp. 1-22, ACM. (2026)

Cslib: The Lean Computer Science Library . Clark W. Barrett, Swarat Chaudhuri, Fabrizio Montesi, Jim Grundy, Pushmeet Kohli, Leonardo Moura, Alexandre Rademaker and Sorrachai Yingchareonthawornchai. In CoRR, vol. abs/2602.04846, . (2026)

Conference Papers

Pono 2.0: A versatile SMT-based model checker for safety and liveness (long tool paper). Aron Ricardo Perez-Lopez, Po-Chun Chien, Florian Lonsing, Samantha Archer, Ahmed Irfan and Clark W. Barrett. In Formal methods - 27th international symposium, FM 2026, tokyo, japan, may 18-22, 2026, proceedings, part II, Lecture notes in computer science, pp. 3-26, Springer. (2026)
FM Best Tool Paper Award

Integrating string reasoning in symbolic execution of C programs. Rachel Cleaveland and Clark W. Barrett. In Tools and algorithms for the construction and analysis of systems - 32nd international conference, TACAS 2026, held as part of the international joint conferences on theory and practice of software, ETAPS 2026, turin, italy, april 11-16, 2026, proceedings, part II, Lecture notes in computer science, pp. 151-172, Springer. (2026)

Exploring the SMT-LIB benchmark library. Hans-Jörg Schurr, François Bobot, Mathias Preiner, Aina Niemetz, Clark W. Barrett, Pascal Fontaine and Cesare Tinelli. In Tools and algorithms for the construction and analysis of systems - 32nd international conference, TACAS 2026, held as part of the international joint conferences on theory and practice of software, ETAPS 2026, turin, italy, april 11-16, 2026, proceedings, part I, Lecture notes in computer science, pp. 150-169, Springer. (2026)

VeriStruct: AI-assisted automated verification of data-structure modules in verus. Chuyue Sun, Yican Sun, Daneshvar Amrollahi, Ethan Zhang, Shuvendu K. Lahiri, Shan Lu, David L. Dill and Clark W. Barrett. In Tools and algorithms for the construction and analysis of systems - 32nd international conference, TACAS 2026, held as part of the international joint conferences on theory and practice of software, ETAPS 2026, turin, italy, april 11-16, 2026, proceedings, part II, Lecture notes in computer science, pp. 109-128, Springer. (2026)

Bit-precise interpolation in Bitwuzla. Aina Niemetz and Mathias Preiner. In Tools and algorithms for the construction and analysis of systems - 32nd international conference, TACAS 2026, held as part of the international joint conferences on theory and practice of software, ETAPS 2026, turin, italy, april 11-16, 2026, proceedings, part I, vol. 16505, Lecture notes in computer science, pp. 66-88, Springer. (2026)

Massively parallel bit-precise verification with Bitwuzla and Mallob. Dominik Schreiber, Aina Niemetz and Mathias Preiner. In Tools and algorithms for the construction and analysis of systems - 32nd international conference, TACAS 2026, held as part of the international joint conferences on theory and practice of software, ETAPS 2026, turin, italy, april 11-16, 2026, proceedings, part I, vol. 16505, Lecture notes in computer science, pp. 170-191, Springer. (2026)
ETAPS Best Tool Paper Award
TACAS Distinguished Paper Award
TACAS Distinguished Artifact Award

Lookahead branching for neural network verification. Liam Davis, Duo Zhou, Huan Zhang, Guy Katz, Clark W. Barrett and Haoze Wu. In Proceedings of the thirty-fifth international joint conference on artificial intelligence and the 29th european conference on artificial intelligence, IJCAI/ECAI 2026, bremen, germany, 15-21 august 2026, pp. 518-526, ijcai.org. (2026)

Satisfiability modulo extensional constant arrays. Mathias Preiner, Aina Niemetz and Clark W. Barrett. In Computer aided verification - 38th international conference, CAV 2026, lisbon, portugal, july 26-29, 2026, proceedings, part II, vol. 16683, Lecture notes in computer science, pp. 27-49, Springer. (2026)
CAV Distinguished Paper Award

Automating bitvector and finite field equivalence proofs in lean. Elizaveta Pertseva, Valentin Robert, Clark W. Barrett and James Parker. In Computer aided verification - 38th international conference, CAV 2026, lisbon, portugal, july 26-29, 2026, proceedings, part II, vol. 16683, Lecture notes in computer science, pp. 165-187, Springer. (2026)

The cooperating proof calculus: Comprehensive proofs for an SMT solver. Andrew Reynolds, Hans-Jörg Schurr, Haniel Barbosa, Ofec Israel, Jibiana Jakpor, Hanna Lachnitt, Abdalrhman Mohamed, Aina Niemetz, Mathias Preiner, Yoni Zohar, Robert B. Jones, Clark W. Barrett and Cesare Tinelli. In Computer aided verification - 38th international conference, CAV 2026, lisbon, portugal, july 26-29, 2026, proceedings, part II, vol. 16683, Lecture notes in computer science, pp. 188-212, Springer. (2026)

The termination of nielsen transformations applied to word equations with length constraints. Benjamin Przybocki and Clark W. Barrett. In Automated reasoning - 13th international joint conference, IJCAR 2026, lisbon, portugal, july 26-29, 2026, proceedings, part II, vol. 16689, Lecture notes in computer science, pp. 234-250, Springer. (2026)

Checking regular expressions in Cvc5 proofs. Ofec Israel, Yoni Zohar, Andrew Reynolds, S. Hitarth, Bruno Dutertre, Clark W. Barrett and Cesare Tinelli. In Automated reasoning - 13th international joint conference, IJCAR 2026, lisbon, portugal, july 26-29, 2026, proceedings, part I, vol. 16688, Lecture notes in computer science, pp. 267-275, Springer. (2026)

Ethos: A fast proof checker for the eunoia logical framework. Andrew Reynolds, Hans-Jörg Schurr, Mallku Soldevila, Haniel Barbosa, Clark W. Barrett and Cesare Tinelli. In Automated reasoning - 13th international joint conference, IJCAR 2026, lisbon, portugal, july 26-29, 2026, proceedings, part I, vol. 16688, Lecture notes in computer science, pp. 305-314, Springer. (2026)

Markovian transformers for informative language modeling. Scott Viteri, Max Lamparth, Peter Chatain and Clark W. Barrett. In The fourteenth international conference on learning representations, ICLR 2026, rio de janeiro, brazil, april 23-27, 2026, proceedings.iclr.cc. (2026)

Artificial incorrectness: SMT and LLMs in hardware synthesis. Edward Wang, Joe Walston, Luca Daniel, Tony Tan, Yoni Zohar and Clark W. Barrett. In NASA formal methods - 18th international symposium, NFM 2026, los angeles, CA, USA, may 5-7, 2026, proceedings, vol. 16622, Lecture notes in computer science, pp. 261-284, Springer. (2026)

Parameterized abstract interpretation for transformer verification. Pei Huang, Dennis Wei, Omri Isac, Haoze Wu, Min Wu and Clark W. Barrett. In Fortieth AAAI conference on artificial intelligence, thirty-eighth conference on innovative applications of artificial intelligence, sixteenth symposium on educational advances in artificial intelligence, AAAI 2026, singapore, january 20-27, 2026, pp. 35500-35508, AAAI Press. (2026)

Cubing for tuning. Haoze Wu, Clark W. Barrett and Nina Narodytska. In Fortieth AAAI conference on artificial intelligence, thirty-eighth conference on innovative applications of artificial intelligence, sixteenth symposium on educational advances in artificial intelligence, AAAI 2026, singapore, january 20-27, 2026, pp. 14361-14370, AAAI Press. (2026)

Efficiently computing compact formal explanations. Min Wu, Xiaofu Li, Haoze Wu and Clark W. Barrett. In Fortieth AAAI conference on artificial intelligence, thirty-eighth conference on innovative applications of artificial intelligence, sixteenth symposium on educational advances in artificial intelligence, AAAI 2026, singapore, january 20-27, 2026, pp. 35857-35866, AAAI Press. (2026)

Formalization of a proof calculus for incremental linearization for satisfiability modulo nonlinear arithmetic and transcendental functions. Tomaz Mascarenhas, Harun Khan, Abdalrhman Mohamed, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett and Cesare Tinelli. In Proceedings of the 15th ACM SIGPLAN international conference on certified programs and proofs, CPP 2026, rennes, france, january 12-13, 2026, pp. 216-230, ACM. (2026)

Proof minimization in neural network verification. Omri Isac, Idan Refaeli, Haoze Wu, Clark W. Barrett and Guy Katz. In Verification, model checking, and abstract interpretation - 27th international conference, VMCAI 2026, rennes, france, january 12-13, 2026, proceedings, Lecture notes in computer science, pp. 99-124, Springer. (2026)

2025

Books and Book Chapters

Automated Deduction - Cade 30: Proceedings Of The 30^th International Conference On Automated Deduction . Edited by Clark Barrett and Uwe Waldmann. Lecture notes in artificial intelligence, vol. 15943, Springer. (2025)

Journal Articles

Combining Combination Properties, Part I: Nelson-oppen And Politeness . Guilherme V. Toledo, Yoni Zohar and Clark Barrett. In Journal of Automated Reasoning, vol. 70, Springer. (2025)

Certificates In Ai: Learn But Verify . Clark Barrett, Thomas A Henzinger and Sanjit A Seshia. In Communications of the Association for Computing Machinery (CACM), vol. 69, pp. 66-75, Association for Computing Machinery. (2025)

Interactive Bitvector Reasoning Using Verified Bit-blasting . Henrik Böving, Siddharth Bhat, Luisa Cicolini, Alex Keizer, Léon Frenot, Abdalrhman Mohamed, Léo Stefanesco, Harun Khan, Joshua Clune, Clark Barrett and Tobias Grosser. In Proceedings of the ACM on Programming Languages, vol. 9, pp. 3259-3285, . (2025)

Competitions And Empirical Evaluations In Automated Reasoning (dagstuhl Seminar 25441) . Johannes Klaus Fichte, Matti Järvisalo, Aina Niemetz, Andreas Niskanen and Guido Tack. In Dagstuhl Reports, vol. 15, pp. 135-154, . (2025)

Bounded Verification For Finite-field-blasting In A Compiler For Zero Knowledge Proofs . Alex Ozdemir, Riad S. Wahby, Fraser Brown and Clark Barrett. In Formal Methods in System Design, vol. 67, pp. 161-188, Springer. (2025)

Conference Papers

Automated translation validation of a compiler for statically scheduled accelerators. Jackson Melchert, Caleb Terrill, Áron Ricardo Perez-Lopez, Clark Barrett and Priyanka Raina. In Proceedings of the 25^th international conference on formal methods in computer-aided design (FMCAD’25), pp. 198-208, TU Wien Academic Press. (2025)

Solving set constraints with comprehensions and bounded quantifiers. Mudathir Mohamed, Nick Feng, Andrew Reynolds, Cesare Tinelli, Clark Barrett and Marsha Chechik. In Proceedings of the 25^th international conference on formal methods in computer-aided design (FMCAD’25), pp. 104-114, TU Wien Academic Press. (2025)

Per-instance subproblem generation for strategy selection in SMT. Amalee Wilson, Nina Narodytska, Clark Barrett and Haoze Wu. In Proceedings of the 25^th international conference on formal methods in computer-aided design (FMCAD’25), pp. 94-103, TU Wien Academic Press. (2025)

Towards SMT solver stability via input normalization. Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz, Andrew Reynolds, Moses Charikar, Cesare Tinelli and Clark Barrett. In Proceedings of the 25^th international conference on formal methods in computer-aided design (FMCAD’25), pp. 84-93, TU Wien Academic Press. (2025)

Improving the SMT proof reconstruction pipeline in Isabelle/HOL. Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Andrew Reynolds, Jibiana Jakpor, Bruno Andreotti, Clark Barrett, Hans-Joerg Schurr and Cesare Tinelli. In Proceedings of the 16^th international conference on interactive theorem proving (ITP’25), vol. 352, Leibniz international proceedings in informatics (LIPIcs), pp. 26:1-26:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik. (2025)

Bit-precise reasoning with parametric bit-vectors. Zvika Berger, Yoni Zohar, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett and Cesare Tinelli. In Proceedings of the 28^th international conference on theory and applications of satisfiability testing (SAT’25), vol. 341, Leibniz international proceedings in informatics (LIPIcs), pp. 4:1-4:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik. (2025)

A proposal for an OMT extension to SMT-LIB. Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli and Clark Barrett. In Joint proceedings of the 23^rd international workshop on satisfiability modulo theories and the 16th pragmatics of SAT international workshop (SMT’25 and PoS’25), . (2025)

ClassInvGen: Class invariant synthesis using large language models. Chuyue Sun, Viraj Agashe, Saikat Chakraborty, Jubi Taneja, Clark Barrett, David Dill, Xiaokang Qiu and Shuvendu K. Lahiri. In Proceedings of the 2^nd international symposium on AI verification (SAIV’25), pp. 64-96, Springer. (2025)

Lean-SMT: An SMT tactic for discharging proof goals in lean. Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli and Clark Barrett. In Proceedings of the 37^th international conference on computer aided verification (CAV’25), vol. 15931, Lecture notes in computer science, pp. 197-212, Springer. (2025)

Lean-auto: An interface between lean 4 and automated theorem provers. Yicheng Qian, Joshua Clune, Clark Barrett and Jeremy Avigad. In Proceedings of the 37^th international conference on computer aided verification (CAV’25), vol. 15931, Lecture notes in computer science, pp. 175-196, Springer. (2025)

Relational hoare logic for realistically modelled machine code. Denis Mazzucato, Abdalrhman Mohamed, Juneyoung Lee, Clark Barrett, Jim Grundy, John Harrison and Corina S. Păsăreanu. In Proceedings of the 37^th international conference on computer aided verification (CAV’25), vol. 15931, Lecture notes in computer science, pp. 389-413, Springer. (2025)

Integer reasoning modulo different constants in SMT. Elizaveta Pertseva, Alex Ozdemir, Shankara Pailoor, Alp Bassa, Sorawee Porncharoenwase, Işil Dillig and Clark Barrett. In Proceedings of the 37^th international conference on computer aided verification (CAV’25), vol. 15931, Lecture notes in computer science, pp. 339-362, Springer. (2025)

Pantograph: A machine-to-machine interaction interface for advanced theorem proving, high level reasoning, and data extraction in lean 4. Leni Aniva, Chuyue Sun, Brando Miranda, Clark Barrett and Sanmi Koyejo. In Proceedings of the 31^st international conference on tools and algorithms for the construction and analysis of systems (TACAS’25), vol. 15696, Lecture notes in computer science, pp. 104-123, Springer. (2025)

Application of formal methods (SAT/SMT) to the design of constrained codes. Sunil Sudhakaran, Clark Barrett and Mark Horowitz. In Proceedings of design, automation & test in europe conference (DATE’25), IEEE. (2025)

Efficient SAT-based bounded model checking of evolving systems. Sophie Andrews, Matthew Sotoudeh and Clark Barrett. In Proceedings of design, automation & test in europe conference (DATE’25), IEEE. (2025)

2024

Journal Articles

Satisfiability Modulo User Propagators . Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider and Armin Biere. In J. Artif. Intell. Res., vol. 81, pp. 989-1017, . (2024)

Qed And Symbolic Qed: Dramatic Improvements In Pre-silicon Verification And Post-silicon Validation . Keerthikumara Devarajegowda, Florian Lonsing, Mohammad R. Fadiheh, Saranyu Chattopadhyay, David Lin, Srinivas Shashank Nuthakki, Eshan Singh, Clark Barrett, Wolfgang Ecker, Wolfgang Kunz, Yanjing Li, Dominik Stoffel and Subhasish Mitra. In Foundations and Trends in Integrated Circuits and Systems, vol. 3, pp. 51-217, now publishers inc.. (2024)

Conference Papers

SGLang: Efficient execution of structured language model programs. Lianmin Zheng, Liangsheng Yin, Zhiqiang Xie, Chuyue Sun, Jeff Huang, Cody Hao Yu, Shiyi Cao, Christos Kozyrakis, Ion Stoica, Joseph Gonzalez, Clark Barrett and Ying Sheng. In Advances in neural information processing systems 37 (NeurIPS 2024), vol. 37, pp. 62557-62583, Neural Information Processing Systems Foundation, Inc. (NeurIPS). (2024)

Efficiently synthesizing lowest cost rewrite rules for instruction selection. Ross Daly, Caleb Donovick, Caleb Terrill, Jackson Melchert, Priyanka Raina, Clark Barrett and Pat Hanrahan. In Proceedings of the 24^th international conference on formal methods in computer-aided design (FMCAD’24), pp. 8-17, TU Wien Academic Press. (2024)

SMT-d: New strategies for portfolio-based SMT solving. Clark Barrett, Pei-Wei Chen, Byron Cook, Bruno Dutertre, Robert Jones, Nham Le, Andrew Reynolds, Kunal Sheth, Mike Whalen and Chriss Stephens. In Proceedings of the 24^th international conference on formal methods in computer-aided design (FMCAD’24), pp. 39-48, TU Wien Academic Press. (2024)

Formally verifying deep reinforcement learning controllers with lyapunov barrier certificates. Udayan Mandal, Guy Amir, Haoze Wu, Ieva Daukantas, Fletcher Lee Newell, Umberto J. Ravaioli, Baoluo Meng, Michael Durling, Milan Ganai, Tobey Shim, Guy Katz and Clark Barrett. In Proceedings of the 24^th international conference on formal methods in computer-aided design (FMCAD’24), pp. 95-106, TU Wien Academic Press. (2024)

Satisfiability modulo theories: A beginner’s tutorial. Clark Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds and Yoni Zohar. In Proceedings of the 26^th international symposium on formal methods (FM’24), part II, vol. 14934, Lecture notes in computer science, pp. 571-596, Springer Nature Switzerland. (2024)
FM Distinguished Tutorial Paper Award

The nonexistence of unicorns and many-sorted löwenheim–skolem theorems. Benjamin Przybocki, Guilherme Toledo, Yoni Zohar and Clark Barrett. In Proceedings of the 26^th international symposium on formal methods (FM’24), part i, vol. 14933, Lecture notes in computer science, pp. 658-675, Springer Nature Switzerland. (2024)

Robust mean estimation by all means. Reynald Affeldt, Clark Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa and Carsten Schürmann. In Proceedings of the 15^th international conference on interactive theorem proving (ITP 2024), vol. 309, Leibniz international proceedings in informatics (LIPIcs), pp. 39:1-39:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik. (2024)

Safe and reliable training of learning-based aerospace controllers. Udayan Mandal, Guy Amir, Haoze Wu, Ieva Daukantas, Fletcher Lee Newell, Umberto Ravaioli, Baoluo Meng, Michael Durling, Kerianne Hobbs, Milan Ganai, Tobey Shim, Guy Katz and Clark Barrett. In 2024 AIAA DATC/IEEE 43^rd digital avionics systems conference (DASC’24), IEEE. (2024)

Parallel verification for δ-equivalence of neural network quantization. Pei Huang, Yuting Yang, Haoze Wu, Ieva Daukantas, Min Wu, Fuqi Jia and Clark Barrett. In Proceedings of the first international symposium on AI verification (SAIV’24), pp. 78-99, Springer-Verlag. (2024)

Clover: Closed-loop verifiable code generation. Chuyue Sun, Ying Sheng, Oded Padon and Clark Barrett. In Proceedings of the first international symposium on AI verification (SAIV’24), pp. 134-155, Springer-Verlag. (2024)

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 36^th 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 36^th 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 12^th 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 30^th 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)

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, vol. 22, pp. 1-34, . (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)

H₂o: 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 23^rd 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 23^rd 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 23^rd 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 14^th 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 14^th 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 34^th 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 60^th 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 35^th 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 35^th 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 29^th 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)
CAV 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, alghero, italy, july 4-8, 2023, vol. 271, LIPIcs, pp. 8:1-8:13, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. (2023)
SAT 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 26^th 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 28^th 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 24^th 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 24^th 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)

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)

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 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)
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 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)

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)
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 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 Păsăreanu 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)
IJCAR 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)

The Smt Competition 2015-2018 . Tjark Weber, Sylvain Conchon, David Déharbe, Matthias Heizmann, Aina Niemetz and Giles Reger. In J. Satisf. Boolean Model. Comput., vol. 11, pp. 221-259, . (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)
TACAS 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 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)
FMCAD 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)