default search action
Clark 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
Satisfiability Modulo Theories: A Beginner's Tutorial. FM (2) 2024: 571-596 - [c148]Benjamin Przybocki
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
Generalized Optimization Modulo Theories. IJCAR (1) 2024: 458-479 - [c145]Reynald Affeldt
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
Clover: Closed-Loop Verifiable Code Generation. SAIV 2024: 134-155 - [c141]Hanna Lachnitt
IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. TACAS (1) 2024: 311-330 - [i79]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) - [i78]Nestan Tsiskaridze, Clark W. Barrett, Cesare Tinelli:
Generalized Optimization Modulo Theories. CoRR abs/2404.16122 (2024) - [i77]Scott Viteri, Max Lamparth, Peter Chatain, Clark W. Barrett:
Markovian Agents for Truthful Language Modeling. CoRR abs/2404.18988 (2024) - [i76]Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett:
Verifying SQL Queries using Theories of Tables and Relations. CoRR abs/2405.03057 (2024) - [i75]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) - [i74]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) - [i73]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) - [i72]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) - [i71]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) - [i70]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) - [i69]Leni Aniva, Chuyue Sun, Brando Miranda, Clark W. Barrett, Sanmi Koyejo:
Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4. CoRR abs/2410.16429 (2024) - [i68]Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz, Andrew Reynolds, Moses Charikar, Cesare Tinelli, Clark W. Barrett:
Using Normalization to Improve SMT Solver Stability. CoRR abs/2410.22419 (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
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
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
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
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
Combining Stable Infiniteness and (Strong) Politeness. J. Autom. Reason. 67(4): 34 (2023) - [j26]Christopher A. Strong
Global optimization of objective functions represented by ReLU networks. Mach. Learn. 112(10): 3685-3712 (2023) - [j25]Kalhan Koul
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
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
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
Formal Verification of Bit-Vector Invertibility Conditions in Coq. FroCoS 2023: 41-59 - [c129]Guilherme Vicentin de Toledo
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
Toward Certified Robustness Against Real-World Distribution Shifts. SaTML 2023: 537-553 - [c121]Hanna Lachnitt, Mathias Fleury
Automatic Verification of SMT Rewrites in Isabelle/HOL. SMT 2023: 78 - [d5]Hanna Lachnitt
IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. Zenodo, 2023 - [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
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
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays. Log. Methods Comput. Sci. 18(3) (2022) - [j21]Haoze Wu
Scalable verification of GNN-based job schedulers. Proc. ACM Program. Lang. 6(OOPSLA2): 1036-1065 (2022) - [c120]Matan Ostrovsky
An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks. ATVA 2022: 391-396 - [c119]Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz
Flexible Proof Production in an Industrial-Strength SMT Solver. IJCAR 2022: 15-35 - [c118]Gereon Kremer
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
Reasoning About Vectors Using an SMT Theory of Sequences. IJCAR 2022: 125-143 - [c116]Aina Niemetz
Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers. CAV (2) 2022: 92-106 - [c115]Andres Nötzli
Even Faster Conflicts and Lazier Reductions for String Solvers. CAV (2) 2022: 205-226 - [c114]Tom Zelazny, Haoze Wu
On Optimizing Back-Substitution Methods for Neural Network Verification. FMCAD 2022: 17-26 - [c113]Omri Isac, Clark W. Barrett
Neural Network Verification with Proof Production. FMCAD 2022: 38-48 - [c112]Andres Nötzli, Haniel Barbosa, Aina Niemetz
Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language. FMCAD 2022: 65-74 - [c111]Abhishek Anil Nair, Saranyu Chattopadhyay
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
Synthesizing Instruction Selection Rewrite Rules from RTL using SMT. FMCAD 2022: 139-150 - [c109]Haoze Wu
Efficient Neural Network Analysis with Sum-of-Infeasibilities. TACAS (1) 2022: 143-163 - [c108]Haniel Barbosa
cvc5: A Versatile and Industrial-Strength SMT Solver. TACAS (1) 2022: 415-442 - [c107]Yoni Zohar
Bit-Precise Reasoning via Int-Blasting. VMCAI 2022: 496-518 - [d4]Aina Niemetz
Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers. Zenodo, 2022 - [d3]Haoze Wu
Artifact for Paper Scalable Verification of GNN-Based Job Schedulers. Zenodo, 2022 - [d2]Haoze Wu
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
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
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
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
Towards Satisfiability Modulo Parametric Bit-vectors. J. Autom. Reason. 65(7): 1001-1025 (2021) - [c106]Ying Sheng
Politeness and Stable Infiniteness: Stronger Together. CADE 2021: 148-165 - [c105]Makai Mann
Pono: A Flexible and Extensible SMT-Based Model Checker. CAV (2) 2021: 461-474 - [c104]Saranyu Chattopadhyay
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
DeepCert: Verification of Contextually Relevant Robustness for Neural Network Image Classifiers. SAFECOMP 2021: 3-17 - [c99]Makai Mann
Smt-Switch: A Solver-Agnostic C++ API for SMT Solving. SAT 2021: 377-386 - [c98]Makai Mann
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays. TACAS (1) 2021: 113-132 - [c97]Aina Niemetz
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
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
Verifying Recurrent Neural Networks Using Invariant Inference. ATVA 2020: 57-74 - [c94]Andrew Reynolds
A Decision Procedure for String to Code Point Conversion. IJCAR (1) 2020: 218-237 - [c93]Ying Sheng
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
The Move Prover. CAV (1) 2020: 137-150 - [c91]Lenny Truong, Steven Herbst, Rajsekhar Setaluri, Makai Mann, Ross G. Daly, Keyi Zhang, Caleb Donovick
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
Creating an Agile Hardware Design Flow. DAC 2020: 1-6 - [c89]Eshan Singh, Florian Lonsing, Saranyu Chattopadhyay
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
A Theoretical Framework for Symbolic Quick Error Detection. FMCAD 2020: 1-10 - [c86]Haoze Wu
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
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
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
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
Reports of the AAAI 2019 Spring Symposium Series. AI Mag. 40(3): 59-66 (2019) - [j16]Andrew Reynolds, Viktor Kuncak, Cesare Tinelli
Refutation-based synthesis in SMT. Formal Methods Syst. Des. 55(2): 73-102 (2019) - [j15]Clark W. Barrett
Selected Extended Papers of NFM 2017: Preface. J. Autom. Reason. 63(4): 1003-1004 (2019) - [c81]Haniel Barbosa
Extending SMT Solvers to Higher-Order Logic. CADE 2019: 35-54 - [c80]Aina Niemetz
Towards Bit-Width-Independent Proofs in SMT Solvers. CADE 2019: 366-384 - [c79]Andrew Reynolds
High-Level Abstractions for Simplifying Extended String Constraints in SMT. CAV (2) 2019: 23-42 - [c78]Andrew Reynolds, Haniel Barbosa
cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis. CAV (2) 2019: 74-83 - [c77]Martin Brain
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
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
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
Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores: Industrial Case Study. DATE 2019: 1000-1005 - [c73]Florian Lonsing
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
Agile SMT-Based Mapping for CGRAs with Restricted Routing Networks. ReConFig 2019: 1-8 - [c70]Andres Nötzli
Syntax-Guided Rewrite Rule Enumeration for SMT Solvers. SAT 2019: 279-297 - [c69]Alex Ozdemir
DRAT-based Bit-Vector Proofs in CVC4. SAT 2019: 298-305 - [c68]Yafim Kazak, Clark W. Barrett
Verifying Deep-RL-Driven Systems. NetAI@SIGCOMM 2019: 83-89 - [c67]Burak Ekici
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
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
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
Datatypes with Shared Selectors. IJCAR 2018: 591-608 - [c64]Aina Niemetz
Solving Quantified Bit-Vectors Using Invertibility Conditions. CAV (2) 2018: 236-255 - [c63]Mohammad Rahmani Fadiheh, Joakim Urdahl, Srinivasa Shashank Nuthakki
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
p4pktgen: Automated Test Case Generation for P4 Programs. SOSR 2018: 5:1-5:7 - [c60]Cristian Mattarei, Clark W. Barrett
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
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
Constraint solving for finite model finding in SMT solvers. Theory Pract. Log. Program. 17(4): 516-558 (2017) - [c59]Baoluo Meng
Relational Constraint Solving in SMT. CADE 2017: 148-165 - [c58]Guy Katz, Clark W. Barrett
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. CAV (1) 2017: 97-117 - [c57]Eshan Singh, Clark W. Barrett
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
SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. CAV (2) 2017: 126-133 - [c55]Andrew Reynolds, Maverick Woo, Clark W. Barrett
Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification. CAV (2) 2017: 453-474 - [c54]Andrew Reynolds, Cesare Tinelli
Designing Theory Solvers with Extensions. FroCoS 2017: 22-40 - [c53]Wei Wang, Clark W. Barrett
Partitioned Memory Models for Program Analysis. VMCAI 2017: 539-558 - [c52]Guy Katz, Clark W. Barrett
Towards Proving the Adversarial Robustness of Deep Neural Networks. FVAV@iFM 2017: 19-26 - [e1]Clark W. Barrett
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
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
An efficient SMT solver for string constraints. Formal Methods Syst. Des. 48(3): 206-234 (2016) - [c51]Kshitij Bansal, Andrew Reynolds, Clark W. Barrett
A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. IJCAR 2016: 82-98 - [c50]Guy Katz, Clark W. Barrett
Lazy proofs for DPLL(T)-based SMT solvers. FMCAD 2016: 93-100 - [c49]Clark W. Barrett
Efficient solving of string constraints for security analysis. HotSoS 2016: 4-6 - 2015
- [c48]Kshitij Bansal, Andrew Reynolds, Tim King, Clark W. Barrett
Deciding Local Theory Extensions via E-matching. CAV (2) 2015: 87-105 - [c47]Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli
Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. CAV (2) 2015: 198-216 - [c46]Guy Katz, Clark W. Barrett
Theory-Aided Model Checking of Concurrent Transition Systems. FMCAD 2015: 81-88 - [c45]Tianyi Liang, Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli
A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings. FroCos 2015: 135-150 - [c44]David Lin, Eshan Singh, Clark W. Barrett
A structured approach to post-silicon validation and debug using symbolic quick error detection. ITC 2015: 1-10 - [c43]Liana Hadarean, Clark W. Barrett
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
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
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
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
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
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
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
Witness Runs for Counter Machines. FroCos 2013: 120-150 - [c31]Clark W. Barrett
Witness Runs for Counter Machines - (Abstract). TABLEAUX 2013: 1-4 - 2011
- [c30]Clark W. Barrett
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
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
Solving quantified verification conditions using satisfiability modulo theories. Ann. Math. Artif. Intell. 55(1-2): 101-122 (2009) - [p1]Clark W. Barrett
Satisfiability Modulo Theories. Handbook of Satisfiability 2009: 825-885 - 2008
- [j6]Clark W. Barrett
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
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
Splitting on Demand in SAT Modulo Theories. LPAR 2006: 512-526 - [c20]Clark W. Barrett
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
Translation and Run-Time Validation of Loop Transformations. Formal Methods Syst. Des. 27(3): 335-360 (2005) - [j2]Clark W. Barrett
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
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
Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite. PDPAR@CAV 2005: 43-51 - [c16]Ying Hu, Clark W. Barrett
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
Combining SAT Methods with Non-Clausal Decision Heuristics. D/PDPAR@IJCAR 2004: 3-12 - [c12]Sergey Berezin, Clark W. Barrett
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
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
Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF. LFM 2002: 29-41 - 2001
- [c5]Aaron Stump, Clark W. Barrett
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
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] [i76] [i68] [j31] [j29] [j28] [j27] [c132] [c131] [c127] [c121] [d5] [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] [i78] [i76] [i68] [j31] [j29] [j28] [j27] [c136] [c132] [c131] [c130] [c127] [c121] [d5] [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-12-10 21:44 CET 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: