


Остановите войну!
for scientists:


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
- 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) - [c115]Matan Ostrovsky, Clark W. Barrett, Guy Katz:
An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks. ATVA 2022: 391-396 - [c114]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 - [c113]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 - [c112]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 - [c111]Aina Niemetz
, Mathias Preiner
, Clark W. Barrett
:
Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers. CAV (2) 2022: 92-106 - [c110]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 - [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 - [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 - [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]