Google
Google Scholar
Semantic Scholar
MS Academic
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
- 2021
[j28]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)- [j27]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) - [j26]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) - [c95]Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Politeness and Stable Infiniteness: Stronger Together. CADE 2021: 148-165 - [c94]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 - [c93]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 - [c92]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 - [c91]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 - [c90]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 - [c89]Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Syntax-Guided Quantifier Instantiation. TACAS (2) 2021: 145-163 - [c88]Guy Amir, Haoze Wu, Clark W. Barrett, Guy Katz:
An SMT-Based Approach for Verifying Binarized Neural Networks. TACAS (2) 2021: 203-222 - [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
- [c87]Yuval Jacoby, Clark W. Barrett, Guy Katz:
Verifying Recurrent Neural Networks Using Invariant Inference. ATVA 2020: 57-74 - [c86]Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli:
A Decision Procedure for String to Code Point Conversion. IJCAR (1) 2020: 218-237 - [c85]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 - [c84]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 - [c83]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 - [c82]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 J. Thomas, Christopher Torng, Leonard Truong, Nestan Tsiskaridze, Keyi Zhang:
Creating an Agile Hardware Design Flow. DAC 2020: 1-6 - [c81]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 - [c80]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 - [c79]Florian Lonsing, Subhasish Mitra, Clark W. Barrett:
A Theoretical Framework for Symbolic Quick Error Detection. FMCAD 2020: 1-10 - [c78]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 - [c77]Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli:
Reductions for Strings and Regular Expressions Revisited. FMCAD 2020: 225-235 - [c76]Sumathi Gokulanathan, Alexander Feldsher, Adi Malca, Clark W. Barrett, Guy Katz:
Simplifying Neural Networks Using Formal Verification. NFM 2020: 85-93 - [c75]Makai Mann, Amalee Wilson, Cesare Tinelli, Clark W. Barrett:
Smt-Switch: A Solver-agnostic C++ API for SMT Solving. SMT 2020: 48-58 - [c74]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
- [j25]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) - [j24]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) - [j23]Clark W. Barrett, Temesghen Kahsai:
Selected Extended Papers of NFM 2017: Preface. J. Autom. Reason. 63(4): 1003-1004 (2019) - [c73]Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, Clark W. Barrett:
Extending SMT Solvers to Higher-Order Logic. CADE 2019: 35-54 - [c72]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 - [c71]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 - [c70]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 - [c69]Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Invertibility Conditions for Floating-Point Formulas. CAV (2) 2019: 116-136 - [c68]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 - [c67]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 - [c66]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 - [c65]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 - [c64]Jiaxuan You, Haoze Wu, Clark W. Barrett, Raghuram Ramanujan, Jure Leskovec:
G2SAT: Learning to Generate SAT Formulas. NeurIPS 2019: 10552-10563 - [c63]Caleb Donovick, Makai Mann, Clark W. Barrett, Pat Hanrahan:
Agile SMT-Based Mapping for CGRAs with Restricted Routing Networks. ReConFig 2019: 1-8 - [c62]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 - [c61]Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark W. Barrett:
DRAT-based Bit-Vector Proofs in CVC4. SAT 2019: 298-305 - [c60]Yafim Kazak, Clark W. Barrett, Guy Katz, Michael Schapira:
Verifying Deep-RL-Driven Systems. NetAI@SIGCOMM 2019: 83-89 - [c59]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
- [j22]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) - [c58]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 - [c57]Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, Clark W. Barrett:
Datatypes with Shared Selectors. IJCAR 2018: 591-608 - [c56]Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Solving Quantified Bit-Vectors Using Invertibility Conditions. CAV (2) 2018: 236-255 - [c55]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 - [c54]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 - [c53]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 - [c52]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
- [j21]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) - [c51]Baoluo Meng, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett:
Relational Constraint Solving in SMT. CADE 2017: 148-165 - [c50]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 - [c49]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 - [c48]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 - [c47]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 - [c46]Andrew Reynolds, Cesare Tinelli, Dejan Jovanovic, Clark W. Barrett:
Designing Theory Solvers with Extensions. FroCoS 2017: 22-40 - [c45]Wei Wang, Clark W. Barrett, Thomas Wies:
Partitioned Memory Models for Program Analysis. VMCAI 2017: 539-558 - [c44]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 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
- [j20]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) - [j19]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) - [c43]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 - [c42]Guy Katz, Clark W. Barrett, Cesare Tinelli, Andrew Reynolds, Liana Hadarean:
Lazy proofs for DPLL(T)-based SMT solvers. FMCAD 2016: 93-100 - [c41]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
- [c40]Kshitij Bansal, Andrew Reynolds, Tim King, Clark W. Barrett, Thomas Wies:
Deciding Local Theory Extensions via E-matching. CAV (2) 2015: 87-105 - [c39]Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett:
Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. CAV (2) 2015: 198-216 - [c38]Guy Katz, Clark W. Barrett, David Harel:
Theory-Aided Model Checking of Concurrent Transition Systems. FMCAD 2015: 81-88 - [c37]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 - [c36]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 - [c35]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 - [c34]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
- [c33]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 - [c32]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 - [c31]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 - [c30]Tim King, Clark W. Barrett, Cesare Tinelli:
Leveraging linear and mixed integer programming for SMT. FMCAD 2014: 139-146 - [c29]Clark W. Barrett:
SMT: Where do we go from here? SMT 2014: 1 - [c28]Tim King, Clark W. Barrett, Cesare Tinelli:
Leveraging Linear and Mixed Integer Programming for SMT. SMT 2014: 65 - [c27]Wei Wang, Clark W. Barrett, Thomas Wies:
Cascade 2.0. VMCAI 2014: 142-160 - 2013
- [j18]Dejan Jovanovic, Clark W. Barrett:
Being careful about theory combination. Formal Methods Syst. Des. 42(1): 67-90 (2013) - [j17]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) - [j16]