Clark W. Barrett
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
150
Venues
29
Active years
1996–2026
Best venue rank
A*
Where they publish
- A*CAV38 papers
- BFMCAD29 papers
- ACADE15 papers
- ATACAS13 papers
- ADATE6 papers
- BLPAR6 papers
- A*AAAI4 papers
- AIJCAR4 papers
- BVMCAI4 papers
- ASAT4 papers
- A*DAC4 papers
- BFM3 papers
- BATVA3 papers
- BITP2 papers
- BCPP1 paper
- A*ICLR1 paper
- AAISTATS1 paper
- A*ASPLOS1 paper
- BCONCUR1 paper
- AIROS1 paper
- A*IJCAI1 paper
- BSAFECOMP1 paper
- AICCAD1 paper
- A*SIGCOMM1 paper
- AITC1 paper
- BTABLEAUX1 paper
- BSAS1 paper
- BSEFM1 paper
- A*LICS1 paper
Papers
150 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2026 | AAAI | Parameterized Abstract Interpretation for Transformer Verification. | Pei Huang, Dennis Wei, Omri Isac, Haoze Wu, Min Wu, Clark W. Barrett |
| 2026 | AAAI | Cubing for Tuning. | Haoze Wu, Clark W. Barrett, Nina Narodytska |
| 2026 | AAAI | Efficiently Computing Compact Formal Explanations. | Min Wu, Xiaofu Li, Haoze Wu, Clark W. Barrett |
| 2026 | CAV | Automating Bitvector and Finite Field Equivalence Proofs in Lean. | Elizaveta Pertseva, Valentin Robert, Clark W. Barrett, James Parker |
| 2026 | CAV | Satisfiability Modulo Extensional Constant Arrays. | Mathias Preiner, Aina Niemetz, Clark W. Barrett |
| 2026 | CAV | The Cooperating Proof Calculus: Comprehensive Proofs for an SMT Solver. | Andrew Reynolds, Hans-Jrg Schurr, Haniel Barbosa, Ofec Israel, Jibiana Jakpor, Hanna Lachnitt, Abdalrhman Mohamed, Aina Niemetz, Mathias Preiner, Yoni Zohar, Robert B. Jones, Clark W. Barrett, Cesare Tinelli |
| 2026 | CPP | 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, Cesare Tinelli |
| 2026 | FM | 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, Clark W. Barrett |
| 2026 | IJCAR | Checking Regular Expressions in Cvc5 Proofs. | Ofec Israel, Yoni Zohar, Andrew Reynolds, S. Hitarth, Bruno Dutertre, Clark W. Barrett, Cesare Tinelli |
| 2026 | IJCAR | The Termination of Nielsen Transformations Applied to Word Equations with Length Constraints. | Benjamin Przybocki, Clark W. Barrett |
| 2026 | IJCAR | Ethos: A Fast Proof Checker for the Eunoia Logical Framework. | Andrew Reynolds, Hans-Jrg Schurr, Mallku Soldevila, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli |
| 2026 | TACAS | Integrating String Reasoning in Symbolic Execution of C Programs. | Rachel Cleaveland, Clark W. Barrett |
| 2026 | TACAS | Exploring the SMT-LIB Benchmark Library. | Hans-Jrg Schurr, Franois Bobot, Mathias Preiner, Aina Niemetz, Clark W. Barrett, Pascal Fontaine, Cesare Tinelli |
| 2026 | TACAS | 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, Clark W. Barrett |
| 2026 | VMCAI | Proof Minimization in Neural Network Verification. | Omri Isac, Idan Refaeli, Haoze Wu, Clark W. Barrett, Guy Katz |
| 2025 | CAV | Relational Hoare Logic for Realistically Modelled Machine Code. | Denis Mazzucato, Abdalrhman Mohamed, Juneyoung Lee, Clark W. Barrett, Jim Grundy, John Harrison, Corina S. Pasareanu |
| 2025 | CAV | 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, Clark W. Barrett |
| 2025 | CAV | Integer Reasoning Modulo Different Constants in SMT. | Elizaveta Pertseva, Alex Ozdemir, Shankara Pailoor, Alp Bassa, Sorawee Porncharoenwase, Isil Dillig, Clark W. Barrett |
| 2025 | CAV | Lean-Auto: An Interface Between Lean 4 and Automated Theorem Provers. | Yicheng Qian, Joshua Clune, Clark W. Barrett, Jeremy Avigad |
| 2025 | DATE | Efficient SAT-Based Bounded Model Checking of Evolving Systems. | Sophie Andrews, Matthew Sotoudeh, Clark W. Barrett |
| 2025 | DATE | Application of Formal Methods (SAT/SMT) to the Design of Constrained Codes. | Sunil Sudhakaran, Clark W. Barrett, Mark Horowitz |
| 2025 | FMCAD | Towards SMT Solver Stability via Input Normalization. | Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz, Andrew Reynolds, Moses Charikar, Cesare Tinelli, Clark W. Barrett |
| 2025 | FMCAD | Automated Translation Validation of a Compiler for Statically Scheduled Accelerators. | Jackson Melchert, Caleb Terrill, Aron Ricardo Perez-Lopez, Clark W. Barrett, Priyanka Raina |
| 2025 | FMCAD | Solving Set Constraints with Comprehensions and Bounded Quantifiers. | Mudathir Mohamed, Nick Feng, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett, Marsha Chechik |
| 2025 | FMCAD | Per-Instance Subproblem Generation for Strategy Selection in SMT. | Amalee Wilson, Nina Narodytska, Clark W. Barrett, Haoze Wu |
| 2025 | ITP | Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL. | Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds, Hans-Jrg Schurr, Clark W. Barrett, Cesare Tinelli |
| 2025 | SAT | Bit-Precise Reasoning with Parametric Bit-Vectors. | Zvika Berger, Yoni Zohar, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2025 | TACAS | 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 W. Barrett, Sanmi Koyejo |
| 2024 | AAAI | Towards Efficient Verification of Quantized Neural Networks. | Pei Huang, Haoze Wu, Yuting Yang, Ieva Daukantas, Min Wu, Yedi Zhang, Clark W. Barrett |
| 2024 | CAV | Split Grbner Bases for Satisfiability Modulo Finite Fields. | Alex Ozdemir, Shankara Pailoor, Alp Bassa, Kostas Ferles, Clark W. Barrett, Isil Dillig |
| 2024 | CAV | Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. | Haoze Wu, Omri Isac, Aleksandar Zeljic, Teruhiro Tagomori, Matthew L. Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, Pei Huang, Ori Lahav, Min Wu, Min Zhang, Ekaterina Komendantskaya, Guy Katz, Clark W. Barrett |
| 2024 | FM | Satisfiability Modulo Theories: A Beginner's Tutorial. | Clark W. Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar |
| 2024 | FM | The Nonexistence of Unicorns and Many-Sorted Lwenheim-Skolem Theorems. | Benjamin Przybocki, Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett |
| 2024 | FMCAD | SMT-D: New Strategies for Portfolio-Based SMT Solving. | Clark W. Barrett, Pei-Wei Chen, Byron Cook, Bruno Dutertre, Robert B. Jones, Nham Le, Andrew Reynolds, Kunal Sheth, Christopher Stephens, Michael W. Whalen |
| 2024 | FMCAD | Efficiently Synthesizing Lowest Cost Rewrite Rules for Instruction Selection. | Ross Daly, Caleb Donovick, Caleb Terrill, Jackson Melchert, Priyanka Raina, Clark W. Barrett, Pat Hanrahan |
| 2024 | FMCAD | 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, Clark W. Barrett |
| 2024 | ICLR | Lemur: Integrating Large Language Models in Automated Program Verification. | Haoze Wu, Clark W. Barrett, Nina Narodytska |
| 2024 | IJCAR | Generalized Optimization Modulo Theories. | Nestan Tsiskaridze, Clark W. Barrett, Cesare Tinelli |
| 2024 | ITP | Robust Mean Estimation by All Means (Short Paper). | Reynald Affeldt, Clark W. Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa, Carsten Schrmann |
| 2024 | LPAR | Verifying SQL queries using theories of tables and relations. | Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett |
| 2024 | TACAS | IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. | Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Ntzli, Clark W. Barrett, Cesare Tinelli |
| 2023 | AISTATS | Convex Bounds on the Softmax Function with Applications to Robustness Verification. | Dennis Wei, Haoze Wu, Min Wu, Pin-Yu Chen, Clark W. Barrett, Eitan Farchi |
| 2023 | ASPLOS | 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 W. Barrett, Mark A. Horowitz, Pat Hanrahan, Priyanka Raina |
| 2023 | CADE | Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness. | Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett |
| 2023 | CAV | Satisfiability Modulo Finite Fields. | Alex Ozdemir, Gereon Kremer, Cesare Tinelli, Clark W. Barrett |
| 2023 | CAV | Bounded Verification for Finite-Field-Blasting - In a Compiler for Zero Knowledge Proofs. | Alex Ozdemir, Riad S. Wahby, Fraser Brown, Clark W. Barrett |
| 2023 | CONCUR | DNN Verification, Reachability, and the Exponential Function Problem. | Omri Isac, Yoni Zohar, Clark W. Barrett, Guy Katz |
| 2023 | DAC | 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 Deep Bhatt, Sebastian Prebeck, Wolfgang Ecker, Caroline Trippel, Clark W. Barrett, Subhasish Mitra |
| 2023 | FMCAD | A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery. | Abdalrhman Mohamed, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2023 | FMCAD | Partitioning Strategies for Distributed SMT Solving. | Amalee Wilson, Andres Ntzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett |
| 2023 | FMCAD | Lightweight Online Learning for Sets of Related Problems in Automated Reasoning. | Haoze Wu, Christopher Hahn, Florian Lonsing, Makai Mann, Raghuram Ramanujan, Clark W. Barrett |
| 2023 | IROS | Soy: An Efficient MILP Solver for Piecewise-Affine Systems. | Haoze Wu, Min Wu, Dorsa Sadigh, Clark W. Barrett |
| 2023 | LPAR | An Interactive SMT Tactic in Coq using Abductive Reasoning. | Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli, Clark W. Barrett |
| 2023 | LPAR | Tighter Abstract Queries in Neural Network Verification. | Elazar Cohen, Yizhak Yisrael Elboher, Clark W. Barrett, Guy Katz |
| 2022 | ATVA | An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks. | Matan Ostrovsky, Clark W. Barrett, Guy Katz |
| 2022 | CADE | Flexible Proof Production in an Industrial-Strength SMT Solver. | Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Ntzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, Clark W. Barrett |
| 2022 | CADE | Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description). | Gereon Kremer, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2022 | CADE | Reasoning About Vectors Using an SMT Theory of Sequences. | Ying Sheng, Andres Ntzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli |
| 2022 | CAV | Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers. | Aina Niemetz, Mathias Preiner, Clark W. Barrett |
| 2022 | CAV | Even Faster Conflicts and Lazier Reductions for String Solvers. | Andres Ntzli, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli |
| 2022 | FMCAD | Synthesizing Instruction Selection Rewrite Rules from RTL using SMT. | Ross Daly, Caleb Donovick, Jackson Melchert, Rajsekhar Setaluri, Nestan Tsiskaridze, Priyanka Raina, Clark W. Barrett, Pat Hanrahan |
| 2022 | FMCAD | Neural Network Verification with Proof Production. | Omri Isac, Clark W. Barrett, Min Zhang, Guy Katz |
| 2022 | FMCAD | Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers. | Abhishek Anil Nair, Saranyu Chattopadhyay, Haoze Wu, Alex Ozdemir, Clark W. Barrett |
| 2022 | FMCAD | Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language. | Andres Ntzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2022 | FMCAD | On Optimizing Back-Substitution Methods for Neural Network Verification. | Tom Zelazny, Haoze Wu, Clark W. Barrett, Guy Katz |
| 2022 | TACAS | 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 Ntzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, Yoni Zohar |
| 2022 | TACAS | Efficient Neural Network Analysis with Sum-of-Infeasibilities. | Haoze Wu, Aleksandar Zeljic, Guy Katz, Clark W. Barrett |
| 2022 | VMCAI | Bit-Precise Reasoning via Int-Blasting. | Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Ntzli, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2021 | CADE | Politeness and Stable Infiniteness: Stronger Together. | Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2021 | CAV | Pono: A Flexible and Extensible SMT-Based Model Checker. | Makai Mann, Ahmed Irfan, Florian Lonsing, Yahan Yang, Hongce Zhang, Kristopher Brown, Aarti Gupta, Clark W. Barrett |
| 2021 | FMCAD | 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 P. Carloni, Deming Chen, Jason Cong, Ramesh Karri, Zhiru Zhang, Caroline Trippel, Clark W. Barrett, Subhasish Mitra |
| 2021 | FMCAD | SAT Solving in the Serverless Cloud. | Alex Ozdemir, Haoze Wu, Clark W. Barrett |
| 2021 | FMCAD | Automating System Configuration. | Nestan Tsiskaridze, Maxwell Strange, Makai Mann, Kavya Sreedhar, Qiaoyi Liu, Mark Horowitz, Clark W. Barrett |
| 2021 | IJCAI | Politeness for the Theory of Algebraic Datatypes (Extended Abstract). | Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett |
| 2021 | SAFECOMP | DeepCert: Verification of Contextually Relevant Robustness for Neural Network Image Classifiers. | Colin Paterson, Haoze Wu, John Grese, Radu Calinescu, Corina S. Pasareanu, Clark W. Barrett |
| 2021 | SAT | 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, Clark W. Barrett |
| 2021 | TACAS | An SMT-Based Approach for Verifying Binarized Neural Networks. | Guy Amir, Haoze Wu, Clark W. Barrett, Guy Katz |
| 2021 | TACAS | Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays. | Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark W. Barrett |
| 2021 | TACAS | Syntax-Guided Quantifier Instantiation. | Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2020 | ATVA | Verifying Recurrent Neural Networks Using Invariant Inference. | Yuval Jacoby, Clark W. Barrett, Guy Katz |
| 2020 | CADE | Politeness for the Theory of Algebraic Datatypes. | Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett |
| 2020 | CADE | A Decision Procedure for String to Code Point Conversion. | Andrew Reynolds, Andres Ntzli, Clark W. Barrett, Cesare Tinelli |
| 2020 | CAV | fault: A Python Embedded Domain-Specific Language for Metaprogramming Portable Hardware Verification Components. | Lenny Truong, Steven Herbst, Rajsekhar Setaluri, Makai Mann, Ross G. Daly, Keyi Zhang, Caleb Donovick, Daniel Stanley, Mark Horowitz, Clark W. Barrett, Pat Hanrahan |
| 2020 | CAV | The Move Prover. | Jingyi Emma Zhong, Kevin Cheang, Shaz Qadeer, Wolfgang Grieskamp, Sam Blackshear, Junkil Park, Yoni Zohar, Clark W. Barrett, David L. Dill |
| 2020 | DAC | Creating an Agile Hardware Design Flow. | Rick Bahr, Clark W. Barrett, Nikhil Bhagdikar, Alex Carsello, Ross Daly, Caleb Donovick, David Durst, Kayvon Fatahalian, Kathleen Feng, Pat Hanrahan, Teguh Hofstee, Mark Horowitz, Dillon Huff, Fredrik Kjolstad, Taeyoung Kong, Qiaoyi Liu, Makai Mann, Jackson Melchert, Ankita Nayak, Aina Niemetz, Gedeon Nyengele, Priyanka Raina, Stephen Richardson, Rajsekhar Setaluri, Jeff Setter, Kavya Sreedhar, Maxwell Strange, James Thomas, Christopher Torng, Leonard Truong, Nestan Tsiskaridze, Keyi Zhang |
| 2020 | DAC | A-QED Verification of Hardware Accelerators. | Eshan Singh, Florian Lonsing, Saranyu Chattopadhyay, Maxwell Strange, Peng Wei, Xiaofan Zhang, Yuan Zhou, Deming Chen, Jason Cong, Priyanka Raina, Zhiru Zhang, Clark W. Barrett, Subhasish Mitra |
| 2020 | DATE | Gap-free Processor Verification by S | Keerthikumara Devarajegowda, Mohammad Rahmani Fadiheh, Eshan Singh, Clark W. Barrett, Subhasish Mitra, Wolfgang Ecker, Dominik Stoffel, Wolfgang Kunz |
| 2020 | FMCAD | A Theoretical Framework for Symbolic Quick Error Detection. | Florian Lonsing, Subhasish Mitra, Clark W. Barrett |
| 2020 | FMCAD | Reductions for Strings and Regular Expressions Revisited. | Andrew Reynolds, Andres Ntzli, Clark W. Barrett, Cesare Tinelli |
| 2020 | FMCAD | Parallelization Techniques for Verifying Neural Networks. | Haoze Wu, Alex Ozdemir, Aleksandar Zeljic, Kyle Julian, Ahmed Irfan, Divya Gopinath, Sadjad Fouladi, Guy Katz, Corina S. Pasareanu, Clark W. Barrett |
| 2020 | TACAS | Partial Order Reduction for Deep Bug Finding in Synchronous Hardware. | Makai Mann, Clark W. Barrett |
| 2019 | CADE | Extending SMT Solvers to Higher-Order Logic. | Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, Clark W. Barrett |
| 2019 | CADE | Towards Bit-Width-Independent Proofs in SMT Solvers. | Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli |
| 2019 | CAV | Invertibility Conditions for Floating-Point Formulas. | Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2019 | CAV | 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 Zeljic, David L. Dill, Mykel J. Kochenderfer, Clark W. Barrett |
| 2019 | CAV | cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis. | Andrew Reynolds, Haniel Barbosa, Andres Ntzli, Clark W. Barrett, Cesare Tinelli |
| 2019 | CAV | High-Level Abstractions for Simplifying Extended String Constraints in SMT. | Andrew Reynolds, Andres Ntzli, Clark W. Barrett, Cesare Tinelli |
| 2019 | DATE | Processor Hardware Security Vulnerabilities and their Detection by Unique Program Execution Checking. | Mohammad Rahmani Fadiheh, Dominik Stoffel, Clark W. Barrett, Subhasish Mitra, Wolfgang Kunz |
| 2019 | DATE | Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores: Industrial Case Study. | Eshan Singh, Keerthikumara Devarajegowda, Sebastian Simon, Ralf Schnieder, Karthik Ganesan, Mohammad Rahmani Fadiheh, Dominik Stoffel, Wolfgang Kunz, Clark W. Barrett, Wolfgang Ecker, Subhasish Mitra |
| 2019 | ICCAD | 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, Clark W. Barrett |
| 2019 | SIGCOMM | Verifying Deep-RL-Driven Systems. | Yafim Kazak, Clark W. Barrett, Guy Katz, Michael Schapira |
| 2019 | SAT | Syntax-Guided Rewrite Rule Enumeration for SMT Solvers. | Andres Ntzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark W. Barrett, Cesare Tinelli |
| 2019 | SAT | DRAT-based Bit-Vector Proofs in CVC4. | Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark W. Barrett |
| 2018 | ATVA | DeepSafe: A Data-Driven Approach for Assessing Robustness of Neural Networks. | Divya Gopinath, Guy Katz, Corina S. Pasareanu, Clark W. Barrett |
| 2018 | CADE | Datatypes with Shared Selectors. | Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, Clark W. Barrett |
| 2018 | CAV | Solving Quantified Bit-Vectors Using Invertibility Conditions. | Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2018 | DATE | Symbolic quick error detection using symbolic initial state for pre-silicon verification. | Mohammad Rahmani Fadiheh, Joakim Urdahl, Srinivasa Shashank Nuthakki, Subhasish Mitra, Clark W. Barrett, Dominik Stoffel, Wolfgang Kunz |
| 2018 | FMCAD | CoSA: Integrated Verification for Agile Hardware Design. | Cristian Mattarei, Makai Mann, Clark W. Barrett, Ross G. Daly, Dillon Huff, Pat Hanrahan |
| 2018 | TACAS | EMME: A Formal Tool for ECMAScript Memory Model Evaluation. | Cristian Mattarei, Clark W. Barrett, Shu-yu Guo, Bradley Nelson, Ben Smith |
| 2017 | CADE | Relational Constraint Solving in SMT. | Baoluo Meng, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett |
| 2017 | CAV | SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. | Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, Clark W. Barrett |
| 2017 | CAV | Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. | Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer |
| 2017 | CAV | Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification. | Andrew Reynolds, Maverick Woo, Clark W. Barrett, David Brumley, Tianyi Liang, Cesare Tinelli |
| 2017 | CAV | E-QED: Electrical Bug Localization During Post-silicon Validation Enabled by Quick Error Detection and Formal Methods. | Eshan Singh, Clark W. Barrett, Subhasish Mitra |
| 2017 | VMCAI | Partitioned Memory Models for Program Analysis. | Wei Wang, Clark W. Barrett, Thomas Wies |
| 2016 | CADE | A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. | Kshitij Bansal, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2016 | FMCAD | Lazy proofs for DPLL(T)-based SMT solvers. | Guy Katz, Clark W. Barrett, Cesare Tinelli, Andrew Reynolds, Liana Hadarean |
| 2015 | CAV | Deciding Local Theory Extensions via E-matching. | Kshitij Bansal, Andrew Reynolds, Tim King, Clark W. Barrett, Thomas Wies |
| 2015 | CAV | Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. | Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett |
| 2015 | FMCAD | Theory-Aided Model Checking of Concurrent Transition Systems. | Guy Katz, Clark W. Barrett, David Harel |
| 2015 | ITC | A structured approach to post-silicon validation and debug using symbolic quick error detection. | David Lin, Eshan Singh, Clark W. Barrett, Subhasish Mitra |
| 2015 | LPAR | Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors. | Liana Hadarean, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli, Morgan Deters |
| 2015 | TACAS | Cascade - (Competition Contribution). | Wei Wang, Clark W. Barrett |
| 2014 | CAV | A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors. | Liana Hadarean, Kshitij Bansal, Dejan Jovanovic, Clark W. Barrett, Cesare Tinelli |
| 2014 | CAV | A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions. | Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett, Morgan Deters |
| 2014 | FMCAD | Leveraging linear and mixed integer programming for SMT. | Tim King, Clark W. Barrett, Cesare Tinelli |
| 2014 | FMCAD | A tour of CVC4: How it works, and how to use it. | Morgan Deters, Andrew Reynolds, Tim King, Clark W. Barrett, Cesare Tinelli |
| 2014 | VMCAI | Cascade 2.0. | Wei Wang, Clark W. Barrett, Thomas Wies |
| 2013 | CADE | Quantifier Instantiation Techniques for Finite Model Finding in SMT. | Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic, Morgan Deters, Clark W. Barrett |
| 2013 | FMCAD | Simplex with sum of infeasibilities for SMT. | Tim King, Clark W. Barrett, Bruno Dutertre |
| 2013 | TABLEAUX | Witness Runs for Counter Machines - (Abstract). | Clark W. Barrett, Stphane Demri, Morgan Deters |
| 2011 | CAV | CVC4. | Clark W. Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, Cesare Tinelli |
| 2010 | CAV | Verifying Low-Level Implementations of High-Level Datatypes. | Christopher L. Conway, Clark W. Barrett |
| 2010 | LPAR | Polite Theories Revisited. | Dejan Jovanovic, Clark W. Barrett |
| 2008 | SAS | Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors. | Christopher L. Conway, Dennis Dams, Kedar S. Namjoshi, Clark W. Barrett |
| 2007 | CADE | Solving Quantified Verification Conditions Using Satisfiability Modulo Theories. | Yeting Ge, Clark W. Barrett, Cesare Tinelli |
| 2007 | CAV | CVC3. | Clark W. Barrett, Cesare Tinelli |
| 2006 | CAV | cascade: C Assertion Checker and Deductive Engine. | Nikhil Sethi, Clark W. Barrett |
| 2006 | LPAR | Splitting on Demand in SAT Modulo Theories. | Clark W. Barrett, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli |
| 2005 | CAV | TVOC: A Translation Validator for Optimizing Compilers. | Clark W. Barrett, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, Lenore D. Zuck |
| 2005 | CAV | SMT-COMP: Satisfiability Modulo Theories Competition. | Clark W. Barrett, Leonardo Mendona de Moura, Aaron Stump |
| 2004 | CAV | CVC Lite: A New Implementation of the Cooperating Validity Checker Category B. | Clark W. Barrett, Sergey Berezin |
| 2004 | SEFM | Theory and Algorithms for the Generation and Validation of Speculative Loop Optimizations. | Ying Hu, Clark W. Barrett, Benjamin Goldberg |
| 2002 | CAV | Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. | Clark W. Barrett, David L. Dill, Aaron Stump |
| 2002 | CAV | CVC: A Cooperating Validity Checker. | Aaron Stump, Clark W. Barrett, David L. Dill |
| 2001 | LICS | A Decision Procedure for an Extensional Theory of Arrays. | Aaron Stump, Clark W. Barrett, David L. Dill, Jeremy R. Levitt |
| 2000 | CADE | A Framework for Cooperating Decision Procedures. | Clark W. Barrett, David L. Dill, Aaron Stump |
| 1998 | DAC | A Decision Procedure for Bit-Vector Arithmetic. | Clark W. Barrett, David L. Dill, Jeremy R. Levitt |
| 1996 | FMCAD | Validity Checking for Combinations of Theories with Equality. | Clark W. Barrett, David L. Dill, Jeremy R. Levitt |
| 1996 | FMCAD | Automatic Generation of Invariants in Processor Verification. | Jeffrey X. Su, David L. Dill, Clark W. Barrett |