Clark W. Barrett

317 papers A* 27A 29B 50Journal 132Unranked 74

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	A New Strategy for Verifying Reach-Avoid Specifications in Neural Feedback Systems. CoRR Samuel I. Akinwande, Sydney M. Katz, Mykel J. Kochenderfer, Clark W. Barrett
2026	J	`jnl`	CSLib: The Lean Computer Science Library. CoRR Clark W. Barrett, Swarat Chaudhuri, Fabrizio Montesi, Jim Grundy, Pushmeet Kohli, Leonardo de Moura, Alexandre Rademaker, Sorrachai Yingchareonthawornchai
2026	J	`jnl`	Certificates in AI: Learn but Verify. Commun. ACM Clark W. Barrett, Thomas A. Henzinger, Sanjit A. Seshia
2026	J	`jnl`	Combining Combination Properties, Part I: Nelson-Oppen and Politeness. J. Autom. Reason. Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett
2026	A*	`conf`	Cubing for Tuning. AAAI Haoze Wu, Clark W. Barrett, Nina Narodytska
2026	A*	`conf`	Efficiently Computing Compact Formal Explanations. AAAI Min Wu, Xiaofu Li, Haoze Wu, Clark W. Barrett
2026	—	`conf`	Exploring the SMT-LIB Benchmark Library. TACAS (1) Hans-Jörg Schurr, François Bobot, Mathias Preiner, Aina Niemetz, Clark W. Barrett, Pascal Fontaine, Cesare Tinelli
2026	B	`conf`	Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions. CPP Tomaz Mascarenhas, Harun Khan, Abdalrhman Mohamed, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli
2026	—	`conf`	Integrating String Reasoning in Symbolic Execution of C Programs. TACAS (2) Rachel Cleaveland, Clark W. Barrett
2026	J	`jnl`	Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4. CoRR Leni Aniva, Iori Oikawa, David Dill, Clark W. Barrett
2026	J	`jnl`	PEak: A Single Source of Truth for Hardware Design and Verification. ACM Trans. Embed. Comput. Syst. Caleb Donovick, Jackson Melchert, Ross Daly, Lenny Truong, Priyanka Raina, Pat Hanrahan, Clark W. Barrett
2026	A*	`conf`	Parameterized Abstract Interpretation for Transformer Verification. AAAI Pei Huang, Dennis Wei, Omri Isac, Haoze Wu, Min Wu, Clark W. Barrett
2026	B	`conf`	Proof Minimization in Neural Network Verification. VMCAI Omri Isac, Idan Refaeli, Haoze Wu, Clark W. Barrett, Guy Katz
2026	J	`jnl`	Self-Supervised Bootstrapping of Action-Predictive Embodied Reasoning. CoRR Milan Ganai, Katie Luo, Jonas Frey, Clark W. Barrett, Marco Pavone
2026	J	`jnl`	The FABRIC Strategy for Verifying Neural Feedback Systems. CoRR Samuel I. Akinwande, Sydney M. Katz, Mykel J. Kochenderfer, Clark W. Barrett
2026	—	`conf`	VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus. TACAS (2) Chuyue Sun, Yican Sun, Daneshvar Amrollahi, Ethan Zhang, Shuvendu K. Lahiri, Shan Lu, David L. Dill, Clark W. Barrett
2025	A	`conf`	Application of Formal Methods (SAT/SMT) to the Design of Constrained Codes. DATE Sunil Sudhakaran, Clark W. Barrett, Mark Horowitz
2025	A	`ed.`	Automated Deduction - CADE 30 - 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, Proceedings CADE Clark W. Barrett, Uwe Waldmann
2025	B	`conf`	Automated Translation Validation of a Compiler for Statically Scheduled Accelerators. FMCAD Jackson Melchert, Caleb Terrill, Aron Ricardo Perez-Lopez, Clark W. Barrett, Priyanka Raina
2025	A	`conf`	Bit-Precise Reasoning with Parametric Bit-Vectors. SAT Zvika Berger, Yoni Zohar, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2025	J	`jnl`	Bounded verification for finite-field-blasting in a compiler for zero knowledge proofs. Formal Methods Syst. Des. Alex Ozdemir, Riad S. Wahby, Fraser Brown, Clark W. Barrett
2025	—	`conf`	ClassInvGen: Class Invariant Synthesis Using Large Language Models. SAIV Chuyue Sun, Viraj Agashe, Saikat Chakraborty, Jubi Taneja, Clark W. Barrett, David L. Dill, Xiaokang Qiu, Shuvendu K. Lahiri
2025	J	`jnl`	ClassInvGen: Class Invariant Synthesis using Large Language Models. CoRR Chuyue Sun, Viraj Agashe, Saikat Chakraborty, Jubi Taneja, Clark W. Barrett, David L. Dill, Xiaokang Qiu, Shuvendu K. Lahiri
2025	J	`jnl`	Cubing for Tuning. CoRR Haoze Wu, Clark W. Barrett, Nina Narodytska
2025	A	`conf`	Efficient SAT-Based Bounded Model Checking of Evolving Systems. DATE Sophie Andrews, Matthew Sotoudeh, Clark W. Barrett
2025	B	`conf`	Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL. ITP Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds, Hans-Jörg Schurr, Clark W. Barrett, Cesare Tinelli
2025	—	`conf`	Integer Reasoning Modulo Different Constants in SMT. CAV (1) Elizaveta Pertseva, Alex Ozdemir, Shankara Pailoor, Alp Bassa, Sorawee Porncharoenwase, Isil Dillig, Clark W. Barrett
2025	J	`jnl`	Integer Reasoning Modulo Different Constants in SMT. CoRR Elizaveta Pertseva, Alex Ozdemir, Shankara Pailoor, Alp Bassa, Sorawee Porncharoenwase, Isil Dillig, Clark W. Barrett
2025	J	`jnl`	Interactive Bitvector Reasoning using Verified Bit-Blasting. Proc. ACM Program. Lang. Henrik Böving, Siddharth Bhat, Luisa Cicolini, Alex C. Keizer, Léon Frénot, Abdalrhman Mohamed, Léo Stefanesco, Harun Khan, Joshua Clune, Clark W. Barrett, Tobias Grosser
2025	—	`conf`	Lean-Auto: An Interface Between Lean 4 and Automated Theorem Provers. CAV (3) Yicheng Qian, Joshua Clune, Clark W. Barrett, Jeremy Avigad
2025	J	`jnl`	Lean-SMT: An SMT tactic for discharging proof goals in Lean. CoRR Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett
2025	J	`jnl`	Lean-auto: An Interface between Lean 4 and Automated Theorem Provers. CoRR Yicheng Qian, Joshua Clune, Clark W. Barrett, Jeremy Avigad
2025	—	`conf`	Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4. TACAS (1) Leni Aniva, Chuyue Sun, Brando Miranda, Clark W. Barrett, Sanmi Koyejo
2025	B	`conf`	Per-Instance Subproblem Generation for Strategy Selection in SMT. FMCAD Amalee Wilson, Nina Narodytska, Clark W. Barrett, Haoze Wu
2025	J	`jnl`	Proof Minimization in Neural Network Verification. CoRR Omri Isac, Idan Refaeli, Haoze Wu, Clark W. Barrett, Guy Katz
2025	J	`jnl`	Proof-Driven Clause Learning in Neural Network Verification. CoRR Omri Isac, Idan Refaeli, Haoze Wu, Clark W. Barrett, Guy Katz
2025	—	`conf`	Relational Hoare Logic for Realistically Modelled Machine Code. CAV (1) Denis Mazzucato, Abdalrhman Mohamed, Juneyoung Lee, Clark W. Barrett, Jim Grundy, John Harrison, Corina S. Pasareanu
2025	J	`jnl`	Relational Hoare Logic for Realistically Modelled Machine Code. CoRR Denis Mazzucato, Abdalrhman Mohamed, Juneyoung Lee, Clark W. Barrett, Jim Grundy, John Harrison, Corina S. Pasareanu
2025	B	`conf`	Solving Set Constraints with Comprehensions and Bounded Quantifiers. FMCAD Mudathir Mohamed, Nick Feng, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett, Marsha Chechik
2025	J	`jnl`	Solving Set Constraints with Comprehensions and Bounded Quantifiers. CoRR Mudathir Mohamed, Nick Feng, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett, Marsha Chechik
2025	J	`jnl`	The termination of Nielsen transformations applied to word equations with length constraints. CoRR Benjamin Przybocki, Clark W. Barrett
2025	B	`conf`	Towards SMT Solver Stability via Input Normalization. FMCAD Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz, Andrew Reynolds, Moses Charikar, Cesare Tinelli, Clark W. Barrett
2025	J	`jnl`	VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus. CoRR Chuyue Sun, Yican Sun, Daneshvar Amrollahi, Ethan Zhang, Shuvendu K. Lahiri, Shan Lu, David L. Dill, Clark W. Barrett
2025	J	`jnl`	Verifying Nonlinear Neural Feedback Systems using Polyhedral Enclosures. CoRR Samuel I. Akinwande, Chelsea Sidrane, Mykel J. Kochenderfer, Clark W. Barrett
2025	—	`conf`	lean-smt: An SMT Tactic for Discharging Proof Goals in Lean. CAV (3) Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett
2024	J	`jnl`	Better Verified Explanations with Applications to Incorrectness and Out-of-Distribution Detection. CoRR Min Wu, Xiaofu Li, Haoze Wu, Clark W. Barrett
2024	—	`conf`	Clover: Closed-Loop Verifiable Code Generation. SAIV Chuyue Sun, Ying Sheng, Oded Padon, Clark W. Barrett
2024	B	`conf`	Efficiently Synthesizing Lowest Cost Rewrite Rules for Instruction Selection. FMCAD Ross Daly, Caleb Donovick, Caleb Terrill, Jackson Melchert, Priyanka Raina, Clark W. Barrett, Pat Hanrahan
2024	J	`jnl`	Efficiently Synthesizing Lowest Cost Rewrite Rules for Instruction Selection. CoRR Ross Daly, Caleb Donovick, Caleb Terrill, Jackson Melchert, Priyanka Raina, Clark W. Barrett, Pat Hanrahan
2024	B	`conf`	Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates. FMCAD 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	J	`jnl`	Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates. CoRR 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	—	`conf`	Generalized Optimization Modulo Theories. IJCAR (1) Nestan Tsiskaridze, Clark W. Barrett, Cesare Tinelli
2024	J	`jnl`	Generalized Optimization Modulo Theories. CoRR Nestan Tsiskaridze, Clark W. Barrett, Cesare Tinelli
2024	—	`conf`	IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. TACAS (1) Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2024	A*	`conf`	Lemur: Integrating Large Language Models in Automated Program Verification. ICLR Haoze Wu, Clark W. Barrett, Nina Narodytska
2024	—	`conf`	Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. CAV (2) 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	J	`jnl`	Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. CoRR 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	J	`jnl`	Markovian Agents for Truthful Language Modeling. CoRR Scott Viteri, Max Lamparth, Peter Chatain, Clark W. Barrett
2024	J	`jnl`	Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4. CoRR Leni Aniva, Chuyue Sun, Brando Miranda, Clark W. Barrett, Sanmi Koyejo
2024	—	`conf`	Parallel Verification for δ-Equivalence of Neural Network Quantization. SAIV Pei Huang, Yuting Yang, Haoze Wu, Ieva Daukantas, Min Wu, Fuqi Jia, Clark W. Barrett
2024	B	`conf`	Robust Mean Estimation by All Means (Short Paper). ITP Reynald Affeldt, Clark W. Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa, Carsten Schürmann
2024	A*	`conf`	SGLang: Efficient Execution of Structured Language Model Programs. NeurIPS Lianmin Zheng, Liangsheng Yin, Zhiqiang Xie, Chuyue Sun, Jeff Huang, Cody Hao Yu, Shiyi Cao, Christos Kozyrakis, Ion Stoica, Joseph E. Gonzalez, Clark W. Barrett, Ying Sheng
2024	B	`conf`	SMT-D: New Strategies for Portfolio-Based SMT Solving. FMCAD 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	J	`jnl`	Safe and Reliable Training of Learning-Based Aerospace Controllers. CoRR Udayan Mandal, Guy Amir, Haoze Wu, Ieva Daukantas, Fletcher Lee Newell, Umberto J. Ravaioli, Baoluo Meng, Michael Durling, Kerianne Hobbs, Milan Ganai, Tobey Shim, Guy Katz, Clark W. Barrett
2024	—	`conf`	Satisfiability Modulo Theories: A Beginner's Tutorial. FM (2) Clark W. Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar
2024	—	`conf`	Split Gröbner Bases for Satisfiability Modulo Finite Fields. CAV (1) Alex Ozdemir, Shankara Pailoor, Alp Bassa, Kostas Ferles, Clark W. Barrett, Isil Dillig
2024	J	`jnl`	Split Gröbner Bases for Satisfiability Modulo Finite Fields. IACR Cryptol. ePrint Arch. Alex Ozdemir, Shankara Pailoor, Alp Bassa, Kostas Ferles, Clark W. Barrett, Isil Dillig
2024	—	`conf`	The Nonexistence of Unicorns and Many-Sorted Löwenheim-Skolem Theorems. FM (1) Benjamin Przybocki, Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett
2024	J	`jnl`	The nonexistence of unicorns and many-sorted Löwenheim-Skolem theorems. CoRR Benjamin Przybocki, Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett
2024	A*	`conf`	Towards Efficient Verification of Quantized Neural Networks. AAAI Pei Huang, Haoze Wu, Yuting Yang, Ieva Daukantas, Min Wu, Yedi Zhang, Clark W. Barrett
2024	J	`jnl`	Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems. CoRR David Dalrymple, Joar Skalse, Yoshua Bengio, Stuart Russell, Max Tegmark, Sanjit A. Seshia, Steve Omohundro, Christian Szegedy, Ben Goldhaber, Nora Ammann, Alessandro Abate, Joe Halpern, Clark W. Barrett, Ding Zhao, Tan Zhi-Xuan, Jeannette M. Wing, Joshua B. Tenenbaum
2024	J	`jnl`	Using Normalization to Improve SMT Solver Stability. CoRR Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz, Andrew Reynolds, Moses Charikar, Cesare Tinelli, Clark W. Barrett
2024	J	`jnl`	Verifying SQL Queries using Theories of Tables and Relations. CoRR Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
2024	B	`conf`	Verifying SQL queries using theories of tables and relations. LPAR Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
2023	B	`conf`	A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery. FMCAD Abdalrhman Mohamed, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2023	J	`jnl`	AHA: An Agile Approach to the Design of Coarse-Grained Reconfigurable Accelerators and Compilers. ACM Trans. Embed. Comput. Syst. 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 A. Myers, Nestan Tsiskaridze, Stephen Richardson, Rick Bahr, Kayvon Fatahalian, Pat Hanrahan, Clark W. Barrett, Mark Horowitz, Christopher Torng, Fredrik Kjolstad, Priyanka Raina
2023	—	`conf`	APEX: A Framework for Automated Processing Element Design Space Exploration using Frequent Subgraph Analysis. ASPLOS (3) Jackson Melchert, Kathleen Feng, Caleb Donovick, Ross Daly, Ritvik Sharma, Clark W. Barrett, Mark A. Horowitz, Pat Hanrahan, Priyanka Raina
2023	B	`conf`	An Interactive SMT Tactic in Coq using Abductive Reasoning. LPAR Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli, Clark W. Barrett
2023	—	`conf`	Automatic Verification of SMT Rewrites in Isabelle/HOL. SMT Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2023	J	`jnl`	Bounded Verification for Finite-Field-Blasting (In a Compiler for Zero Knowledge Proofs). IACR Cryptol. ePrint Arch. Alex Ozdemir, Riad S. Wahby, Fraser Brown, Clark W. Barrett
2023	—	`conf`	Bounded Verification for Finite-Field-Blasting - In a Compiler for Zero Knowledge Proofs. CAV (3) Alex Ozdemir, Riad S. Wahby, Fraser Brown, Clark W. Barrett
2023	J	`jnl`	Clover: Closed-Loop Verifiable Code Generation. CoRR Chuyue Sun, Ying Sheng, Oded Padon, Clark W. Barrett
2023	A	`conf`	Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness. CADE Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett
2023	J	`jnl`	Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness. CoRR Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett
2023	—	`conf`	Combining Finite Combination Properties: Finite Models and Busy Beavers. FroCoS Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett
2023	J	`jnl`	Combining Finite Combination Properties: Finite Models and Busy Beavers. CoRR Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett
2023	J	`jnl`	Combining Stable Infiniteness and (Strong) Politeness. J. Autom. Reason. Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2023	A	`conf`	Convex Bounds on the Softmax Function with Applications to Robustness Verification. AISTATS Dennis Wei, Haoze Wu, Min Wu, Pin-Yu Chen, Clark W. Barrett, Eitan Farchi
2023	J	`jnl`	Convex Bounds on the Softmax Function with Applications to Robustness Verification. CoRR Dennis Wei, Haoze Wu, Min Wu, Pin-Yu Chen, Clark W. Barrett, Eitan Farchi
2023	B	`conf`	DNN Verification, Reachability, and the Exponential Function Problem. CONCUR Omri Isac, Yoni Zohar, Clark W. Barrett, Guy Katz
2023	J	`jnl`	DNN Verification, Reachability, and the Exponential Function Problem. CoRR Omri Isac, Yoni Zohar, Clark W. Barrett, Guy Katz
2023	J	`jnl`	Efficiently Programming Large Language Models using SGLang. CoRR Lianmin Zheng, Liangsheng Yin, Zhiqiang Xie, Jeff Huang, Chuyue Sun, Cody Hao Yu, Shiyi Cao, Christos Kozyrakis, Ion Stoica, Joseph E. Gonzalez, Clark W. Barrett, Ying Sheng
2023	—	`conf`	Formal Verification of Bit-Vector Invertibility Conditions in Coq. FroCoS Burak Ekici, Arjun Viswanathan, Yoni Zohar, Cesare Tinelli, Clark W. Barrett
2023	A*	`conf`	G-QED: Generalized QED Pre-silicon Verification beyond Non-Interfering Hardware Accelerators. DAC 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	J	`jnl`	Generating and Exploiting Automated Reasoning Proof Certificates. Commun. ACM Haniel Barbosa, Clark W. Barrett, Byron Cook, Bruno Dutertre, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Cesare Tinelli, Yoni Zohar
2023	J	`jnl`	Global optimization of objective functions represented by ReLU networks. Mach. Learn. Christopher A. Strong, Haoze Wu, Aleksandar Zeljic, Kyle D. Julian, Guy Katz, Clark W. Barrett, Mykel J. Kochenderfer
2023	J	`jnl`	H CoRR Zhenyu Zhang, Ying Sheng, Tianyi Zhou, Tianlong Chen, Lianmin Zheng, Ruisi Cai, Zhao Song, Yuandong Tian, Christopher Ré, Clark W. Barrett, Zhangyang Wang, Beidi Chen
2023	A*	`conf`	H2O: Heavy-Hitter Oracle for Efficient Generative Inference of Large Language Models. NeurIPS Zhenyu Zhang, Ying Sheng, Tianyi Zhou, Tianlong Chen, Lianmin Zheng, Ruisi Cai, Zhao Song, Yuandong Tian, Christopher Ré, Clark W. Barrett, Zhangyang Wang, Beidi Chen
2023	J	`jnl`	High-throughput Generative Inference of Large Language Models with a Single GPU. CoRR Ying Sheng, Lianmin Zheng, Binhang Yuan, Zhuohan Li, Max Ryabinin, Daniel Y. Fu, Zhiqiang Xie, Beidi Chen, Clark W. Barrett, Joseph E. Gonzalez, Percy Liang, Christopher Ré, Ion Stoica, Ce Zhang
2023	J	`jnl`	Identifying and Mitigating the Security Risks of Generative AI. CoRR Clark W. Barrett, Brad Boyd, Ellie Burzstein, 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 C. Mitchell, Zulfikar Ramzan, Khawaja Shams, Dawn Song, Ankur Taly, Diyi Yang
2023	J	`jnl`	Identifying and Mitigating the Security Risks of Generative AI. Found. Trends Priv. Secur. Clark W. 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 C. Mitchell, Zulfikar Ramzan, Khawaja Shams, Dawn Song, Ankur Taly, Diyi Yang
2023	J	`jnl`	Lemur: Integrating Large Language Models in Automated Program Verification. CoRR Haoze Wu, Clark W. Barrett, Nina Narodytska
2023	B	`conf`	Lightweight Online Learning for Sets of Related Problems in Automated Reasoning. FMCAD Haoze Wu, Christopher Hahn, Florian Lonsing, Makai Mann, Raghuram Ramanujan, Clark W. Barrett
2023	J	`jnl`	Lightweight Online Learning for Sets of Related Problems in Automated Reasoning. CoRR Haoze Wu, Christopher Hahn, Florian Lonsing, Makai Mann, Raghuram Ramanujan, Clark W. Barrett
2023	J	`jnl`	On Optimal Caching and Model Multiplexing for Large Model Inference. CoRR Banghua Zhu, Ying Sheng, Lianmin Zheng, Clark W. Barrett, Michael I. Jordan, Jiantao Jiao
2023	J	`jnl`	PEak: A Single Source of Truth for Hardware Design and Verification. CoRR Caleb Donovick, Ross Daly, Jackson Melchert, Lenny Truong, Priyanka Raina, Pat Hanrahan, Clark W. Barrett
2023	B	`conf`	Partitioning Strategies for Distributed SMT Solving. FMCAD Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett
2023	J	`jnl`	Partitioning Strategies for Distributed SMT Solving. CoRR Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett
2023	J	`jnl`	Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences. J. Autom. Reason. Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
2023	—	`conf`	Satisfiability Modulo Finite Fields. CAV (2) Alex Ozdemir, Gereon Kremer, Cesare Tinelli, Clark W. Barrett
2023	J	`jnl`	Satisfiability Modulo Finite Fields. IACR Cryptol. ePrint Arch. Alex Ozdemir, Gereon Kremer, Cesare Tinelli, Clark W. Barrett
2023	A	`conf`	Soy: An Efficient MILP Solver for Piecewise-Affine Systems. IROS Haoze Wu, Min Wu, Dorsa Sadigh, Clark W. Barrett
2023	J	`jnl`	Soy: An Efficient MILP Solver for Piecewise-Affine Systems. CoRR Haoze Wu, Min Wu, Dorsa Sadigh, Clark W. Barrett
2023	J	`jnl`	Synthesising Programs with Non-trivial Constants. J. Autom. Reason. Alessandro Abate, Haniel Barbosa, Clark W. Barrett, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, Andrew Reynolds, Cesare Tinelli
2023	B	`conf`	Tighter Abstract Queries in Neural Network Verification. LPAR Elazar Cohen, Yizhak Yisrael Elboher, Clark W. Barrett, Guy Katz
2023	—	`conf`	Toward Certified Robustness Against Real-World Distribution Shifts. SaTML Haoze Wu, Teruhiro Tagomori, Alexander Robey, Fengjun Yang, Nikolai Matni, George J. Pappas, Hamed Hassani, Corina S. Pasareanu, Clark W. Barrett
2023	J	`jnl`	Towards Efficient Verification of Quantized Neural Networks. CoRR Pei Huang, Haoze Wu, Yuting Yang, Ieva Daukantas, Min Wu, Yedi Zhang, Clark W. Barrett
2023	A*	`conf`	Towards Optimal Caching and Model Selection for Large Model Inference. NeurIPS Banghua Zhu, Ying Sheng, Lianmin Zheng, Clark W. Barrett, Michael I. Jordan, Jiantao Jiao
2023	A*	`conf`	VeriX: Towards Verified Explainability of Deep Neural Networks. NeurIPS Min Wu, Haoze Wu, Clark W. Barrett
2022	B	`conf`	An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks. ATVA Matan Ostrovsky, Clark W. Barrett, Guy Katz
2022	J	`jnl`	An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks. CoRR Matan Ostrovsky, Clark W. Barrett, Guy Katz
2022	B	`conf`	Bit-Precise Reasoning via Int-Blasting. VMCAI Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2022	A	`conf`	Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description). IJCAR Gereon Kremer, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2022	J	`jnl`	Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays. Log. Methods Comput. Sci. Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark W. Barrett
2022	—	`conf`	Efficient Neural Network Analysis with Sum-of-Infeasibilities. TACAS (1) Haoze Wu, Aleksandar Zeljic, Guy Katz, Clark W. Barrett
2022	J	`jnl`	Efficient Neural Network Analysis with Sum-of-Infeasibilities. CoRR Haoze Wu, Aleksandar Zeljic, Guy Katz, Clark W. Barrett
2022	—	`conf`	Even Faster Conflicts and Lazier Reductions for String Solvers. CAV (2) Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli
2022	A	`conf`	Flexible Proof Production in an Industrial-Strength SMT Solver. IJCAR 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, Clark W. Barrett
2022	—	`conf`	Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers. CAV (2) Aina Niemetz, Mathias Preiner, Clark W. Barrett
2022	B	`conf`	Neural Network Verification with Proof Production. FMCAD Omri Isac, Clark W. Barrett, Min Zhang, Guy Katz
2022	J	`jnl`	Neural Network Verification with Proof Production. CoRR Omri Isac, Clark W. Barrett, Min Zhang, Guy Katz
2022	B	`conf`	On Optimizing Back-Substitution Methods for Neural Network Verification. FMCAD Tom Zelazny, Haoze Wu, Clark W. Barrett, Guy Katz
2022	J	`jnl`	On Optimizing Back-Substitution Methods for Neural Network Verification. CoRR Tom Zelazny, Haoze Wu, Clark W. Barrett, Guy Katz
2022	J	`jnl`	Polite Combination of Algebraic Datatypes. J. Autom. Reason. Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett
2022	J	`jnl`	Proof-Stitch: Proof Combination for Divide and Conquer SAT Solvers. CoRR Abhishek Nair, Saranyu Chattopadhyay, Haoze Wu, Alex Ozdemir, Clark W. Barrett
2022	B	`conf`	Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers. FMCAD Abhishek Anil Nair, Saranyu Chattopadhyay, Haoze Wu, Alex Ozdemir, Clark W. Barrett
2022	A	`conf`	Reasoning About Vectors Using an SMT Theory of Sequences. IJCAR Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
2022	J	`jnl`	Reasoning About Vectors using an SMT Theory of Sequences. CoRR Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
2022	B	`conf`	Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language. FMCAD Andres Nötzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2022	J	`jnl`	Reluplex: a calculus for reasoning about deep neural networks. Formal Methods Syst. Des. Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer
2022	J	`jnl`	Scalable Verification of GNN-based Job Schedulers. CoRR Haoze Wu, Clark W. Barrett, Mahmood Sharif, Nina Narodytska, Gagandeep Singh
2022	J	`jnl`	Scalable verification of GNN-based job schedulers. Proc. ACM Program. Lang. Haoze Wu, Clark W. Barrett, Mahmood Sharif, Nina Narodytska, Gagandeep Singh
2022	B	`conf`	Synthesizing Instruction Selection Rewrite Rules from RTL using SMT. FMCAD Ross Daly, Caleb Donovick, Jackson Melchert, Rajsekhar Setaluri, Nestan Tsiskaridze, Priyanka Raina, Clark W. Barrett, Pat Hanrahan
2022	J	`jnl`	Tighter Abstract Queries in Neural Network Verification. CoRR Elazar Cohen, Yizhak Yisrael Elboher, Clark W. Barrett, Guy Katz
2022	J	`jnl`	Toward Certified Robustness Against Real-World Distribution Shifts. CoRR Haoze Wu, Teruhiro Tagomori, Alexander Robey, Fengjun Yang, Nikolai Matni, George J. Pappas, Hamed Hassani, Corina S. Pasareanu, Clark W. Barrett
2022	J	`jnl`	VeriX: Towards Verified Explainability of Deep Neural Networks. CoRR Min Wu, Haoze Wu, Clark W. Barrett
2022	—	`conf`	cvc5: A Versatile and Industrial-Strength SMT Solver. TACAS (1) 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, Yoni Zohar
2021	J	`jnl`	Algorithms for Verifying Deep Neural Networks. Found. Trends Optim. Changliu Liu, Tomer Arnon, Christopher Lazarus, Christopher A. Strong, Clark W. Barrett, Mykel J. Kochenderfer
2021	—	`conf`	An SMT-Based Approach for Verifying Binarized Neural Networks. TACAS (2) Guy Amir, Haoze Wu, Clark W. Barrett, Guy Katz
2021	J	`jnl`	Automated Design Space Exploration of CGRA Processing Element Architectures using Frequent Subgraph Analysis. CoRR Jackson Melchert, Kathleen Feng, Caleb Donovick, Ross Daly, Clark W. Barrett, Mark Horowitz, Pat Hanrahan, Priyanka Raina
2021	B	`conf`	Automating System Configuration. FMCAD Nestan Tsiskaridze, Maxwell Strange, Makai Mann, Kavya Sreedhar, Qiaoyi Liu, Mark Horowitz, Clark W. Barrett
2021	J	`jnl`	Automating System Configuration. CoRR Nestan Tsiskaridze, Maxwell Strange, Makai Mann, Kavya Sreedhar, Qiaoyi Liu, Mark Horowitz, Clark W. Barrett
2021	—	`conf`	Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays. TACAS (1) Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark W. Barrett
2021	J	`jnl`	Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays. CoRR Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark W. Barrett
2021	B	`conf`	DeepCert: Verification of Contextually Relevant Robustness for Neural Network Image Classifiers. SAFECOMP Colin Paterson, Haoze Wu, John Grese, Radu Calinescu, Corina S. Pasareanu, Clark W. Barrett
2021	J	`jnl`	DeepCert: Verification of Contextually Relevant Robustness for Neural Network Image Classifiers. CoRR Colin Paterson, Haoze Wu, John Grese, Radu Calinescu, Corina S. Pasareanu, Clark W. Barrett
2021	J	`jnl`	Effective Pre-Silicon Verification of Processor Cores by Breaking the Bounds of Symbolic Quick Error Detection. CoRR Karthik Ganesan, Florian Lonsing, Srinivasa Shashank Nuthakki, Eshan Singh, Mohammad Rahmani Fadiheh, Wolfgang Kunz, Dominik Stoffel, Clark W. Barrett, Subhasish Mitra
2021	J	`jnl`	On solving quantified bit-vector constraints using invertibility conditions. Formal Methods Syst. Des. Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2021	A	`conf`	Politeness and Stable Infiniteness: Stronger Together. CADE Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2021	J	`jnl`	Politeness and Stable Infiniteness: Stronger Together. CoRR Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2021	A*	`conf`	Politeness for the Theory of Algebraic Datatypes (Extended Abstract). IJCAI Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett
2021	—	`conf`	Pono: A Flexible and Extensible SMT-Based Model Checker. CAV (2) Makai Mann, Ahmed Irfan, Florian Lonsing, Yahan Yang, Hongce Zhang, Kristopher Brown, Aarti Gupta, Clark W. Barrett
2021	B	`conf`	SAT Solving in the Serverless Cloud. FMCAD Alex Ozdemir, Haoze Wu, Clark W. Barrett
2021	—	`ch.`	Satisfiability Modulo Theories. Handbook of Satisfiability Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, Cesare Tinelli
2021	B	`conf`	Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition. FMCAD 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	J	`jnl`	Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition. CoRR 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	A	`conf`	Smt-Switch: A Solver-Agnostic C++ API for SMT Solving. SAT Makai Mann, Amalee Wilson, Yoni Zohar, Lindsey Stuntz, Ahmed Irfan, Kristopher Brown, Caleb Donovick, Allison Guman, Cesare Tinelli, Clark W. Barrett
2021	—	`conf`	Syntax-Guided Quantifier Instantiation. TACAS (2) Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2021	J	`jnl`	Towards Satisfiability Modulo Parametric Bit-vectors. J. Autom. Reason. Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
2021	J	`jnl`	lazybvtoint at the SMT Competition 2020. CoRR Yoni Zohar, Ahmed Irfan, Makai Mann, Andres Nötzli, Andrew Reynolds, Clark W. Barrett
2020	—	`conf`	A Decision Procedure for String to Code Point Conversion. IJCAR (1) Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2020	B	`conf`	A Theoretical Framework for Symbolic Quick Error Detection. FMCAD Florian Lonsing, Subhasish Mitra, Clark W. Barrett
2020	J	`jnl`	A Theoretical Framework for Symbolic Quick Error Detection. CoRR Florian Lonsing, Subhasish Mitra, Clark W. Barrett
2020	A*	`conf`	A-QED Verification of Hardware Accelerators. DAC 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	J	`jnl`	An SMT-Based Approach for Verifying Binarized Neural Networks. CoRR Guy Amir, Haoze Wu, Clark W. Barrett, Guy Katz
2020	A*	`conf`	Creating an Agile Hardware Design Flow. DAC 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	A	`conf`	Gap-free Processor Verification by S DATE Keerthikumara Devarajegowda, Mohammad Rahmani Fadiheh, Eshan Singh, Clark W. Barrett, Subhasish Mitra, Wolfgang Ecker, Dominik Stoffel, Wolfgang Kunz
2020	J	`jnl`	Global Optimization of Objective Functions Represented by ReLU Networks. CoRR Christopher A. Strong, Haoze Wu, Aleksandar Zeljic, Kyle D. Julian, Guy Katz, Clark W. Barrett, Mykel J. Kochenderfer
2020	B	`conf`	Parallelization Techniques for Verifying Neural Networks. FMCAD Haoze Wu, Alex Ozdemir, Aleksandar Zeljic, Kyle Julian, Ahmed Irfan, Divya Gopinath, Sadjad Fouladi, Guy Katz, Corina S. Pasareanu, Clark W. Barrett
2020	J	`jnl`	Parallelization Techniques for Verifying Neural Networks. CoRR Haoze Wu, Alex Ozdemir, Aleksandar Zeljic, Ahmed Irfan, Kyle Julian, Divya Gopinath, Sadjad Fouladi, Guy Katz, Corina S. Pasareanu, Clark W. Barrett
2020	—	`conf`	Partial Order Reduction for Deep Bug Finding in Synchronous Hardware. TACAS (1) Makai Mann, Clark W. Barrett
2020	—	`conf`	Politeness for the Theory of Algebraic Datatypes. IJCAR (1) Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett
2020	J	`jnl`	Politeness for the Theory of Algebraic Datatypes. CoRR Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett
2020	B	`conf`	Reductions for Strings and Regular Expressions Revisited. FMCAD Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2020	J	`jnl`	Resources: A Safe Language Abstraction for Money. CoRR Sam Blackshear, David L. Dill, Shaz Qadeer, Clark W. Barrett, John C. Mitchell, Oded Padon, Yoni Zohar
2020	—	`conf`	Simplifying Neural Networks Using Formal Verification. NFM Sumathi Gokulanathan, Alexander Feldsher, Adi Malca, Clark W. Barrett, Guy Katz
2020	—	`conf`	Smt-Switch: A Solver-agnostic C++ API for SMT Solving. SMT Makai Mann, Amalee Wilson, Cesare Tinelli, Clark W. Barrett
2020	J	`jnl`	Smt-Switch: a solver-agnostic C++ API for SMT Solving. CoRR Makai Mann, Amalee Wilson, Cesare Tinelli, Clark W. Barrett
2020	—	`conf`	The Move Prover. CAV (1) Jingyi Emma Zhong, Kevin Cheang, Shaz Qadeer, Wolfgang Grieskamp, Sam Blackshear, Junkil Park, Yoni Zohar, Clark W. Barrett, David L. Dill
2020	B	`conf`	Verifying Recurrent Neural Networks Using Invariant Inference. ATVA Yuval Jacoby, Clark W. Barrett, Guy Katz
2020	J	`jnl`	Verifying Recurrent Neural Networks using Invariant Inference. CoRR Yuval Jacoby, Clark W. Barrett, Guy Katz
2020	J	`jnl`	fault: A Python Embedded Domain-Specific Language For Metaprogramming Portable Hardware Verification Components. CoRR 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	—	`conf`	fault: A Python Embedded Domain-Specific Language for Metaprogramming Portable Hardware Verification Components. CAV (1) Lenny Truong, Steven Herbst, Rajsekhar Setaluri, Makai Mann, Ross G. Daly, Keyi Zhang, Caleb Donovick, Daniel Stanley, Mark Horowitz, Clark W. Barrett, Pat Hanrahan
2019	B	`ed.`	2019 Formal Methods in Computer Aided Design, FMCAD 2019, San Jose, CA, USA, October 22-25, 2019 FMCAD Clark W. Barrett, Jin Yang
2019	—	`conf`	Agile SMT-Based Mapping for CGRAs with Restricted Routing Networks. ReConFig Caleb Donovick, Makai Mann, Clark W. Barrett, Pat Hanrahan
2019	J	`jnl`	Algorithms for Verifying Deep Neural Networks. CoRR Changliu Liu, Tomer Arnon, Christopher Lazarus, Clark W. Barrett, Mykel J. Kochenderfer
2019	J	`jnl`	CVC4SY for SyGuS-COMP 2019. CoRR Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2019	A	`conf`	DRAT-based Bit-Vector Proofs in CVC4. SAT Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark W. Barrett
2019	J	`jnl`	DRAT-based Bit-Vector Proofs in CVC4. CoRR Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark W. Barrett
2019	A	`conf`	Extending SMT Solvers to Higher-Order Logic. CADE Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, Clark W. Barrett
2019	A*	`conf`	G2SAT: Learning to Generate SAT Formulas. NeurIPS Jiaxuan You, Haoze Wu, Clark W. Barrett, Raghuram Ramanujan, Jure Leskovec
2019	J	`jnl`	G2SAT: Learning to Generate SAT Formulas. CoRR Jiaxuan You, Haoze Wu, Clark W. Barrett, Raghuram Ramanujan, Jure Leskovec
2019	—	`conf`	High-Level Abstractions for Simplifying Extended String Constraints in SMT. CAV (2) Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2019	—	`conf`	Invertibility Conditions for Floating-Point Formulas. CAV (2) Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2019	A	`conf`	Processor Hardware Security Vulnerabilities and their Detection by Unique Program Execution Checking. DATE Mohammad Rahmani Fadiheh, Dominik Stoffel, Clark W. Barrett, Subhasish Mitra, Wolfgang Kunz
2019	J	`jnl`	Refutation-based synthesis in SMT. Formal Methods Syst. Des. Andrew Reynolds, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett, Morgan Deters
2019	J	`jnl`	Reports of the AAAI 2019 Spring Symposium Series. AI Mag. Ioana Baldini, Clark W. Barrett, Antonio Chella, Carlos Cinelli, David Gamez, Leilani H. Gilpin, Knut Hinkelmann, Dylan Holmes, Takashi Kido, Murat Kocaoglu, William F. Lawless, Alessio Lomuscio, Jamie C. Macbeth, Andreas Martin, Ranjeev Mittu, Evan Patterson, Donald Sofge, Prasad Tadepalli, Keiki Takadama, Shomir Wilson
2019	J	`jnl`	Selected Extended Papers of NFM 2017: Preface. J. Autom. Reason. Clark W. Barrett, Temesghen Kahsai
2019	J	`jnl`	Simplifying Neural Networks with the Marabou Verification Engine. CoRR Sumathi Gokulanathan, Alexander Feldsher, Adi Malca, Clark W. Barrett, Guy Katz
2019	A	`conf`	Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores: Industrial Case Study. DATE 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	J	`jnl`	Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores: Industrial Case Study. CoRR 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	A	`conf`	Syntax-Guided Rewrite Rule Enumeration for SMT Solvers. SAT Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark W. Barrett, Cesare Tinelli
2019	—	`conf`	The Marabou Framework for Verification and Analysis of Deep Neural Networks. CAV (1) 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	A	`conf`	Towards Bit-Width-Independent Proofs in SMT Solvers. CADE Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
2019	J	`jnl`	Towards Bit-Width-Independent Proofs in SMT Solvers. CoRR Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
2019	A	`conf`	Unlocking the Power of Formal Hardware Verification with CoSA and Symbolic QED: Invited Paper. ICCAD Florian Lonsing, Karthik Ganesan, Makai Mann, Srinivasa Shashank Nuthakki, Eshan Singh, Mario Srouji, Yahan Yang, Subhasish Mitra, Clark W. Barrett
2019	—	`conf`	Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract). PxTP Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
2019	—	`conf`	Verifying Deep-RL-Driven Systems. NetAI@SIGCOMM Yafim Kazak, Clark W. Barrett, Guy Katz, Michael Schapira
2019	—	`conf`	cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis. CAV (2) Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2018	J	`jnl`	CVC4 at the SMT Competition 2018. CoRR Clark W. Barrett, Haniel Barbosa, Martin Brain, Duligur Ibeling, Tim King, Paul Meng, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Cesare Tinelli
2018	B	`conf`	CoSA: Integrated Verification for Agile Hardware Design. FMCAD Cristian Mattarei, Makai Mann, Clark W. Barrett, Ross G. Daly, Dillon Huff, Pat Hanrahan
2018	A	`conf`	Datatypes with Shared Selectors. IJCAR Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, Clark W. Barrett
2018	B	`conf`	DeepSafe: A Data-Driven Approach for Assessing Robustness of Neural Networks. ATVA Divya Gopinath, Guy Katz, Corina S. Pasareanu, Clark W. Barrett
2018	—	`conf`	EMME: A Formal Tool for ECMAScript Memory Model Evaluation. TACAS (2) Cristian Mattarei, Clark W. Barrett, Shu-Yu Guo, Bradley Nelson, Ben Smith
2018	J	`jnl`	EMME: a formal tool for ECMAScript Memory Model Evaluation. CoRR Cristian Mattarei, Clark W. Barrett, Shu-Yu Guo, Bradley Nelson, Ben Smith
2018	J	`jnl`	On Solving Quantified Bit-Vectors using Invertibility Conditions. CoRR Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2018	J	`jnl`	Processor Hardware Security Vulnerabilities and their Detection by Unique Program Execution Checking. CoRR Mohammad Rahmani Fadiheh, Dominik Stoffel, Clark W. Barrett, Subhasish Mitra, Wolfgang Kunz
2018	J	`jnl`	Reasoning with Finite Sets and Cardinality Constraints in SMT. Log. Methods Comput. Sci. Kshitij Bansal, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli
2018	—	`ch.`	Satisfiability Modulo Theories. Handbook of Model Checking Clark W. Barrett, Cesare Tinelli
2018	—	`conf`	Solving Quantified Bit-Vectors Using Invertibility Conditions. CAV (2) Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2018	A	`conf`	Symbolic quick error detection using symbolic initial state for pre-silicon verification. DATE Mohammad Rahmani Fadiheh, Joakim Urdahl, Srinivasa Shashank Nuthakki, Subhasish Mitra, Clark W. Barrett, Dominik Stoffel, Wolfgang Kunz
2018	J	`jnl`	Toward Scalable Verification for Safety-Critical Deep Networks. CoRR Lindsey Kuper, Guy Katz, Justin Gottschlich, Kyle Julian, Clark W. Barrett, Mykel J. Kochenderfer
2018	—	`conf`	p4pktgen: Automated Test Case Generation for P4 Programs. SOSR Andres Nötzli, Jehandad Khan, Andy Fingerhut, Clark W. Barrett, Peter Athanas
2017	J	`jnl`	A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. CoRR Kshitij Bansal, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli
2017	J	`jnl`	Constraint Solving for Finite Model Finding in SMT Solvers. CoRR Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
2017	J	`jnl`	Constraint solving for finite model finding in SMT solvers. Theory Pract. Log. Program. Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
2017	J	`jnl`	DeepSafe: A Data-driven Approach for Checking Adversarial Robustness in Neural Networks. CoRR Divya Gopinath, Guy Katz, Corina S. Pasareanu, Clark W. Barrett
2017	—	`conf`	Designing Theory Solvers with Extensions. FroCoS Andrew Reynolds, Cesare Tinelli, Dejan Jovanovic, Clark W. Barrett
2017	J	`jnl`	E-QED: Electrical Bug Localization During Post-Silicon Validation Enabled by Quick Error Detection and Formal Methods. CoRR Eshan Singh, Clark W. Barrett, Subhasish Mitra
2017	—	`conf`	E-QED: Electrical Bug Localization During Post-silicon Validation Enabled by Quick Error Detection and Formal Methods. CAV (2) Eshan Singh, Clark W. Barrett, Subhasish Mitra
2017	J	`jnl`	Ground-Truth Adversarial Examples. CoRR Nicholas Carlini, Guy Katz, Clark W. Barrett, David L. Dill
2017	J	`jnl`	Logic Bug Detection and Localization Using Symbolic Quick Error Detection. CoRR Eshan Singh, David Lin, Clark W. Barrett, Subhasish Mitra
2017	—	`ed.`	NASA Formal Methods - 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings NFM Clark W. Barrett, Misty D. Davies, Temesghen Kahsai
2017	B	`conf`	Partitioned Memory Models for Program Analysis. VMCAI Wei Wang, Clark W. Barrett, Thomas Wies
2017	A	`conf`	Relational Constraint Solving in SMT. CADE Baoluo Meng, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
2017	—	`conf`	Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. CAV (1) Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer
2017	J	`jnl`	Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. CoRR Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer
2017	—	`conf`	SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. CAV (2) Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, Clark W. Barrett
2017	—	`conf`	Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification. CAV (2) Andrew Reynolds, Maverick Woo, Clark W. Barrett, David Brumley, Tianyi Liang, Cesare Tinelli
2017	—	`conf`	Towards Proving the Adversarial Robustness of Deep Neural Networks. FVAV@iFM Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer
2016	A	`conf`	A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. IJCAR Kshitij Bansal, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2016	J	`jnl`	An efficient SMT solver for string constraints. Formal Methods Syst. Des. Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze, Cesare Tinelli, Clark W. Barrett, Morgan Deters
2016	—	`conf`	Efficient solving of string constraints for security analysis. HotSoS Clark W. Barrett, Cesare Tinelli, Morgan Deters, Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze
2016	B	`conf`	Lazy proofs for DPLL(T)-based SMT solvers. FMCAD Guy Katz, Clark W. Barrett, Cesare Tinelli, Andrew Reynolds, Liana Hadarean
2016	J	`jnl`	Symbolic Quick Error Detection for Pre-Silicon and Post-Silicon Validation: Frequently Asked Questions. IEEE Des. Test Eshan Singh, David Lin, Clark W. Barrett, Subhasish Mitra
2015	—	`conf`	A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings. FroCos Tianyi Liang, Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
2015	A	`conf`	A structured approach to post-silicon validation and debug using symbolic quick error detection. ITC David Lin, Eshan Singh, Clark W. Barrett, Subhasish Mitra
2015	A	`conf`	Cascade - (Competition Contribution). TACAS Wei Wang, Clark W. Barrett
2015	—	`conf`	Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. CAV (2) Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett
2015	—	`conf`	Deciding Local Theory Extensions via E-matching. CAV (2) Kshitij Bansal, Andrew Reynolds, Tim King, Clark W. Barrett, Thomas Wies
2015	B	`conf`	Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors. LPAR Liana Hadarean, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli, Morgan Deters
2015	J	`jnl`	On Counterexample Guided Quantifier Instantiation for Synthesis in CVC4. CoRR Andrew Reynolds, Morgan Deters, Viktor Kuncak, Clark W. Barrett, Cesare Tinelli
2015	J	`jnl`	On Deciding Local Theory Extensions via E-matching. CoRR Kshitij Bansal, Andrew Reynolds, Tim King, Clark W. Barrett, Thomas Wies
2015	B	`conf`	Theory-Aided Model Checking of Concurrent Transition Systems. FMCAD Guy Katz, Clark W. Barrett, David Harel
2014	A*	`conf`	A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions. CAV Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett, Morgan Deters
2014	A*	`conf`	A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors. CAV Liana Hadarean, Kshitij Bansal, Dejan Jovanovic, Clark W. Barrett, Cesare Tinelli
2014	B	`conf`	A tour of CVC4: How it works, and how to use it. FMCAD Morgan Deters, Andrew Reynolds, Tim King, Clark W. Barrett, Cesare Tinelli
2014	B	`conf`	Cascade 2.0. VMCAI Wei Wang, Clark W. Barrett, Thomas Wies
2014	—	`conf`	Leveraging Linear and Mixed Integer Programming for SMT. SMT Tim King, Clark W. Barrett, Cesare Tinelli
2014	B	`conf`	Leveraging linear and mixed integer programming for SMT. FMCAD Tim King, Clark W. Barrett, Cesare Tinelli
2014	—	`conf`	SMT: Where do we go from here? SMT Clark W. Barrett
2013	J	`jnl`	"Decision Procedures: An Algorithmic Point of View, " by Daniel Kroening and Ofer Strichman, Springer-Verlag, 2008. J. Autom. Reason. Clark W. Barrett
2013	J	`jnl`	6 Years of SMT-COMP. J. Autom. Reason. Clark W. Barrett, Morgan Deters, Leonardo Mendonça de Moura, Albert Oliveras, Aaron Stump
2013	J	`jnl`	Being careful about theory combination. Formal Methods Syst. Des. Dejan Jovanovic, Clark W. Barrett
2013	A	`conf`	Quantifier Instantiation Techniques for Finite Model Finding in SMT. CADE Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic, Morgan Deters, Clark W. Barrett
2013	B	`conf`	Simplex with sum of infeasibilities for SMT. FMCAD Tim King, Clark W. Barrett, Bruno Dutertre
2013	B	`conf`	Witness Runs for Counter Machines - (Abstract). TABLEAUX Clark W. Barrett, Stéphane Demri, Morgan Deters
2013	—	`conf`	Witness Runs for Counter Machines. FroCos Clark W. Barrett, Stéphane Demri, Morgan Deters
2011	A*	`conf`	CVC4. CAV Clark W. Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, Cesare Tinelli
2011	—	`conf`	Sharing Is Caring: Combination of Theories. FroCoS Dejan Jovanovic, Clark W. Barrett
2010	—	`conf`	Polite Theories Revisited. LPAR (Yogyakarta) Dejan Jovanovic, Clark W. Barrett
2010	—	`conf`	The SMT-LIB Initiative and the Rise of SMT - (HVC 2010 Award Talk). Haifa Verification Conference Clark W. Barrett, Leonardo Mendonça de Moura, Silvio Ranise, Aaron Stump, Cesare Tinelli
2010	A*	`conf`	Verifying Low-Level Implementations of High-Level Datatypes. CAV Christopher L. Conway, Clark W. Barrett
2009	—	`ch.`	Satisfiability Modulo Theories. Handbook of Satisfiability Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, Cesare Tinelli
2009	J	`jnl`	Solving quantified verification conditions using satisfiability modulo theories. Ann. Math. Artif. Intell. Yeting Ge, Clark W. Barrett, Cesare Tinelli
2008	J	`jnl`	Design and Results of the 3rd Annual Satisfiability Modulo Theories Competition (SMT-Comp 2007). Int. J. Artif. Intell. Tools Clark W. Barrett, Morgan Deters, Albert Oliveras, Aaron Stump
2008	B	`conf`	Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors. SAS Christopher L. Conway, Dennis Dams, Kedar S. Namjoshi, Clark W. Barrett
2007	J	`jnl`	An Abstract Decision Procedure for a Theory of Inductive Data Types. J. Satisf. Boolean Model. Comput. Clark W. Barrett, Igor Shikanian, Cesare Tinelli
2007	A*	`conf`	CVC3. CAV Clark W. Barrett, Cesare Tinelli
2007	J	`jnl`	Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006). Formal Methods Syst. Des. Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump
2007	A	`conf`	Solving Quantified Verification Conditions Using Satisfiability Modulo Theories. CADE Yeting Ge, Clark W. Barrett, Cesare Tinelli
2006	—	`conf`	An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types. PDPAR/PaUL@FLoC Clark W. Barrett, Igor Shikanian, Cesare Tinelli
2006	B	`conf`	Splitting on Demand in SAT Modulo Theories. LPAR Clark W. Barrett, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli
2006	A*	`conf`	cascade: C Assertion Checker and Deductive Engine. CAV Nikhil Sethi, Clark W. Barrett
2005	J	`jnl`	An industrially effective environment for formal hardware verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Carl-Johan H. Seger, Robert B. Jones, John W. O'Leary, Thomas F. Melham, Mark D. Aagaard, Clark W. Barrett, Don Syme
2005	—	`conf`	Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite. PDPAR@CAV Sean McLaughlin, Clark W. Barrett, Yeting Ge
2005	J	`jnl`	Design and Results of the First Satisfiability Modulo Theories Competition (SMT-COMP 2005). J. Autom. Reason. Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump
2005	A*	`conf`	SMT-COMP: Satisfiability Modulo Theories Competition. CAV Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump
2005	A*	`conf`	TVOC: A Translation Validator for Optimizing Compilers. CAV Clark W. Barrett, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, Lenore D. Zuck
2005	J	`jnl`	Translation and Run-Time Validation of Loop Transformations. Formal Methods Syst. Des. Lenore D. Zuck, Amir Pnueli, Benjamin Goldberg, Clark W. Barrett, Yi Fang, Ying Hu
2005	—	`conf`	Validating More Loop Optimizations. COCV Ying Hu, Clark W. Barrett, Benjamin Goldberg, Amir Pnueli
2004	—	`conf`	A Practical Approach to Partial Functions in CVC Lite. D/PDPAR@IJCAR Sergey Berezin, Clark W. Barrett, Igor Shikanian, Marsha Chechik, Arie Gurfinkel, David L. Dill
2004	A*	`conf`	CVC Lite: A New Implementation of the Cooperating Validity Checker Category B. CAV Clark W. Barrett, Sergey Berezin
2004	—	`conf`	Combining SAT Methods with Non-Clausal Decision Heuristics. D/PDPAR@IJCAR Clark W. Barrett, Jacob Donham
2004	—	`conf`	Into the Loops: Practical Issues in Translation Validation for Optimizing Compilers. COCV Benjamin Goldberg, Lenore D. Zuck, Clark W. Barrett
2004	B	`conf`	Theory and Algorithms for the Generation and Validation of Speculative Loop Optimizations. SEFM Ying Hu, Clark W. Barrett, Benjamin Goldberg
2003	—	`conf`	Run-Time Validation of Speculative Optimizations using CVC. RV@CAV Clark W. Barrett, Benjamin Goldberg, Lenore D. Zuck
2002	—	`conf`	A Generalization of Shostak's Method for Combining Decision Procedures. FroCoS Clark W. Barrett, David L. Dill, Aaron Stump
2002	A*	`conf`	CVC: A Cooperating Validity Checker. CAV Aaron Stump, Clark W. Barrett, David L. Dill
2002	A*	`conf`	Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. CAV Clark W. Barrett, David L. Dill, Aaron Stump
2002	—	`—`	Checking validity of quantifier-free formulas in combinations of first-order theories. Clark W. Barrett
2002	—	`conf`	Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF. LFM Aaron Stump, Clark W. Barrett, David L. Dill
2001	A*	`conf`	A Decision Procedure for an Extensional Theory of Arrays. LICS Aaron Stump, Clark W. Barrett, David L. Dill, Jeremy R. Levitt
2000	A	`conf`	A Framework for Cooperating Decision Procedures. CADE Clark W. Barrett, David L. Dill, Aaron Stump
1998	A*	`conf`	A Decision Procedure for Bit-Vector Arithmetic. DAC Clark W. Barrett, David L. Dill, Jeremy R. Levitt
1996	B	`conf`	Automatic Generation of Invariants in Processor Verification. FMCAD Jeffrey X. Su, David L. Dill, Clark W. Barrett
1996	B	`conf`	Validity Checking for Combinations of Theories with Equality. FMCAD Clark W. Barrett, David L. Dill, Jeremy R. Levitt