default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDClark W. Barrett
Person information
- affiliation: Stanford University, Computer Science Department, CA, USA
- affiliation: New York University, Department of Computer Science, NY, USA
- affiliation: Stanford University, Computer Systems Laboratory, CA, USA
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
[c152]Pei Huang, Haoze Wu, Yuting Yang, Ieva Daukantas, Min Wu, Yedi Zhang, Clark W. Barrett:
Towards Efficient Verification of Quantized Neural Networks. AAAI 2024: 21152-21160- [c151]Alex Ozdemir, Shankara Pailoor, Alp Bassa, Kostas Ferles, Clark W. Barrett, Isil Dillig:
Split Gröbner Bases for Satisfiability Modulo Finite Fields. CAV (1) 2024: 3-25 - [c150]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:
Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. CAV (2) 2024: 249-264 - [c149]Clark W. Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar:
Satisfiability Modulo Theories: A Beginner's Tutorial. FM (2) 2024: 571-596 - [c148]Benjamin Przybocki, Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett:
The Nonexistence of Unicorns and Many-Sorted Löwenheim-Skolem Theorems. FM (1) 2024: 658-675 - [c147]Haoze Wu, Clark W. Barrett, Nina Narodytska:
Lemur: Integrating Large Language Models in Automated Program Verification. ICLR 2024 - [c146]Nestan Tsiskaridze, Clark W. Barrett, Cesare Tinelli:
Generalized Optimization Modulo Theories. IJCAR (1) 2024: 458-479 - [c145]Reynald Affeldt, Clark W. Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa, Carsten Schürmann:
Robust Mean Estimation by All Means (Short Paper). ITP 2024: 39:1-39:8 - [c144]Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett:
Verifying SQL queries using theories of tables and relations. LPAR 2024: 445-463 - [c143]Pei Huang, Yuting Yang, Haoze Wu, Ieva Daukantas, Min Wu, Fuqi Jia, Clark W. Barrett:
Parallel Verification for δ-Equivalence of Neural Network Quantization. SAIV 2024: 78-99 - [c142]Chuyue Sun, Ying Sheng, Oded Padon, Clark W. Barrett:
Clover: Closed-Loop Verifiable Code Generation. SAIV 2024: 134-155 - [c141]Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli:
IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. TACAS (1) 2024: 311-330 - [i77]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:
Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. CoRR abs/2401.14461 (2024) - [i76]Nestan Tsiskaridze, Clark W. Barrett, Cesare Tinelli:
Generalized Optimization Modulo Theories. CoRR abs/2404.16122 (2024) - [i75]Scott Viteri, Max Lamparth, Peter Chatain, Clark W. Barrett:
Markovian Agents for Truthful Language Modeling. CoRR abs/2404.18988 (2024) - [i74]Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett:
Verifying SQL Queries using Theories of Tables and Relations. CoRR abs/2405.03057 (2024) - [i73]Ross Daly, Caleb Donovick, Caleb Terrill, Jackson Melchert, Priyanka Raina, Clark W. Barrett, Pat Hanrahan:
Efficiently Synthesizing Lowest Cost Rewrite Rules for Instruction Selection. CoRR abs/2405.06127 (2024) - [i72]David Dalrymple, Joar Skalse, Yoshua Bengio, Stuart Russell, Max Tegmark, Sanjit Seshia, Steve Omohundro, Christian Szegedy, Ben Goldhaber, Nora Ammann, Alessandro Abate, Joe Halpern, Clark W. Barrett, Ding Zhao, Tan Zhi-Xuan, Jeannette Wing, Joshua B. Tenenbaum:
Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems. CoRR abs/2405.06624 (2024) - [i71]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:
Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates. CoRR abs/2405.14058 (2024) - [i70]Benjamin Przybocki, Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett:
The nonexistence of unicorns and many-sorted Löwenheim-Skolem theorems. CoRR abs/2406.18912 (2024) - [i69]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:
Safe and Reliable Training of Learning-Based Aerospace Controllers. CoRR abs/2407.07088 (2024) - [i68]Min Wu, Xiaofu Li, Haoze Wu, Clark W. Barrett:
Better Verified Explanations with Applications to Incorrectness and Out-of-Distribution Detection. CoRR abs/2409.03060 (2024) - [i67]Alex Ozdemir, Shankara Pailoor, Alp Bassa, Kostas Ferles, Clark W. Barrett, Isil Dillig:
Split Gröbner Bases for Satisfiability Modulo Finite Fields. IACR Cryptol. ePrint Arch. 2024: 572 (2024) - 2023
- [j31]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:
Generating and Exploiting Automated Reasoning Proof Certificates. Commun. ACM 66(10): 86-95 (2023) - [j30]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:
Identifying and Mitigating the Security Risks of Generative AI. Found. Trends Priv. Secur. 6(1): 1-52 (2023) - [j29]Alessandro Abate, Haniel Barbosa, Clark W. Barrett, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, Andrew Reynolds, Cesare Tinelli:
Synthesising Programs with Non-trivial Constants. J. Autom. Reason. 67(2): 19 (2023) - [j28]Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli:
Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences. J. Autom. Reason. 67(3): 32 (2023) - [j27]Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Combining Stable Infiniteness and (Strong) Politeness. J. Autom. Reason. 67(4): 34 (2023) - [j26]Christopher A. Strong, Haoze Wu, Aleksandar Zeljic, Kyle D. Julian, Guy Katz, Clark W. Barrett, Mykel J. Kochenderfer:
Global optimization of objective functions represented by ReLU networks. Mach. Learn. 112(10): 3685-3712 (2023) - [j25]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 W. Barrett, Mark Horowitz, Christopher Torng, Fredrik Kjolstad, Priyanka Raina:
AHA: An Agile Approach to the Design of Coarse-Grained Reconfigurable Accelerators and Compilers. ACM Trans. Embed. Comput. Syst. 22(2): 35:1-35:34 (2023) - [c140]Dennis Wei, Haoze Wu, Min Wu, Pin-Yu Chen, Clark W. Barrett, Eitan Farchi:
Convex Bounds on the Softmax Function with Applications to Robustness Verification. AISTATS 2023: 6853-6878 - [c139]Jackson Melchert, Kathleen Feng, Caleb Donovick, Ross Daly, Ritvik Sharma, Clark W. Barrett, Mark A. Horowitz, Pat Hanrahan, Priyanka Raina:
APEX: A Framework for Automated Processing Element Design Space Exploration using Frequent Subgraph Analysis. ASPLOS (3) 2023: 33-45 - [c138]Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett:
Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness. CADE 2023: 522-541 - [c137]Alex Ozdemir, Riad S. Wahby, Fraser Brown, Clark W. Barrett:
Bounded Verification for Finite-Field-Blasting - In a Compiler for Zero Knowledge Proofs. CAV (3) 2023: 154-175 - [c136]Alex Ozdemir, Gereon Kremer, Cesare Tinelli, Clark W. Barrett:
Satisfiability Modulo Finite Fields. CAV (2) 2023: 163-186 - [c135]Omri Isac, Yoni Zohar, Clark W. Barrett, Guy Katz:
DNN Verification, Reachability, and the Exponential Function Problem. CONCUR 2023: 26:1-26:18 - [c134]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:
G-QED: Generalized QED Pre-silicon Verification beyond Non-Interfering Hardware Accelerators. DAC 2023: 1-6 - [c133]Haoze Wu, Christopher Hahn, Florian Lonsing, Makai Mann, Raghuram Ramanujan, Clark W. Barrett:
Lightweight Online Learning for Sets of Related Problems in Automated Reasoning. FMCAD 2023: 1-11 - [c132]Abdalrhman Mohamed, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery. FMCAD 2023: 189-198 - [c131]Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett:
Partitioning Strategies for Distributed SMT Solving. FMCAD 2023: 199-208 - [c130]Burak Ekici, Arjun Viswanathan, Yoni Zohar, Cesare Tinelli, Clark W. Barrett:
Formal Verification of Bit-Vector Invertibility Conditions in Coq. FroCoS 2023: 41-59 - [c129]Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett:
Combining Finite Combination Properties: Finite Models and Busy Beavers. FroCoS 2023: 159-175 - [c128]Haoze Wu, Min Wu, Dorsa Sadigh, Clark W. Barrett:
Soy: An Efficient MILP Solver for Piecewise-Affine Systems. IROS 2023: 6281-6288 - [c127]Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli, Clark W. Barrett:
An Interactive SMT Tactic in Coq using Abductive Reasoning. LPAR 2023: 11-22 - [c126]Elazar Cohen, Yizhak Yisrael Elboher, Clark W. Barrett, Guy Katz:
Tighter Abstract Queries in Neural Network Verification. LPAR 2023: 124-143 - [c125]Min Wu, Haoze Wu, Clark W. Barrett:
VeriX: Towards Verified Explainability of Deep Neural Networks. NeurIPS 2023 - [c124]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:
H2O: Heavy-Hitter Oracle for Efficient Generative Inference of Large Language Models. NeurIPS 2023 - [c123]Banghua Zhu, Ying Sheng, Lianmin Zheng, Clark W. Barrett, Michael I. Jordan, Jiantao Jiao:
Towards Optimal Caching and Model Selection for Large Model Inference. NeurIPS 2023 - [c122]Haoze Wu, Teruhiro Tagomori, Alexander Robey, Fengjun Yang, Nikolai Matni, George J. Pappas, Hamed Hassani, Corina S. Pasareanu, Clark W. Barrett:
Toward Certified Robustness Against Real-World Distribution Shifts. SaTML 2023: 537-553 - [c121]Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli:
Automatic Verification of SMT Rewrites in Isabelle/HOL. SMT 2023: 78 - [i66]Dennis Wei, Haoze Wu, Min Wu, Pin-Yu Chen, Clark W. Barrett, Eitan Farchi:
Convex Bounds on the Softmax Function with Applications to Robustness Verification. CoRR abs/2303.01713 (2023) - [i65]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:
High-throughput Generative Inference of Large Language Models with a Single GPU. CoRR abs/2303.06865 (2023) - [i64]Haoze Wu, Min Wu, Dorsa Sadigh, Clark W. Barrett:
Soy: An Efficient MILP Solver for Piecewise-Affine Systems. CoRR abs/2303.13697 (2023) - [i63]Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett:
Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness. CoRR abs/2305.02384 (2023) - [i62]Omri Isac, Yoni Zohar, Clark W. Barrett, Guy Katz:
DNN Verification, Reachability, and the Exponential Function Problem. CoRR abs/2305.06064 (2023) - [i61]Haoze Wu, Christopher Hahn, Florian Lonsing, Makai Mann, Raghuram Ramanujan, Clark W. Barrett:
Lightweight Online Learning for Sets of Related Problems in Automated Reasoning. CoRR abs/2305.11087 (2023) - [i60]Banghua Zhu, Ying Sheng, Lianmin Zheng, Clark W. Barrett, Michael I. Jordan, Jiantao Jiao:
On Optimal Caching and Model Multiplexing for Large Model Inference. CoRR abs/2306.02003 (2023) - [i59]Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett:
Partitioning Strategies for Distributed SMT Solving. CoRR abs/2306.05854 (2023) - [i58]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:
H2O: Heavy-Hitter Oracle for Efficient Generative Inference of Large Language Models. CoRR abs/2306.14048 (2023) - [i57]Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett:
Combining Finite Combination Properties: Finite Models and Busy Beavers. CoRR abs/2307.07885 (2023) - [i56]Caleb Donovick, Ross Daly, Jackson Melchert, Lenny Truong, Priyanka Raina, Pat Hanrahan, Clark W. Barrett:
PEak: A Single Source of Truth for Hardware Design and Verification. CoRR abs/2308.13106 (2023) - [i55]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:
Identifying and Mitigating the Security Risks of Generative AI. CoRR abs/2308.14840 (2023) - [i54]Haoze Wu, Clark W. Barrett, Nina Narodytska:
Lemur: Integrating Large Language Models in Automated Program Verification. CoRR abs/2310.04870 (2023) - [i53]Chuyue Sun, Ying Sheng, Oded Padon, Clark W. Barrett:
Clover: Closed-Loop Verifiable Code Generation. CoRR abs/2310.17807 (2023) - [i52]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:
Efficiently Programming Large Language Models using SGLang. CoRR abs/2312.07104 (2023) - [i51]Pei Huang, Haoze Wu, Yuting Yang, Ieva Daukantas, Min Wu, Yedi Zhang, Clark W. Barrett:
Towards Efficient Verification of Quantized Neural Networks. CoRR abs/2312.12679 (2023) - [i50]Alex Ozdemir, Gereon Kremer, Cesare Tinelli, Clark W. Barrett:
Satisfiability Modulo Finite Fields. IACR Cryptol. ePrint Arch. 2023: 91 (2023) - [i49]Alex Ozdemir, Riad S. Wahby, Fraser Brown, Clark W. Barrett:
Bounded Verification for Finite-Field-Blasting (In a Compiler for Zero Knowledge Proofs). IACR Cryptol. ePrint Arch. 2023: 778 (2023) - 2022
- [j24]Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer:
Reluplex: a calculus for reasoning about deep neural networks. Formal Methods Syst. Des. 60(1): 87-116 (2022) - [j23]Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett:
Polite Combination of Algebraic Datatypes. J. Autom. Reason. 66(3): 331-355 (2022) - [j22]Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark W. Barrett:
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays. Log. Methods Comput. Sci. 18(3) (2022) - [j21]Haoze Wu, Clark W. Barrett, Mahmood Sharif, Nina Narodytska, Gagandeep Singh:
Scalable verification of GNN-based job schedulers. Proc. ACM Program. Lang. 6(OOPSLA2): 1036-1065 (2022) - [c120]Matan Ostrovsky, Clark W. Barrett, Guy Katz:
An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks. ATVA 2022: 391-396 - [c119]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:
Flexible Proof Production in an Industrial-Strength SMT Solver. IJCAR 2022: 15-35 - [c118]Gereon Kremer, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description). IJCAR 2022: 95-105 - [c117]Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli:
Reasoning About Vectors Using an SMT Theory of Sequences. IJCAR 2022: 125-143 - [c116]Aina Niemetz, Mathias Preiner, Clark W. Barrett:
Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers. CAV (2) 2022: 92-106 - [c115]Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli:
Even Faster Conflicts and Lazier Reductions for String Solvers. CAV (2) 2022: 205-226 - [c114]Tom Zelazny, Haoze Wu, Clark W. Barrett, Guy Katz:
On Optimizing Back-Substitution Methods for Neural Network Verification. FMCAD 2022: 17-26 - [c113]Omri Isac, Clark W. Barrett, Min Zhang, Guy Katz:
Neural Network Verification with Proof Production. FMCAD 2022: 38-48 - [c112]Andres Nötzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language. FMCAD 2022: 65-74 - [c111]Abhishek Anil Nair, Saranyu Chattopadhyay, Haoze Wu, Alex Ozdemir, Clark W. Barrett:
Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers. FMCAD 2022: 84-88 - [c110]Ross Daly, Caleb Donovick, Jackson Melchert, Rajsekhar Setaluri, Nestan Tsiskaridze, Priyanka Raina, Clark W. Barrett, Pat Hanrahan:
Synthesizing Instruction Selection Rewrite Rules from RTL using SMT. FMCAD 2022: 139-150 - [c109]Haoze Wu, Aleksandar Zeljic, Guy Katz, Clark W. Barrett:
Efficient Neural Network Analysis with Sum-of-Infeasibilities. TACAS (1) 2022: 143-163 - [c108]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:
cvc5: A Versatile and Industrial-Strength SMT Solver. TACAS (1) 2022: 415-442 - [c107]Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Bit-Precise Reasoning via Int-Blasting. VMCAI 2022: 496-518 - [d4]Aina Niemetz, Mathias Preiner, Clark W. Barrett:
Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers. Zenodo, 2022
- [d3]Haoze Wu, Clark W. Barrett, Mahmood Sharif, Nina Narodytska, Gagandeep Singh:
Artifact for Paper Scalable Verification of GNN-Based Job Schedulers. Zenodo, 2022 - [d2]Haoze Wu, Aleksandar Zeljic, Guy Katz, Clark W. Barrett:
Artifact for Paper Efficient Neural Network Analysis with Sum-of-Infeasibilities. Zenodo, 2022 - [i48]Matan Ostrovsky, Clark W. Barrett, Guy Katz:
An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks. CoRR abs/2201.01978 (2022) - [i47]Haoze Wu, Clark W. Barrett, Mahmood Sharif, Nina Narodytska, Gagandeep Singh:
Scalable Verification of GNN-based Job Schedulers. CoRR abs/2203.03153 (2022) - [i46]Haoze Wu, Aleksandar Zeljic, Guy Katz, Clark W. Barrett:
Efficient Neural Network Analysis with Sum-of-Infeasibilities. CoRR abs/2203.11201 (2022) - [i45]Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli:
Reasoning About Vectors using an SMT Theory of Sequences. CoRR abs/2205.08095 (2022) - [i44]Omri Isac, Clark W. Barrett, Min Zhang, Guy Katz:
Neural Network Verification with Proof Production. CoRR abs/2206.00512 (2022) - [i43]Haoze Wu, Teruhiro Tagomori, Alexander Robey, Fengjun Yang, Nikolai Matni, George J. Pappas, Hamed Hassani, Corina S. Pasareanu, Clark W. Barrett:
Toward Certified Robustness Against Real-World Distribution Shifts. CoRR abs/2206.03669 (2022) - [i42]Tom Zelazny, Haoze Wu, Clark W. Barrett, Guy Katz:
On Optimizing Back-Substitution Methods for Neural Network Verification. CoRR abs/2208.07669 (2022) - [i41]Abhishek Nair, Saranyu Chattopadhyay, Haoze Wu, Alex Ozdemir, Clark W. Barrett:
Proof-Stitch: Proof Combination for Divide and Conquer SAT Solvers. CoRR abs/2209.05201 (2022) - [i40]Elazar Cohen, Yizhak Yisrael Elboher, Clark W. Barrett, Guy Katz:
Tighter Abstract Queries in Neural Network Verification. CoRR abs/2210.12871 (2022) - [i39]Min Wu, Haoze Wu, Clark W. Barrett:
VeriX: Towards Verified Explainability of Deep Neural Networks. CoRR abs/2212.01051 (2022) - 2021
- [j20]Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
On solving quantified bit-vector constraints using invertibility conditions. Formal Methods Syst. Des. 57(1): 87-115 (2021) - [j19]Changliu Liu, Tomer Arnon, Christopher Lazarus, Christopher A. Strong, Clark W. Barrett, Mykel J. Kochenderfer:
Algorithms for Verifying Deep Neural Networks. Found. Trends Optim. 4(3-4): 244-404 (2021) - [j18]Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli:
Towards Satisfiability Modulo Parametric Bit-vectors. J. Autom. Reason. 65(7): 1001-1025 (2021) - [c106]Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Politeness and Stable Infiniteness: Stronger Together. CADE 2021: 148-165 - [c105]Makai Mann, Ahmed Irfan, Florian Lonsing, Yahan Yang, Hongce Zhang, Kristopher Brown, Aarti Gupta, Clark W. Barrett:
Pono: A Flexible and Extensible SMT-Based Model Checker. CAV (2) 2021: 461-474 - [c104]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:
Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition. FMCAD 2021: 42-52 - [c103]Nestan Tsiskaridze, Maxwell Strange, Makai Mann, Kavya Sreedhar, Qiaoyi Liu, Mark Horowitz, Clark W. Barrett:
Automating System Configuration. FMCAD 2021: 102-111 - [c102]Alex Ozdemir, Haoze Wu, Clark W. Barrett:
SAT Solving in the Serverless Cloud. FMCAD 2021: 241-245 - [c101]Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett:
Politeness for the Theory of Algebraic Datatypes (Extended Abstract). IJCAI 2021: 4829-4833 - [c100]Colin Paterson, Haoze Wu, John Grese, Radu Calinescu, Corina S. Pasareanu, Clark W. Barrett:
DeepCert: Verification of Contextually Relevant Robustness for Neural Network Image Classifiers. SAFECOMP 2021: 3-17 - [c99]Makai Mann, Amalee Wilson, Yoni Zohar, Lindsey Stuntz, Ahmed Irfan, Kristopher Brown, Caleb Donovick, Allison Guman, Cesare Tinelli, Clark W. Barrett:
Smt-Switch: A Solver-Agnostic C++ API for SMT Solving. SAT 2021: 377-386 - [c98]Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark W. Barrett:
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays. TACAS (1) 2021: 113-132 - [c97]Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Syntax-Guided Quantifier Instantiation. TACAS (2) 2021: 145-163 - [c96]Guy Amir, Haoze Wu, Clark W. Barrett, Guy Katz:
An SMT-Based Approach for Verifying Binarized Neural Networks. TACAS (2) 2021: 203-222 - [p3]Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, Cesare Tinelli:
Satisfiability Modulo Theories. Handbook of Satisfiability 2021: 1267-1329 - [d1]Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Syntax-Guided Quantifier Instantiation (TACAS 2021 Artifact). Zenodo, 2021 - [i38]Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark W. Barrett:
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays. CoRR abs/2101.06825 (2021) - [i37]Colin Paterson, Haoze Wu, John Grese, Radu Calinescu, Corina S. Pasareanu, Clark W. Barrett:
DeepCert: Verification of Contextually Relevant Robustness for Neural Network Image Classifiers. CoRR abs/2103.01629 (2021) - [i36]Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Politeness and Stable Infiniteness: Stronger Together. CoRR abs/2104.11738 (2021) - [i35]Jackson Melchert, Kathleen Feng, Caleb Donovick, Ross Daly, Clark W. Barrett, Mark Horowitz, Pat Hanrahan, Priyanka Raina:
Automated Design Space Exploration of CGRA Processing Element Architectures using Frequent Subgraph Analysis. CoRR abs/2104.14155 (2021) - [i34]Yoni Zohar, Ahmed Irfan, Makai Mann, Andres Nötzli, Andrew Reynolds, Clark W. Barrett:
lazybvtoint at the SMT Competition 2020. CoRR abs/2105.09743 (2021) - [i33]Karthik Ganesan, Florian Lonsing, Srinivasa Shashank Nuthakki, Eshan Singh, Mohammad Rahmani Fadiheh, Wolfgang Kunz, Dominik Stoffel, Clark W. Barrett, Subhasish Mitra:
Effective Pre-Silicon Verification of Processor Cores by Breaking the Bounds of Symbolic Quick Error Detection. CoRR abs/2106.10392 (2021) - [i32]Nestan Tsiskaridze, Maxwell Strange, Makai Mann, Kavya Sreedhar, Qiaoyi Liu, Mark Horowitz, Clark W. Barrett:
Automating System Configuration. CoRR abs/2108.05987 (2021) - [i31]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:
Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition. CoRR abs/2108.06081 (2021) - 2020
- [c95]Yuval Jacoby, Clark W. Barrett, Guy Katz:
Verifying Recurrent Neural Networks Using Invariant Inference. ATVA 2020: 57-74 - [c94]Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli:
A Decision Procedure for String to Code Point Conversion. IJCAR (1) 2020: 218-237 - [c93]Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett:
Politeness for the Theory of Algebraic Datatypes. IJCAR (1) 2020: 238-255 - [c92]Jingyi Emma Zhong, Kevin Cheang, Shaz Qadeer, Wolfgang Grieskamp, Sam Blackshear, Junkil Park, Yoni Zohar, Clark W. Barrett, David L. Dill:
The Move Prover. CAV (1) 2020: 137-150 - [c91]Lenny Truong, Steven Herbst, Rajsekhar Setaluri, Makai Mann, Ross G. Daly, Keyi Zhang, Caleb Donovick, Daniel Stanley, Mark Horowitz, Clark W. Barrett, Pat Hanrahan:
fault: A Python Embedded Domain-Specific Language for Metaprogramming Portable Hardware Verification Components. CAV (1) 2020: 403-414 - [c90]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:
Creating an Agile Hardware Design Flow. DAC 2020: 1-6 - [c89]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:
A-QED Verification of Hardware Accelerators. DAC 2020: 1-6 - [c88]Keerthikumara Devarajegowda, Mohammad Rahmani Fadiheh, Eshan Singh, Clark W. Barrett, Subhasish Mitra, Wolfgang Ecker, Dominik Stoffel, Wolfgang Kunz:
Gap-free Processor Verification by S2QED and Property Generation. DATE 2020: 526-531 - [c87]Florian Lonsing, Subhasish Mitra, Clark W. Barrett:
A Theoretical Framework for Symbolic Quick Error Detection. FMCAD 2020: 1-10 - [c86]Haoze Wu, Alex Ozdemir, Aleksandar Zeljic, Kyle Julian, Ahmed Irfan, Divya Gopinath, Sadjad Fouladi, Guy Katz, Corina S. Pasareanu, Clark W. Barrett:
Parallelization Techniques for Verifying Neural Networks. FMCAD 2020: 128-137 - [c85]Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli:
Reductions for Strings and Regular Expressions Revisited. FMCAD 2020: 225-235 - [c84]Sumathi Gokulanathan, Alexander Feldsher, Adi Malca, Clark W. Barrett, Guy Katz:
Simplifying Neural Networks Using Formal Verification. NFM 2020: 85-93 - [c83]Makai Mann, Amalee Wilson, Cesare Tinelli, Clark W. Barrett:
Smt-Switch: A Solver-agnostic C++ API for SMT Solving. SMT 2020: 48-58 - [c82]Makai Mann, Clark W. Barrett:
Partial Order Reduction for Deep Bug Finding in Synchronous Hardware. TACAS (1) 2020: 367-386 - [i30]Yuval Jacoby, Clark W. Barrett, Guy Katz:
Verifying Recurrent Neural Networks using Invariant Inference. CoRR abs/2004.02462 (2020) - [i29]Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett:
Politeness for the Theory of Algebraic Datatypes. CoRR abs/2004.04854 (2020) - [i28]Sam Blackshear, David L. Dill, Shaz Qadeer, Clark W. Barrett, John C. Mitchell, Oded Padon, Yoni Zohar:
Resources: A Safe Language Abstraction for Money. CoRR abs/2004.05106 (2020) - [i27]Haoze Wu, Alex Ozdemir, Aleksandar Zeljic, Ahmed Irfan, Kyle Julian, Divya Gopinath, Sadjad Fouladi, Guy Katz, Corina S. Pasareanu, Clark W. Barrett:
Parallelization Techniques for Verifying Neural Networks. CoRR abs/2004.08440 (2020) - [i26]Florian Lonsing, Subhasish Mitra, Clark W. Barrett:
A Theoretical Framework for Symbolic Quick Error Detection. CoRR abs/2006.05449 (2020) - [i25]Lenny Truong, Steven Herbst, Rajsekhar Setaluri, Makai Mann, Ross G. Daly, Keyi Zhang, Caleb Donovick, Daniel Stanley, Mark Horowitz, Clark W. Barrett, Pat Hanrahan:
fault: A Python Embedded Domain-Specific Language For Metaprogramming Portable Hardware Verification Components. CoRR abs/2006.11669 (2020) - [i24]Makai Mann, Amalee Wilson, Cesare Tinelli, Clark W. Barrett:
Smt-Switch: a solver-agnostic C++ API for SMT Solving. CoRR abs/2007.01374 (2020) - [i23]Christopher A. Strong, Haoze Wu, Aleksandar Zeljic, Kyle D. Julian, Guy Katz, Clark W. Barrett, Mykel J. Kochenderfer:
Global Optimization of Objective Functions Represented by ReLU Networks. CoRR abs/2010.03258 (2020) - [i22]Guy Amir, Haoze Wu, Clark W. Barrett, Guy Katz:
An SMT-Based Approach for Verifying Binarized Neural Networks. CoRR abs/2011.02948 (2020)
2010 – 2019
- 2019
- [j17]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:
Reports of the AAAI 2019 Spring Symposium Series. AI Mag. 40(3): 59-66 (2019) - [j16]Andrew Reynolds, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett, Morgan Deters:
Refutation-based synthesis in SMT. Formal Methods Syst. Des. 55(2): 73-102 (2019) - [j15]Clark W. Barrett, Temesghen Kahsai:
Selected Extended Papers of NFM 2017: Preface. J. Autom. Reason. 63(4): 1003-1004 (2019) - [c81]Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, Clark W. Barrett:
Extending SMT Solvers to Higher-Order Logic. CADE 2019: 35-54 - [c80]Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli:
Towards Bit-Width-Independent Proofs in SMT Solvers. CADE 2019: 366-384 - [c79]Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli:
High-Level Abstractions for Simplifying Extended String Constraints in SMT. CAV (2) 2019: 23-42 - [c78]Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli:
cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis. CAV (2) 2019: 74-83 - [c77]Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Invertibility Conditions for Floating-Point Formulas. CAV (2) 2019: 116-136 - [c76]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:
The Marabou Framework for Verification and Analysis of Deep Neural Networks. CAV (1) 2019: 443-452 - [c75]Mohammad Rahmani Fadiheh, Dominik Stoffel, Clark W. Barrett, Subhasish Mitra, Wolfgang Kunz:
Processor Hardware Security Vulnerabilities and their Detection by Unique Program Execution Checking. DATE 2019: 994-999 - [c74]Eshan Singh, Keerthikumara Devarajegowda, Sebastian Simon, Ralf Schnieder, Karthik Ganesan, Mohammad Rahmani Fadiheh, Dominik Stoffel, Wolfgang Kunz, Clark W. Barrett, Wolfgang Ecker, Subhasish Mitra:
Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores: Industrial Case Study. DATE 2019: 1000-1005 - [c73]Florian Lonsing, Karthik Ganesan, Makai Mann, Srinivasa Shashank Nuthakki, Eshan Singh, Mario Srouji, Yahan Yang, Subhasish Mitra, Clark W. Barrett:
Unlocking the Power of Formal Hardware Verification with CoSA and Symbolic QED: Invited Paper. ICCAD 2019: 1-8 - [c72]Jiaxuan You, Haoze Wu, Clark W. Barrett, Raghuram Ramanujan, Jure Leskovec:
G2SAT: Learning to Generate SAT Formulas. NeurIPS 2019: 10552-10563 - [c71]Caleb Donovick, Makai Mann, Clark W. Barrett, Pat Hanrahan:
Agile SMT-Based Mapping for CGRAs with Restricted Routing Networks. ReConFig 2019: 1-8 - [c70]Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark W. Barrett, Cesare Tinelli:
Syntax-Guided Rewrite Rule Enumeration for SMT Solvers. SAT 2019: 279-297 - [c69]Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark W. Barrett:
DRAT-based Bit-Vector Proofs in CVC4. SAT 2019: 298-305 - [c68]Yafim Kazak, Clark W. Barrett, Guy Katz, Michael Schapira:
Verifying Deep-RL-Driven Systems. NetAI@SIGCOMM 2019: 83-89 - [c67]Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark W. Barrett, Cesare Tinelli:
Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract). PxTP 2019: 18-26 - [e2]Clark W. Barrett, Jin Yang:
2019 Formal Methods in Computer Aided Design, FMCAD 2019, San Jose, CA, USA, October 22-25, 2019. IEEE 2019, ISBN 978-0-9835678-9-9 [contents] - [i21]Eshan Singh, Keerthikumara Devarajegowda, Sebastian Simon, Ralf Schnieder, Karthik Ganesan, Mohammad Rahmani Fadiheh, Dominik Stoffel, Wolfgang Kunz, Clark W. Barrett, Wolfgang Ecker, Subhasish Mitra:
Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores: Industrial Case Study. CoRR abs/1902.01494 (2019) - [i20]Changliu Liu, Tomer Arnon, Christopher Lazarus, Clark W. Barrett, Mykel J. Kochenderfer:
Algorithms for Verifying Deep Neural Networks. CoRR abs/1903.06758 (2019) - [i19]Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli:
Towards Bit-Width-Independent Proofs in SMT Solvers. CoRR abs/1905.10434 (2019) - [i18]Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark W. Barrett:
DRAT-based Bit-Vector Proofs in CVC4. CoRR abs/1907.00087 (2019) - [i17]Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli:
CVC4SY for SyGuS-COMP 2019. CoRR abs/1907.10175 (2019) - [i16]Sumathi Gokulanathan, Alexander Feldsher, Adi Malca, Clark W. Barrett, Guy Katz:
Simplifying Neural Networks with the Marabou Verification Engine. CoRR abs/1910.12396 (2019) - [i15]Jiaxuan You, Haoze Wu, Clark W. Barrett, Raghuram Ramanujan, Jure Leskovec:
G2SAT: Learning to Generate SAT Formulas. CoRR abs/1910.13445 (2019) - 2018
- [j14]Kshitij Bansal, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli:
Reasoning with Finite Sets and Cardinality Constraints in SMT. Log. Methods Comput. Sci. 14(4) (2018) - [c66]Divya Gopinath, Guy Katz, Corina S. Pasareanu, Clark W. Barrett:
DeepSafe: A Data-Driven Approach for Assessing Robustness of Neural Networks. ATVA 2018: 3-19 - [c65]Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, Clark W. Barrett:
Datatypes with Shared Selectors. IJCAR 2018: 591-608 - [c64]Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Solving Quantified Bit-Vectors Using Invertibility Conditions. CAV (2) 2018: 236-255 - [c63]Mohammad Rahmani Fadiheh, Joakim Urdahl, Srinivasa Shashank Nuthakki, Subhasish Mitra, Clark W. Barrett, Dominik Stoffel, Wolfgang Kunz:
Symbolic quick error detection using symbolic initial state for pre-silicon verification. DATE 2018: 55-60 - [c62]Cristian Mattarei, Makai Mann, Clark W. Barrett, Ross G. Daly, Dillon Huff, Pat Hanrahan:
CoSA: Integrated Verification for Agile Hardware Design. FMCAD 2018: 1-5 - [c61]Andres Nötzli, Jehandad Khan, Andy Fingerhut, Clark W. Barrett, Peter Athanas:
p4pktgen: Automated Test Case Generation for P4 Programs. SOSR 2018: 5:1-5:7 - [c60]Cristian Mattarei, Clark W. Barrett, Shu-yu Guo, Bradley Nelson, Ben Smith:
EMME: A Formal Tool for ECMAScript Memory Model Evaluation. TACAS (2) 2018: 55-71 - [p2]Clark W. Barrett, Cesare Tinelli:
Satisfiability Modulo Theories. Handbook of Model Checking 2018: 305-343 - [i14]Lindsey Kuper, Guy Katz, Justin Gottschlich, Kyle Julian, Clark W. Barrett, Mykel J. Kochenderfer:
Toward Scalable Verification for Safety-Critical Deep Networks. CoRR abs/1801.05950 (2018) - [i13]Cristian Mattarei, Clark W. Barrett, Shu-yu Guo, Bradley Nelson, Ben Smith:
EMME: a formal tool for ECMAScript Memory Model Evaluation. CoRR abs/1801.10140 (2018) - [i12]Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
On Solving Quantified Bit-Vectors using Invertibility Conditions. CoRR abs/1804.05025 (2018) - [i11]Clark W. Barrett, Haniel Barbosa, Martin Brain, Duligur Ibeling, Tim King, Paul Meng, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Cesare Tinelli:
CVC4 at the SMT Competition 2018. CoRR abs/1806.08775 (2018) - [i10]Mohammad Rahmani Fadiheh, Dominik Stoffel, Clark W. Barrett, Subhasish Mitra, Wolfgang Kunz:
Processor Hardware Security Vulnerabilities and their Detection by Unique Program Execution Checking. CoRR abs/1812.04975 (2018) - 2017
- [j13]Andrew Reynolds, Cesare Tinelli, Clark W. Barrett:
Constraint solving for finite model finding in SMT solvers. Theory Pract. Log. Program. 17(4): 516-558 (2017) - [c59]Baoluo Meng, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett:
Relational Constraint Solving in SMT. CADE 2017: 148-165 - [c58]Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer:
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. CAV (1) 2017: 97-117 - [c57]Eshan Singh, Clark W. Barrett, Subhasish Mitra:
E-QED: Electrical Bug Localization During Post-silicon Validation Enabled by Quick Error Detection and Formal Methods. CAV (2) 2017: 104-125 - [c56]Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, Clark W. Barrett:
SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. CAV (2) 2017: 126-133 - [c55]Andrew Reynolds, Maverick Woo, Clark W. Barrett, David Brumley, Tianyi Liang, Cesare Tinelli:
Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification. CAV (2) 2017: 453-474 - [c54]Andrew Reynolds, Cesare Tinelli, Dejan Jovanovic, Clark W. Barrett:
Designing Theory Solvers with Extensions. FroCoS 2017: 22-40 - [c53]Wei Wang, Clark W. Barrett, Thomas Wies:
Partitioned Memory Models for Program Analysis. VMCAI 2017: 539-558 - [c52]Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer:
Towards Proving the Adversarial Robustness of Deep Neural Networks. FVAV@iFM 2017: 19-26 - [e1]Clark W. Barrett, Misty D. Davies, Temesghen Kahsai:
NASA Formal Methods - 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings. Lecture Notes in Computer Science 10227, 2017, ISBN 978-3-319-57287-1 [contents] - [i9]Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer:
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. CoRR abs/1702.01135 (2017) - [i8]Kshitij Bansal, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli:
A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. CoRR abs/1702.06259 (2017) - [i7]Andrew Reynolds, Cesare Tinelli, Clark W. Barrett:
Constraint Solving for Finite Model Finding in SMT Solvers. CoRR abs/1706.00096 (2017) - [i6]Eshan Singh, Clark W. Barrett, Subhasish Mitra:
E-QED: Electrical Bug Localization During Post-Silicon Validation Enabled by Quick Error Detection and Formal Methods. CoRR abs/1707.07671 (2017) - [i5]Nicholas Carlini, Guy Katz, Clark W. Barrett, David L. Dill:
Ground-Truth Adversarial Examples. CoRR abs/1709.10207 (2017) - [i4]Divya Gopinath, Guy Katz, Corina S. Pasareanu, Clark W. Barrett:
DeepSafe: A Data-driven Approach for Checking Adversarial Robustness in Neural Networks. CoRR abs/1710.00486 (2017) - [i3]Eshan Singh, David Lin, Clark W. Barrett, Subhasish Mitra:
Logic Bug Detection and Localization Using Symbolic Quick Error Detection. CoRR abs/1711.06541 (2017) - 2016
- [j12]Eshan Singh, David Lin, Clark W. Barrett, Subhasish Mitra:
Symbolic Quick Error Detection for Pre-Silicon and Post-Silicon Validation: Frequently Asked Questions. IEEE Des. Test 33(6): 55-62 (2016) - [j11]Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze, Cesare Tinelli, Clark W. Barrett, Morgan Deters:
An efficient SMT solver for string constraints. Formal Methods Syst. Des. 48(3): 206-234 (2016) - [c51]Kshitij Bansal, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. IJCAR 2016: 82-98 - [c50]Guy Katz, Clark W. Barrett, Cesare Tinelli, Andrew Reynolds, Liana Hadarean:
Lazy proofs for DPLL(T)-based SMT solvers. FMCAD 2016: 93-100 - [c49]Clark W. Barrett, Cesare Tinelli, Morgan Deters, Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze:
Efficient solving of string constraints for security analysis. HotSoS 2016: 4-6 - 2015
- [c48]Kshitij Bansal, Andrew Reynolds, Tim King, Clark W. Barrett, Thomas Wies:
Deciding Local Theory Extensions via E-matching. CAV (2) 2015: 87-105 - [c47]Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett:
Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. CAV (2) 2015: 198-216 - [c46]Guy Katz, Clark W. Barrett, David Harel:
Theory-Aided Model Checking of Concurrent Transition Systems. FMCAD 2015: 81-88 - [c45]Tianyi Liang, Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett:
A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings. FroCos 2015: 135-150 - [c44]David Lin, Eshan Singh, Clark W. Barrett, Subhasish Mitra:
A structured approach to post-silicon validation and debug using symbolic quick error detection. ITC 2015: 1-10 - [c43]Liana Hadarean, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli, Morgan Deters:
Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors. LPAR 2015: 340-355 - [c42]Wei Wang, Clark W. Barrett:
Cascade - (Competition Contribution). TACAS 2015: 420-422 - [i2]Andrew Reynolds, Morgan Deters, Viktor Kuncak, Clark W. Barrett, Cesare Tinelli:
On Counterexample Guided Quantifier Instantiation for Synthesis in CVC4. CoRR abs/1502.04464 (2015) - [i1]Kshitij Bansal, Andrew Reynolds, Tim King, Clark W. Barrett, Thomas Wies:
On Deciding Local Theory Extensions via E-matching. CoRR abs/1508.06827 (2015) - 2014
- [c41]Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett, Morgan Deters:
A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions. CAV 2014: 646-662 - [c40]Liana Hadarean, Kshitij Bansal, Dejan Jovanovic, Clark W. Barrett, Cesare Tinelli:
A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors. CAV 2014: 680-695 - [c39]Morgan Deters, Andrew Reynolds, Tim King, Clark W. Barrett, Cesare Tinelli:
A tour of CVC4: How it works, and how to use it. FMCAD 2014: 7 - [c38]Tim King, Clark W. Barrett, Cesare Tinelli:
Leveraging linear and mixed integer programming for SMT. FMCAD 2014: 139-146 - [c37]Clark W. Barrett:
SMT: Where do we go from here? SMT 2014: 1 - [c36]Tim King, Clark W. Barrett, Cesare Tinelli:
Leveraging Linear and Mixed Integer Programming for SMT. SMT 2014: 65 - [c35]Wei Wang, Clark W. Barrett, Thomas Wies:
Cascade 2.0. VMCAI 2014: 142-160 - 2013
- [j10]Dejan Jovanovic, Clark W. Barrett:
Being careful about theory combination. Formal Methods Syst. Des. 42(1): 67-90 (2013) - [j9]Clark W. Barrett, Morgan Deters, Leonardo Mendonça de Moura, Albert Oliveras, Aaron Stump:
6 Years of SMT-COMP. J. Autom. Reason. 50(3): 243-277 (2013) - [j8]Clark W. Barrett:
"Decision Procedures: An Algorithmic Point of View, " by Daniel Kroening and Ofer Strichman, Springer-Verlag, 2008. J. Autom. Reason. 51(4): 453-456 (2013) - [c34]Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic, Morgan Deters, Clark W. Barrett:
Quantifier Instantiation Techniques for Finite Model Finding in SMT. CADE 2013: 377-391 - [c33]Tim King, Clark W. Barrett, Bruno Dutertre:
Simplex with sum of infeasibilities for SMT. FMCAD 2013: 189-196 - [c32]Clark W. Barrett, Stéphane Demri, Morgan Deters:
Witness Runs for Counter Machines. FroCos 2013: 120-150 - [c31]Clark W. Barrett, Stéphane Demri, Morgan Deters:
Witness Runs for Counter Machines - (Abstract). TABLEAUX 2013: 1-4 - 2011
- [c30]Clark W. Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, Cesare Tinelli:
CVC4. CAV 2011: 171-177 - [c29]Dejan Jovanovic, Clark W. Barrett:
Sharing Is Caring: Combination of Theories. FroCoS 2011: 195-210 - 2010
- [c28]Christopher L. Conway, Clark W. Barrett:
Verifying Low-Level Implementations of High-Level Datatypes. CAV 2010: 306-320 - [c27]Clark W. Barrett, Leonardo Mendonça de Moura, Silvio Ranise, Aaron Stump, Cesare Tinelli:
The SMT-LIB Initiative and the Rise of SMT - (HVC 2010 Award Talk). Haifa Verification Conference 2010: 3 - [c26]Dejan Jovanovic, Clark W. Barrett:
Polite Theories Revisited. LPAR (Yogyakarta) 2010: 402-416
2000 – 2009
- 2009
- [j7]Yeting Ge, Clark W. Barrett, Cesare Tinelli:
Solving quantified verification conditions using satisfiability modulo theories. Ann. Math. Artif. Intell. 55(1-2): 101-122 (2009) - [p1]Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, Cesare Tinelli:
Satisfiability Modulo Theories. Handbook of Satisfiability 2009: 825-885 - 2008
- [j6]Clark W. Barrett, Morgan Deters, Albert Oliveras, Aaron Stump:
Design and Results of the 3rd Annual Satisfiability Modulo Theories Competition (SMT-Comp 2007). Int. J. Artif. Intell. Tools 17(4): 569-606 (2008) - [c25]Christopher L. Conway, Dennis Dams, Kedar S. Namjoshi, Clark W. Barrett:
Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors. SAS 2008: 62-77 - 2007
- [j5]Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump:
Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006). Formal Methods Syst. Des. 31(3): 221-239 (2007) - [j4]Clark W. Barrett, Igor Shikanian, Cesare Tinelli:
An Abstract Decision Procedure for a Theory of Inductive Data Types. J. Satisf. Boolean Model. Comput. 3(1-2): 21-46 (2007) - [c24]Yeting Ge, Clark W. Barrett, Cesare Tinelli:
Solving Quantified Verification Conditions Using Satisfiability Modulo Theories. CADE 2007: 167-182 - [c23]Clark W. Barrett, Cesare Tinelli:
CVC3. CAV 2007: 298-302 - 2006
- [c22]Nikhil Sethi, Clark W. Barrett:
cascade: C Assertion Checker and Deductive Engine. CAV 2006: 166-169 - [c21]Clark W. Barrett, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli:
Splitting on Demand in SAT Modulo Theories. LPAR 2006: 512-526 - [c20]Clark W. Barrett, Igor Shikanian, Cesare Tinelli:
An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types. PDPAR/PaUL@FLoC 2006: 23-37 - 2005
- [j3]Lenore D. Zuck, Amir Pnueli, Benjamin Goldberg, Clark W. Barrett, Yi Fang, Ying Hu:
Translation and Run-Time Validation of Loop Transformations. Formal Methods Syst. Des. 27(3): 335-360 (2005) - [j2]Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump:
Design and Results of the First Satisfiability Modulo Theories Competition (SMT-COMP 2005). J. Autom. Reason. 35(4): 373-390 (2005) - [j1]Carl-Johan H. Seger, Robert B. Jones, John W. O'Leary, Thomas F. Melham, Mark D. Aagaard, Clark W. Barrett, Don Syme:
An industrially effective environment for formal hardware verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 24(9): 1381-1405 (2005) - [c19]Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump:
SMT-COMP: Satisfiability Modulo Theories Competition. CAV 2005: 20-23 - [c18]Clark W. Barrett, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, Lenore D. Zuck:
TVOC: A Translation Validator for Optimizing Compilers. CAV 2005: 291-295 - [c17]Sean McLaughlin, Clark W. Barrett, Yeting Ge:
Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite. PDPAR@CAV 2005: 43-51 - [c16]Ying Hu, Clark W. Barrett, Benjamin Goldberg, Amir Pnueli:
Validating More Loop Optimizations. COCV@ETAPS 2005: 69-84 - 2004
- [c15]Clark W. Barrett, Sergey Berezin:
CVC Lite: A New Implementation of the Cooperating Validity Checker Category B. CAV 2004: 515-518 - [c14]Ying Hu, Clark W. Barrett, Benjamin Goldberg:
Theory and Algorithms for the Generation and Validation of Speculative Loop Optimizations. SEFM 2004: 281-289 - [c13]Clark W. Barrett, Jacob Donham:
Combining SAT Methods with Non-Clausal Decision Heuristics. D/PDPAR@IJCAR 2004: 3-12 - [c12]Sergey Berezin, Clark W. Barrett, Igor Shikanian, Marsha Chechik, Arie Gurfinkel, David L. Dill:
A Practical Approach to Partial Functions in CVC Lite. D/PDPAR@IJCAR 2004: 13-23 - [c11]Benjamin Goldberg, Lenore D. Zuck, Clark W. Barrett:
Into the Loops: Practical Issues in Translation Validation for Optimizing Compilers. COCV@ETAPS 2004: 53-71 - 2003
- [c10]Clark W. Barrett, Benjamin Goldberg, Lenore D. Zuck:
Run-Time Validation of Speculative Optimizations using CVC. RV@CAV 2003: 89-107 - 2002
- [b1]Clark W. Barrett:
Checking validity of quantifier-free formulas in combinations of first-order theories. Stanford University, USA, 2002 - [c9]Clark W. Barrett, David L. Dill, Aaron Stump:
Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. CAV 2002: 236-249 - [c8]Aaron Stump, Clark W. Barrett, David L. Dill:
CVC: A Cooperating Validity Checker. CAV 2002: 500-504 - [c7]Clark W. Barrett, David L. Dill, Aaron Stump:
A Generalization of Shostak's Method for Combining Decision Procedures. FroCoS 2002: 132-146 - [c6]Aaron Stump, Clark W. Barrett, David L. Dill:
Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF. LFM 2002: 29-41 - 2001
- [c5]Aaron Stump, Clark W. Barrett, David L. Dill, Jeremy R. Levitt:
A Decision Procedure for an Extensional Theory of Arrays. LICS 2001: 29-37 - 2000
- [c4]Clark W. Barrett, David L. Dill, Aaron Stump:
A Framework for Cooperating Decision Procedures. CADE 2000: 79-98
1990 – 1999
- 1998
- [c3]Clark W. Barrett, David L. Dill, Jeremy R. Levitt:
A Decision Procedure for Bit-Vector Arithmetic. DAC 1998: 522-527 - 1996
- [c2]Clark W. Barrett, David L. Dill, Jeremy R. Levitt:
Validity Checking for Combinations of Theories with Equality. FMCAD 1996: 187-201 - [c1]Jeffrey X. Su, David L. Dill, Clark W. Barrett:
Automatic Generation of Invariants in Processor Verification. FMCAD 1996: 377-388
Coauthor Index
Kyle Julian
aka: Kyle D. Julian
aka: Kyle D. Julian
[c149] [c144] [c141] [i74] [j31] [j29] [j28] [j27] [c132] [c131] [c127] [c121] [i59] [c119] [c118] [c117] [c115] [c112] [c108] [c107] [i45] [j20] [j18] [c106] [c97] [d1] [i36] [i34] [c94] [c85] [j16] [c81] [c80] [c79] [c78] [c77] [c70] [i19] [i17] [j14] [c65] [c64] [i12] [i11] [j13] [c59] [c56] [c55] [c54] [i8] [i7] [j11] [c51] [c50] [c49] [c48] [c47] [c45] [c43] [i2] [i1] [c41] [c39] [c34] [c30]
[c149] [c146] [c144] [c141] [i76] [i74] [j31] [j29] [j28] [j27] [c136] [c132] [c131] [c130] [c127] [c121] [i59] [i50] [c119] [c118] [c117] [c115] [c112] [c108] [c107] [i45] [j20] [j18] [c106] [c99] [c97] [p3] [d1] [i36] [c94] [c85] [c83] [i24] [j16] [c81] [c80] [c79] [c78] [c77] [c70] [c67] [i19] [i17] [j14] [c65] [c64] [p2] [i12] [i11] [j13] [c59] [c56] [c55] [c54] [i8] [i7] [j11] [c51] [c50] [c49] [c47] [c45] [c43] [i2] [c41] [c40] [c39] [c38] [c36] [c34] [c30] [c27] [j7] [p1] [j4] [c24] [c23] [c21] [c20]
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-24 21:31 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
