Also see publications by category
“VeriX: Towards Verified Explainability of Deep Neural Networks”
by Min Wu, Haoze Wu, and Clark Barrett.
In Advances in Neural Information Processing Systems 36 (NeurIPS 2023), (A. Oh, T. Neumann, A. Globerson, K. Saenko, M. Hardt, and S. Levine, eds.), 2023, pp. 22247-22268.
Details.
“Towards Optimal Caching and Model Selection for Large Model Inference”
by Banghua Zhu, Ying Sheng, Lianmin Zheng, Clark Barrett, Michael Jordan, and Jiantao Jiao.
In Advances in Neural Information Processing Systems 36 (NeurIPS 2023), (A. Oh, T. Neumann, A. Globerson, K. Saenko, M. Hardt, and S. Levine, eds.), 2023, pp. 59062-59094.
Details.
“PEak: A Single Source of Truth for Hardware Design and Verification” by Caleb Donovick, Ross Daly, Jackson Melchert, Lenny Truong, Priyanka Raina, Pat Hanrahan, and Clark Barrett, 2023.
Details.
“Identifying and Mitigating the Security Risks of Generative AI”
by Clark Barrett, Brad Boyd, Elie Bursztein, Nicholas Carlini, Brad Chen, Jihye Choi, Amrita Roy Chowdhury, Mihai Christodorescu, Anupam Datta, Soheil Feizi, Kathleen Fisher, Tatsunori Hashimoto, Dan Hendrycks, Somesh Jha, Daniel Kang, Florian Kerschbaum, Eric Mitchell, John Mitchell, Zulfikar Ramzan, Khawaja Shams, Dawn Song, Ankur Taly, and Diyi Yang.
Foundations and Trends in Privacy and Security, vol. 6, no. 1, 2023, pp. 1-52, now publishers inc..
Details.
“H_2O: Heavy-Hitter Oracle for Efficient Generative Inference of Large Language Models”
by Zhenyu Zhang, Ying Sheng, Tianyi Zhou, Tianlong Chen, Lianmin Zheng, Ruisi Cai, Zhao Song, Yuandong Tian, Christopher Ré, Clark Barrett, Zhangyang "Atlas" Wang, and Beidi Chen.
In Advances in Neural Information Processing Systems 36 (NeurIPS 2023), (A. Oh, T. Neumann, A. Globerson, K. Saenko, M. Hardt, and S. Levine, eds.), 2023, pp. 34661-34710.
Details.
“FlexGen: High-Throughput Generative Inference of Large Language Models with a Single GPU”
by Ying Sheng, Lianmin Zheng, Binhang Yuan, Zhuohan Li, Max Ryabinin, Daniel Y. Fu, Zhiqiang Xie, Beidi Chen, Clark Barrett, Joseph E. Gonzalez, Percy Liang, Christopher Ré, Ion Stoica, and Ce Zhang.
2023.
Details.
“Soy: An Efficient MILP Solver for Piecewise-Affine Systems”
by Haoze Wu, Min Wu, Dorsa Sadigh, and Clark Barrett.
In 2023 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS '23), Oct. 2023, pp. 6281-6288. Detroit, MI, USA.
Details.
“Partitioning Strategies for Distributed SMT Solving”
by Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, and Clark Barrett.
In Proceedings of the 23^rd International Conference on Formal Methods In Computer-Aided Design (FMCAD '23), (Alexander Nadel and Kristin Yvonne Rozier, eds.), Oct. 2023, pp. 199-208. Ames, IA.
Details.
“Lightweight Online Learning for Sets of Related Problems in Automated Reasoning”
by Haoze Wu, Christopher Hahn, Florian Matthias Lonsing, Makai Mann, Raghuram Ramanujan, and Clark Barrett.
In Proceedings of the 23^rd International Conference on Formal Methods In Computer-Aided Design (FMCAD '23), (Alexander Nadel and Kristin Yvonne Rozier, eds.), Oct. 2023, pp. 23-33. Ames, IA.
Details.
“Generating and Exploiting Automated Reasoning Proof Certificates”
by Haniel Barbosa, Clark Barrett, Byron Cook, Bruno Dutertre, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Cesare Tinelli, and Yoni Zohar.
Communications of the Association for Computing Machinery (CACM), vol. 66, no. 10, Oct. 2023, pp. 86-95, Association for Computing Machinery.
Details.
“A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery”
by Abdalrhman Mohamed, Andrew Reynolds, Clark Barrett, and Cesare Tinelli.
In Proceedings of the 23^rd International Conference on Formal Methods In Computer-Aided Design (FMCAD '23), (Alexander Nadel and Kristin Yvonne Rozier, eds.), Oct. 2023, pp. 189-198. Ames, IA.
Details.
“DNN Verification, Reachability, and the Exponential Function Problem”
by Omri Isac, Yoni Zohar, Clark Barrett, and Guy Katz.
In 34^th International Conference on Concurrency Theory (CONCUR '23), (Guillermo A. Pérez and Jean-François Raskin, eds.), (Dagstuhl, Germany), Sep. 2023, pp. 26:1-26:18. Antwerp, Belgium.
Details.
“Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences”
by Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark Barrett, and Cesare Tinelli.
Journal of Automated Reasoning, vol. 67, no. 32, Sep. 2023, Springer.
Details.
“Formal Verification of Bit-Vector Invertibility Conditions in Coq”
by Burak Ekici, Arjun Viswanathan, Yoni Zohar, Cesare Tinelli, and Clark Barrett.
In Proceedings of the 14^th International Symposium on Frontiers of Combining Systems (FroCoS '23), (Uri Sattler and Martin Suda, eds.), Sep. 2023, pp. 41-59. Prague, Czech Republic.
Details.
“Combining Stable Infiniteness and (Strong) Politeness”
by Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark Barrett, and Cesare Tinelli.
Journal of Automated Reasoning, vol. 67, no. 34, Sep. 2023, Springer.
Details.
“Combining Finite Combination Properties: Finite Models and Busy Beavers”
by Guilherme V. Toledo, Yoni Zohar, and Clark Barrett.
In Proceedings of the 14^th International Symposium on Frontiers of Combining Systems (FroCoS '23), (Uri Sattler and Martin Suda, eds.), Sep. 2023, pp. 159-175. Prague, Czech Republic.
Details.
“G-QED: Generalized QED Pre-silicon Verification beyond Non-Interfering Hardware Accelerators”
by Saranyu Chattopadhyay, Keerthikumara Devarajegowda, Bihan Zhao, Florian Lonsing, Brandon A. D'Agostino, Ioanna Vavelidou, Vijay D. Bhatt, Sebastian Prebeck, Wolfgang Ecker, Caroline Trippel, Clark Barrett, and Subhasish Mitra.
In Proceedings of the 60^th Design Automation Conference (DAC '23), July 2023. San Francisco, CA.
Details.
“Satisfiability Modulo Finite Fields”
by Alex Ozdemir, Gereon Kremer, Cesare Tinelli, and Clark Barrett.
In Proceedings of the 35^th International Conference on Computer Aided Verification (CAV '23), (Constantin Enea and Akash Lal, eds.), July 2023, pp. 163-186. Paris, France.
Details.
“Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness”
by Guilherme V. Toledo, Yoni Zohar, and Clark Barrett.
In Proceedings of the 29^th International Conference on Automated Deduction (CADE '23), (Brigitte Pientka and Cesare Tinelli, eds.), July 2023, pp. 522-541. Rome, Italy.
Details.
“Bounded Verification for Finite-Field-Blasting”
by Alex Ozdemir, Riad S. Wahby, Fraser Brown, and Clark Barrett.
In Proceedings of the 35^th International Conference on Computer Aided Verification (CAV '23), (Constantin Enea and Akash Lal, eds.), July 2023, pp. 154-175. Paris, France.
Details.
“Synthesising Programs with Non-trivial Constants”
by Alessandro Abate, Haniel Barbosa, Clark Barrett, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, Andrew Reynolds, and Cesare Tinelli.
Journal of Automated Reasoning, vol. 67, no. 19, May 2023, Springer.
Details.
“Convex Bounds on the Softmax Function with Applications to Robustness Verification”
by Dennis Wei, Haoze Wu, Min Wu, Pin-Yu Chen, Clark Barrett, and Eitan Farchi.
In Proceedings of The 26^th International Conference on Artificial Intelligence and Statistics (AISTATS '23), (Francisco Ruiz, Jennifer Dy, and Jan-Willem van de Meent, eds.), Apr. 2023, pp. 6853-6878. Valencia, Spain.
Details.
“APEX: A Framework for Automated Processing Element Design Space Exploration using Frequent Subgraph Analysis”
by Jackson Melchert, Kathleen Feng, Caleb Donovick, Ross Daly, Ritvik Sharma, Clark Barrett, Mark A. Horowitz, Pat Hanrahan, and Priyanka Raina.
In Proceedings of the 28^th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), Volume 3, (New York, NY, USA), Mar. 2023, pp. 33-45. Vancouver, BC, Canada.
Details.
“Tighter Abstract Queries in Neural Network Verification”
by Elazar Cohen, Yizhak Yisrael Elboher, Clark Barrett, and Guy Katz.
In Proceedings of 24^th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR '23), (Ruzica Piskac and Andrei Voronkov, eds.), Mar. 2023, pp. 124-143. Manizales, Columbia.
Details.
“An Interactive SMT Tactic in Coq using Abductive Reasoning”
by Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli, and Clark Barrett.
In Proceedings of 24^th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR '23), (Ruzica Piskac and Andrei Voronkov, eds.), Mar. 2023, pp. 11-22. Manizales, Columbia.
Details.
“Toward Certified Robustness Against Real-World Distribution Shifts”
by Haoze Wu, Teruhiro Tagomori, Alexander Robey, Fengjun Yang, Nikolai Matni, George Pappas, Hamed Hassani, Corina P{\u{a}}s{\u{a}}reanu, and Clark Barrett.
In Proceedings of the 2023 IEEE Conference on Secure and Trustworthy Machine Learning (SaTML), (Patrick McDaniel and Nicolas Papernot, eds.), Feb. 2023, pp. 537-553. Raleigh, NC.
Details.
“Synthesizing Instruction Selection Rewrite Rules from RTL using SMT”
by Ross Daly, Caleb Donovick, Jackson Melchert, Rajsekhar Setaluri, Nestan Tsiskaridze, Priyanka Raina, Clark Barrett, and Pat Hanrahan.
In Proceedings of the 22^nd International Conference on Formal Methods In Computer-Aided Design (FMCAD '22), (Alberto Griggio and Neha Rungta, eds.), Oct. 2022, pp. 139-150.
Details.
“Scalable Verification of GNN-Based Job Schedulers”
by Haoze Wu, Clark Barrett, Mahmood Sharif, Nina Narodytska, and Gagandeep Singh.
Proceedings of the ACM on Programming Languages, vol. 6, no. OOPSLA2, Oct. 2022, pp. 1036-1065.
Details.
“Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language”
by Andres Nötzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli.
In Proceedings of the 22^nd International Conference on Formal Methods In Computer-Aided Design (FMCAD '22), (Alberto Griggio and Neha Rungta, eds.), Oct. 2022, pp. 65-74.
Details.
“Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers”
by Abhishek Nair, Saranyu Chattopadhyay, Haoze Wu, Alex Ozdemir, and Clark Barrett.
In Proceedings of the 22^nd International Conference on Formal Methods In Computer-Aided Design (FMCAD '22), (Alberto Griggio and Neha Rungta, eds.), Oct. 2022, pp. 84-88.
Details.
“On Optimizing Back-Substitution Methods for Neural Network Verification”
by Tom Zelazny, Haoze Wu, Clark Barrett, and Guy Katz.
In Proceedings of the 22^nd International Conference on Formal Methods In Computer-Aided Design (FMCAD '22), (Alberto Griggio and Neha Rungta, eds.), Oct. 2022, pp. 17-26.
Details.
“Neural Network Verification with Proof Production”
by Omri Isac, Clark Barrett, Min Zhang, and Guy Katz.
In Proceedings of the 22^nd International Conference on Formal Methods In Computer-Aided Design (FMCAD '22), (Alberto Griggio and Neha Rungta, eds.), Oct. 2022, pp. 38-48.
Details.
“An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks”
by Matan Ostrovsky, Clark Barrett, and Guy Katz.
In Proceedings of the 20^th International Symposium on Automated Technology for Verification and Analysis (ATVA '22), (Ahmed Bouajjani, Lukás Holk, and Zhilin Wu, eds.), Oct. 2022, pp. 391-396.
Details.
“Reasoning About Vectors Using an SMT Theory of Sequences”
by Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark Barrett, and Cesare Tinelli.
In Proceedings of the 11^th International Joint Conference on Automated Reasoning (IJCAR '22), (Jasmin Blanchette, Laura Kovács, and Dirk Pattinson, eds.), Aug. 2022, pp. 125-143.
Details.
“Polite Combination of Algebraic Datatypes”
by Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, and Clark Barrett.
Journal of Automated Reasoning, vol. 66, no. 3, Aug. 2022, pp. 331-335, Springer.
Details.
“Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers”
by Aina Niemetz, Mathias Preiner, and Clark Barrett.
In Proceedings of the 34^th International Conference on Computer Aided Verification (CAV '22), (Sharon Shoham and Yakir Vizel, eds.), Aug. 2022, pp. 92-106.
Details.
“Flexible Proof Production in an Industrial-Strength SMT Solver”
by 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, and Clark Barrett.
In Proceedings of the 11^th International Joint Conference on Automated Reasoning (IJCAR '22), (Jasmin Blanchette, Laura Kovács, and Dirk Pattinson, eds.), Aug. 2022, pp. 15-35.
Details.
“Even Faster Conflicts and Lazier Reductions for String Solvers”
by Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Clark Barrett, and Cesare Tinelli.
In Proceedings of the 34^th International Conference on Computer Aided Verification (CAV '22), (Sharon Shoham and Yakir Vizel, eds.), Aug. 2022, pp. 205-226.
Details.
“Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays”
by Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, and Clark Barrett.
Logical Methods in Computer Science, vol. 18, no. 3, Aug. 2022.
Details.
“Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description)”
by Gereon Kremer, Andrew Reynolds, Clark Barrett, and Cesare Tinelli.
In Proceedings of the 11^th International Joint Conference on Automated Reasoning (IJCAR '22), (Jasmin Blanchette, Laura Kovács, and Dirk Pattinson, eds.), Aug. 2022, pp. 95-105.
Details.
“AHA: An Agile Approach to the Design of Course-Grained Reconfigurable Accelerators and Compilers”
by Kalhan Koul, Jackson Melchert, Kavya Sreedhar, Leonard Truong, Gedeon Nyengele, Keyi Zhang, Qiaoyi Liu, Jeff Setter, Po-Han Chen, Yuchen Mei, Maxwell Strange, Ross Daly, Caleb Donovick, Alex Carsello, Taeyoung Kong, Kathleen Feng, Dillon Huff, Ankita Nayak, Rajsekhar Setaluri, James Thomas, Nikhil Bhagdikar, David Durst, Zachary Myers, Nestan Tsiskaridze, Stephen Richardson, Rick Bahr, Kayvon Fatahalian, Pat Hanrahan, Clark Barrett, Mark Horowitz, Christopher Torng, Fredrik Kjolstad, and Priyanka Raina.
ACM Transactions on Embedded Computing Systems, Apr. 2022.
Details.
“cvc5: A Versatile and Industrial-Strength SMT Solver”
by 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, and Yoni Zohar.
In Proceedings of the 28^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '22), (Dana Fisman and Grigore Rosu, eds.), Apr. 2022, pp. 415-442. \em Best SCP Tool Paper Award.
Details.
“Efficient Neural Network Analysis with Sum-of-Infeasibilities”
by Haoze Wu, Aleksandar Zeljic, Guy Katz, and Clark Barrett.
In Proceedings of the 28^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '22), (Dana Fisman and Grigore Rosu, eds.), Apr. 2022, pp. 143-163.
Details.
“Reluplex: a Calculus for Reasoning about Deep Neural Networks”
by Guy Katz, Clark Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer.
Formal Methods in System Design, vol. 60, Feb. 2022, pp. 87-116, Springer.
Details.
“Bit-Precise Reasoning via Int-Blasting”
by Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli.
In Proceedings of the 23^rd International Conference on Verification, Model Checking, and Abstract Interpretion (VMCAI '22), (Bernd Finkbeiner and Thomas Wies, eds.), Jan. 2022, pp. 496-518.
Details.
“Effective Pre-Silicon Verification of Processor Cores by Breaking the Bounds of Symbolic Quick Error Detection” by Karthik Ganesan, Florian Lonsing, Srinivasa Shashank Nuthakki, Eshan Singh, Mohammad Rahmani Fadiheh, Wolfgang Kunz, Dominik Stoffel, Clark Barrett, and Subhasish Mitra, 2021.
Details.
“SAT Solving in the Serverless Cloud”
by Alex Ozdemir, Haoze Wu, and Clark Barrett.
In Proceedings of the 21^st International Conference on Formal Methods In Computer-Aided Design (FMCAD '21), (Ruzica Piskac and Michael W. Whalen, eds.), Oct. 2021, pp. 241-245.
Details.
“Towards Satisfiability Modulo Parametric Bit-vectors”
by Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark Barrett, and Cesare Tinelli.
Journal of Automated Reasoning, vol. 65, no. 7, Oct. 2021, pp. 1001-1025, Springer.
Details.
“Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition”
by Saranyu Chattopadhyay, Florian Lonsing, Luca Piccolboni, Deepraj Soni, Peng Wei, Xiaofan Zhang, Yuan Zhou, Luca Carloni, Deming Chen, Jason Cong, Ramesh Karri, Zhiru Zhang, Caroline Trippel, Clark Barrett, and Subhasish Mitra.
In Proceedings of the 21^st International Conference on Formal Methods In Computer-Aided Design (FMCAD '21), (Ruzica Piskac and Michael W. Whalen, eds.), Oct. 2021, pp. 42-52.
Details.
“Global optimization of objective functions represented by ReLU networks”
by Christopher A. Strong, Haoze Wu, Aleksandar Zeljic, Kyle D. Julian, Guy Katz, Clark Barrett, and Mykel J. Kochenderfer.
Machine Learning, Oct. 2021, Springer.
Details.
“Automating System Configuration”
by Nestan Tsiskaridze, Maxwell Strange, Makai Mann, Kavya Sreedhar, Qiaoyi Liu, Mark Horowitz, and Clark Barrett.
In Proceedings of the 21^st International Conference on Formal Methods In Computer-Aided Design (FMCAD '21), (Ruzica Piskac and Michael W. Whalen, eds.), Oct. 2021, pp. 102-111.
Details.
“DeepCert: Verification of Contextually Relevant Robustness for Neural Network Image Classifiers”
by Colin Paterson, Haoze Wu, John Grese, Radu Calinescu, Corina S. P{\u{a}}s{\u{a}}reanu, and Clark Barrett.
In Computer Safety, Reliability, and Security (SAFECOMP '21), (Ibrahim Habli, Mark Sujan, and Friedemann Bitsch, eds.), Sep. 2021, pp. 3-17.
Details.
“Smt-Switch: A Solver-Agnostic C++ API for SMT Solving”
by Makai Mann, Amalee Wilson, Yoni Zohar, Lindsey Stuntz, Ahmed Irfan, Kristopher Brown, Caleb Donovick, Allison Guman, Cesare Tinelli, and Clark Barrett.
In Proceedings of the 24^th International Conference on Theory and Applications of Satisfiability Testing (SAT '21), (Chu-Min Li and Felip Manyà, eds.), July 2021, pp. 377-386. Barcelona, Spain.
Details.
“Pono: A Flexible and Extensible SMT-based Model Checker”
by Makai Mann, Ahmed Irfan, Florian Lonsing, Yahan Yang, Hongce Zhang, Kristopher Brown, Aarti Gupta, and Clark Barrett.
In Proceedings of the 33^rd International Conference on Computer Aided Verification (CAV '21), (Rustan Leino and Alexandra Silva, eds.), July 2021, pp. 461-474.
Details.
“Politeness and Stable Infiniteness: Stronger Together”
by Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark Barrett, and Cesare Tinelli.
In Proceedings of the 28^th International Conference on Automated Deduction (CADE '21), (André Platzer and Geoff Sutcliffe, eds.), July 2021, pp. 148-165.
Details.
“Syntax-Guided Quantifier Instantiation”
by Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli.
In Proceedings of the 27^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '21), (Jan Friso Groote and Kim Guldstrand Larsen, eds.), Mar. 2021, pp. 145-163.
Details.
“Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays”
by Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, and Clark Barrett.
In Proceedings of the 27^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '21), (Jan Friso Groote and Kim Guldstrand Larsen, eds.), Mar. 2021, pp. 113-132.
Details.
“An SMT-Based Approach for Verifying Binarized Neural Networks”
by Guy Amir, Haoze Wu, Clark Barrett, and Guy Katz.
In Proceedings of the 27^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '21), (Jan Friso Groote and Kim Guldstrand Larsen, eds.), Mar. 2021, pp. 203-222.
Details.
“Satisfiability Modulo Theories”
by Clark Barrett, Roberto Sebastiani, Sanjit Seshia, and Cesare Tinelli.
In Handbook of Satisfiability, Second Edition, vol. 336 of Frontiers in Artificial Intelligence and Applications, (Armin Biere, Marijn J. H. Heule, Hans van Maaren, and Toby Walsh, eds.), Feb. 2021, pp. 825-885.
Details.
“Algorithms for Verifying Deep Neural Networks”
by Changliu Liu, Tomer Arnon, Christopher Lazarus, Christopher Strong, Clark Barrett, and Mykel J. Kochenderfer.
Foundations and Trends in Optimization, vol. 4, no. 3-4, Feb. 2021, pp. 244-404, now publishers.
Details.
“On Solving Quantified Bit-Vectors using Invertibility Conditions”
by Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli.
Formal Methods in System Design, vol. 57, no. 1, Jan. 2021, pp. 87-115, Springer US.
Details.
“Resources: A Safe Language Abstraction for Money” by Sam Blackshear, David L. Dill, Shaz Qadeer, Clark W. Barrett, John C. Mitchell, Oded Padon, and Yoni Zohar, 2020.
Details.
“Global Optimization of Objective Functions Represented by ReLU Networks” by Christopher A. Strong, Haoze Wu, Aleksandar Zeljic, Kyle D. Julian, Guy Katz, Clark Barrett, and Mykel J. Kochenderfer, 2020.
Details.
“Verifying Recurrent Neural Networks Using Invariant Inference”
by Yuval Jacoby, Clark Barrett, and Guy Katz.
In Proceedings of the 18^th International Symposium on Automated Technology for Verification and Analysis (ATVA '20), (Dang Van Hung and Oleg Sokolsky, eds.), Oct. 2020, pp. 57-74.
Details.
“Towards Verification of Neural Networks for Small Unmanned Aircraft Collision Avoidance”
by Ahmed Irfan, Kyle D. Julian, Haoze Wu, Clark Barrett, Mykel J. Kochenderfer, Baoluo Meng, and James Lopez.
In Proceedings of the 39^th Digital Avionics Systems Conference (DASC '20), Oct. 2020.
Details.
“Reductions for Strings and Regular Expressions Revisited”
by Andrew Reynolds, Andres Nötzli, Clark Barrett, and Cesare Tinelli.
In Proceedings of the 20^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '20), (Alexander Ivrii and Ofer Strichman, eds.), Sep. 2020, pp. 225-235.
Details.
“Parallelization Techniques for Verifying Neural Networks”
by Haoze Wu, Alex Ozdemir, Aleksandar Zeljic, Kyle Julian, Ahmed Irfan, Divya Gopinath, Sadjad Fouladi, Guy Katz, Corina Pasareanu, and Clark Barrett.
In Proceedings of the 20^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '20), (Alexander Ivrii and Ofer Strichman, eds.), Sep. 2020, pp. 128-137.
Details.
“A Theoretical Framework for Symbolic Quick Error Detection”
by Florian Lonsing, Subhasish Mitra, and Clark Barrett.
In Proceedings of the 20^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '20), (Alexander Ivrii and Ofer Strichman, eds.), Sep. 2020, pp. 26-35.
Details.
“A-QED Verification of Hardware Accelerators”
by Eshan Singh, Florian Lonsing, Saranyu Chattopadhyay, Max Strange, Peng Wei, Xiaofan Zhang, Yuan Zhao, Jason Cong, Deming Chen, Zhiru Zhang, Priyankja Raina, Clark Barrett, and Subhasish Mitra.
In Proceedings of the 57^th Design Automation Conference (DAC '20), July 2020.
Details.
“fault: A Python Embedded Domain-Specific Language for Metaprogramming Portable Hardware Verification Components”
by Lenny Truong, Steven Herbst, Rajsekhar Setaluri, Makai Mann, Ross Daly, Keyi Zhang, Caleb Donovick, Daniel Stanley, Mark Horowitz, Clark Barrett, and Pat Hanrahan.
In Proceedings of the 32^nd International Conference on Computer Aided Verification (CAV '20), (Shuvendu K. Lahiri and Chao Wang, eds.), July 2020, pp. 403-414.
Details.
“The Move Prover”
by Jingyi Emma Zhong, Kevin Cheang, Shaz Qadeer, Wolfgang Grieskamp, Sam Blackshear, Junkil Park, Yoni Zohar, Clark Barrett, and David L. Dill.
In Proceedings of the 32^nd International Conference on Computer Aided Verification (CAV '20), (Shuvendu K. Lahiri and Chao Wang, eds.), July 2020, pp. 137-150.
Details.
“Smt-Switch: A Solver-Agnostic C++ API for SMT Solving (Extended Abstract)”
by Makai Mann, Amalee Wilson, Cesare Tinelli, and Clark Barrett.
In Proceedings of the 18^th International Workshop on Satisfiability Modulo Theories (SMT '20), July 2020.
Details.
“Politeness for the Theory of Algebraic Datatypes”
by Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, and Clark Barrett.
In Proceedings of the 10^th International Joint Conference on Automated Reasoning (IJCAR '20), (Nicolas Peltier and Viorica Sofronie-Stokkermans, eds.), July 2020, pp. 238-255. Best paper award..
Details.
“Creating an Agile Hardware Design Flow”
by R. Bahr, C. Barrett, N. Bhagdikar, A. Carsello, R. Daly, C. Donovick, D. Durst, K. Fatahalian, K. Feng, P. Hanrahan, T. Hofstee, M. Horowitz, D. Huff, F. Kjolstad, T. Kong, Q. Liu, M. Mann, J. Melchert, A. Nayak, A. Niemetz, G. Nyengele, P. Raina, S. Richardson, R. Setaluri, J. Setter, K. Sreedhar, M. Strange, J. Thomas, C. Torng, L. Truong, N. Tsiskaridze, and K. Zhang.
In Proceedings of the 57^th Design Automation Conference (DAC '20), July 2020.
Details.
“A Decision Procedure for String to Code Point Conversion”
by Andrew Reynolds, Andres Nötzli, Clark Barrett, and Cesare Tinelli.
In Proceedings of the 9^th International Joint Conference on Automated Reasoning (IJCAR '20), (Nicolas Peltier and Viorica Sofronie-Stokkermans, eds.), July 2020, pp. 218-237.
Details.
“Simplifying Neural Networks using Formal Verification”
by Sumathi Gokulanathan, Alexander Feldsher, Adi Malca, Clark Barrett, and Guy Katz.
In NASA Formal Methods: 12th International Symposium, (NFM '20), (Ritchie Lee, Susmit Jha, and Anastasia Mavridou, eds.), May 2020, pp. 85-93. Moffet Field, California.
Details.
“Partial Order Reduction for Deep Bug Finding in Synchronous Hardware”
by Makai Mann and Clark Barrett.
In Proceedings of the 26^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '20), (Armin Biere and David Parker, eds.), Apr. 2020, pp. 367-386.
Details.
“Gap-Free Processor Verification by S^2QED and Property Generation”
by Keerthikumara Devarajegowda, Mohammad Rahmani Fadiheh, Eshan Singh, Clark Barrett, Subhasish Mitra, Wolfgang Ecker, Dominik Stoffel, and Wolfgang Kunz.
In Proceedings of the 2020 Design, Automation and Test in Europe (DATE '20), Mar. 2020, pp. 526-531. Grenoble, France.
Details.
“Post-silicon validation and debug using symbolic quick error detection”
by Subhasish Mitra, Clark Barrett, David Lin, and Eshan Singh.
Jan. 2020. Patent No. 10528448.
Details.
“G2SAT: Learning to Generate SAT Formulas”
by Jiaxuan You, Haoze Wu, Clark Barrett, Raghuram Ramanujan, and Jure Leskovec.
In Advances in Neural Information Processing Systems 32 (NeurIPS '19), (H. Wallach, H. Larochelle, A. Beygelzimer, F. d'Alché-Buc, E. Fox, and R. Garnett, eds.), Dec. 2019, pp. 10552-10563. Vancouver, Canada.
Details.
Special Issue: Linearity and Special Issue: Selected Extended Papers of NFM 2017 edited by Iliano Cervesato, Maribel Fernandez, Clark Barrett, and Temesghen Kahsai, vol. 63, Springer, Dec. 2019.
Details.
“Refutation-Based Synthesis in SMT”
by Andrew Reynolds, Viktor Kuncak, Cesare Tinelli, Clark Barrett, and Morgan Deters.
Formal Methods in System Design, vol. 55, no. 2, Dec. 2019, pp. 73-102, Springer US.
Details.
“Agile SMT-Based Mapping for CGRAs with Restricted Routing Networks”
by Caleb Donovick, Makai Mann, Clark Barrett, and Pat Hanrahan.
In Proceedings of the International Conference on ReConFigurable Computing and FPGAs (ReConFig '19), (David Andrews, René Cumplido, Claudia Feregrino, and Marco Platzner, eds.), Dec. 2019. Cancun, Mexico.
Details.
“Unlocking the Power of Formal Hardware Verification with CoSA and Symbolic QED: Invited Paper”
by Florian Lonsing, Karthik Ganesan, Makai Mann, Srinivasa Shashank Nuthakki, Eshan Singh, Mario Srouji, Yahan Yang, Subhasish Mitra, and Clark Barrett.
In Proceedings of the International Conference on Computer-Aided Design (ICCAD '19), (David Pan, ed.), Nov. 2019. Westminster, Colorado.
Details.
“Proceedings of Formal Methods in Computer-Aided Design, FMCAD 2019”
edited by Clark Barrett and Jin Yang, FMCAD Inc..
Oct. 2019.
Details.
“Integration and Flight Test of Small UAS Detect and Avoid on A Miniaturized Avionics Platform”
by J. G. Lopez, L. Ren, B. Meng, R. Fisher, J. Markham, M. Figard, R. Evans, R. Evans, R. Spoelhof, M. Rubenstahl, S. Edwards, I. Pedan, and C. Barrett.
In Proceedings of the 38^th Digital Avionics Systems Conference (DASC '19), Sep. 2019.
Details.
“Verifying Deep-RL-Driven Systems”
by Yafim Kazak, Clark Barrett, Guy Katz, and Michael Schapira.
In Proceedings of the 2019 Workshop on Network Meets AI & ML (NetAI '19), Aug. 2019, pp. 83-89. Beijing, China.
Details.
“Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)”
by Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark Barrett, and Cesare Tinelli.
In Proceedings of the Sixth Workshop on Proof eXchange for Theorem Proving (PxTP '19), (Giselle Reis and Haniel Barbosa, eds.), Aug. 2019, pp. 18-26. Natal, Brazil.
Details.
“Towards Bit-Width-Independent Proofs in SMT Solvers”
by Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark Barrett, and Cesare Tinelli.
In Proceedings of the 27^th International Conference on Automated Deduction (CADE '19), (Pascal Fontaine, ed.), Aug. 2019, pp. 366-384. Natal, Brazil.
Details.
“Extending SMT Solvers to Higher-Order Logic”
by Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, and Clark Barrett.
In Proceedings of the 27^th International Conference on Automated Deduction (CADE '19), (Pascal Fontaine, ed.), Aug. 2019, pp. 35-54. Natal, Brazil.
Details.
“DRAT-based Bit-Vector Proofs in CVC4”
by Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, and Clark Barrett.
In Proceedings of the 22^nd International Conference on Theory and Applications of Satisfiability Testing (SAT '19), (Mikolá\u{s} Janota and Inês Lynce, eds.), July 2019, pp. 298-305. Lisbon, Portugal.
Details.
“CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis”
by Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Cesare Tinelli, and Clark Barrett.
In Proceedings of the 31^st International Conference on Computer Aided Verification (CAV '19), (Isil Dillig and Serdar Tasiran, eds.), July 2019, pp. 74-83. New York, New York.
Details.
“The Marabou Framework for Verification and Analysis of Deep Neural Networks”
by 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, and Clark Barrett.
In Proceedings of the 31^st International Conference on Computer Aided Verification (CAV '19), (Isil Dillig and Serdar Tasiran, eds.), July 2019, pp. 443-452. New York, New York.
Details.
“Syntax-Guided Rewrite Rule Enumeration for SMT Solvers”
by Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark Barrett, and Cesare Tinelli.
In Proceedings of the 22^nd International Conference on Theory and Applications of Satisfiability Testing (SAT '19), (Mikolá\u{s} Janota and Inês Lynce, eds.), July 2019, pp. 279-297. Lisbon, Portugal.
Details.
“Invertibility Conditions for Floating-Point Formulas”
by Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli.
In Proceedings of the 31^st International Conference on Computer Aided Verification (CAV '19), (Isil Dillig and Serdar Tasiran, eds.), July 2019, pp. 116-136. New York, New York.
Details.
“High-Level Abstractions for Simplifying Extended String Constraints in SMT”
by Andrew Reynolds, Andres Nötzli, Clark Barrett, and Cesare Tinelli.
In Proceedings of the 31^st International Conference on Computer Aided Verification (CAV '19), (Isil Dillig and Serdar Tasiran, eds.), July 2019, pp. 23-42. New York, New York.
Details.
“Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores: Industrial Case Study”
by E. Singh, K. Devarajegowda, S. Simon, R. Schnieder, K. Ganesan, M. Fadiheh, D. Stoffel, W. Kunz, C. Barrett, W. Ecker, and S. Mitra.
In Proceedings of the 2019 Design, Automation and Test in Europe (DATE '19), Mar. 2019, pp. 1000-1005. Florence, Italy.
Details.
“Processor Hardware Security Vulnerabilities and their Detection by Unique Program Execution Checking”
by M. R. Fadiheh, D. Stoffel, C. Barrett, S. Mitra, and W. Kunz.
In Proceedings of the 2019 Design, Automation and Test in Europe (DATE '19), Mar. 2019, pp. 994-999. Florence, Italy.
Details.
“Toward Scalable Verification for Safety-Critical Deep Networks” by Lindsey Kuper, Guy Katz, Justin Gottschlich, Kyle Julian, Clark Barrett, and Mykel Kochenderfer, 2018.
Details.
“Satisfiability Modulo Theories”
by Clark Barrett and Cesare Tinelli.
In Handbook of Model Checking, (Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, eds.), 2018, pp. 305-343.
Details.
“Provably Minimally-Distorted Adversarial Examples” by Nicholas Carlini, Guy Katz, Clark Barrett, and David L. Dill, 2018.
Details.
“Logic Bug Detection and Localization Using Symbolic Quick Error Detection”
by Eshan Singh, David Lin, Clark Barrett, and Subhasish Mitra.
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2018, IEEE.
Details.
“Reasoning with Finite Sets and Cardinality Constraints in SMT”
by Kshitij Bansal, Clark Barrett, Andrew Reynolds, and Cesare Tinelli.
Logical Methods in Computer Science, vol. 14, no. 4, Nov. 2018.
Details.
“CoSA: Integrated Verification for Agile Hardware Design”
by Cristian Mattarei, Makai Mann, Clark Barrett, Ross G. Daly, Dillon Huff, and Pat Hanrahan.
In Proceedings of the 18^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '18), (Nikolaj Bjørner and Arie Gurfinkel, eds.), Oct. 2018, pp. 7-11. Austin, Texas.
Details.
“DeepSafe: A Data-driven Approach for Assessing Robustness of Neural Networks”
by Divya Gopinath, Guy Katz, Corina S. P\u{a}s\u{a}reanu, and Clark Barrett.
In Proceedings of the 16^th International Symposium on Automated Technology for Verification and Analysis (ATVA '18), (Shuvendu Lahiri and Chao Wang, eds.), Oct. 2018, pp. 3-19. Los Angeles, California.
Details.
“Solving Quantified Bit-Vectors using Invertibility Conditions”
by Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli.
In Proceedings of the 30^th International Conference on Computer Aided Verification (CAV '18), (Hana Chockler and Georg Weissenbacher, eds.), July 2018, pp. 236-255. Oxford, United Kingdom.
Details.
“Rewrites for SMT Solvers using Syntax-Guided Enumeration”
by Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Andres Nötzli, Mathias Preiner, Clark Barrett, and Cesare Tinelli.
In Proceedings of the 16^th International Workshop on Satisfiability Modulo Theories (SMT '18), July 2018. Oxford, United Kingdom.
Details.
“Datatypes with Shared Selectors”
by Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, and Clark Barrett.
In Proceedings of the 9^th International Joint Conference on Automated Reasoning (IJCAR '18), (Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, eds.), June 2018, pp. 591-608. Oxford, United Kingdom.
Details.
“EMME: a formal tool for ECMAScript Memory Model Evaluation”
by Cristian Mattarei, Clark Barrett, Shu-yu Guo, Bradley Nelson, and Ben Smith.
In Proceedings of the 24^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '18), (Dirk Beyer and Marieke Huisman, eds.), Apr. 2018, pp. 55-71. Thessaloniki, Greece. Distinguished Artifact Award..
Details.
“p4pktgen: Automated Test Case Generation for P4 Programs”
by Andres Nötzli, Jehandad Khan, Andy Fingerhut, Clark Barrett, and Peter Athanas.
In Proceedings of the ACM Symposium on SDN Research (SOSR '18), Mar. 2018, pp. 5:1-5:7. Los Angeles, California.
Details.
“Symbolic quick error detection using symbolic initial state for pre-silicon verification”
by M. R. Fadiheh, J. Urdahl, S. S. Nuthakki, S. Mitra, C. Barrett, D. Stoffel, and W. Kunz.
In Proceedings of the 2018 Design, Automation and Test in Europe (DATE '18), Mar. 2018, pp. 55-60. Dresden, Germany.
Details.
“Towards Proving the Adversarial Robustness of Deep Neural Networks”
by Guy Katz, Clark Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer.
In Proceedings of the First Workshop on Formal Verification of Autonomous Vehicles (FVAV '17), (Lukas Bulwahn, Maryam Kamali, and Sven Linker, eds.), Sep. 2017, pp. 19-26. Turin, Italy.
Details.
“Designing Theory Solvers with Extensions”
by Andrew Reynolds, Cesare Tinelli, Dejan Jovanovic, and Clark Barrett.
In Proceedings of the 11^th International Symposium on Frontiers of Combining Systems (FroCoS '17), (Clare Dixon and Marcelo Finger, eds.), Sep. 2017, pp. 22-40. Brasilia, Brazil.
Details.
“Relational Constraint Solving in SMT”
by Baoluo Meng, Andrew Reynolds, Cesare Tinelli, and Clark Barrett.
In Proceedings of the 26^th International Conference on Automated Deduction (CADE '17), (Leonardo de Moura, ed.), Aug. 2017, pp. 148-165. Gothenburg, Sweden.
Details.
“SMTCoq: A Plug-In for Integrating SMT Solvers into Coq”
by Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, and Clark Barrett.
In Proceedings of the 29^th International Conference on Computer Aided Verification (CAV '17), (Rupak Majumdar and Viktor Kuncak, eds.), July 2017, pp. 126-136. Heidelberg, Germany.
Details.
“E-QED: Electrical Bug Localization During Post-Silicon Validation Enabled by Quick Error Detection and Formal Methods”
by Eshan Singh, Clark Barrett, and Subhasish Mitra.
In Proceedings of the 29^th International Conference on Computer Aided Verification (CAV '17), (Rupak Majumdar and Viktor Kuncak, eds.), July 2017, pp. 104-125. Heidelberg, Germany.
Details.
“Scaling up DPLL(T) String Solvers Using Context-Dependent Simplification”
by Andrew Reynolds, Maverick Woo, Clark Barrett, David Brumley, Tianyi Liang, and Cesare Tinelli.
In Proceedings of the 29^th International Conference on Computer Aided Verification (CAV '17), (Rupak Majumdar and Viktor Kuncak, eds.), July 2017, pp. 453-474. Heidelberg, Germany.
Details.
“Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks”
by Guy Katz, Clark Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer.
In Proceedings of the 29^th International Conference on Computer Aided Verification (CAV '17), (Rupak Majumdar and Viktor Kuncak, eds.), July 2017, pp. 97-117. Heidelberg, Germany.
Details.
“Constraint solving for finite model finding in SMT solvers”
by Andrew Reynolds, Cesare Tinelli, and Clark Barrett.
Theory and Practice of Logic Programming, vol. 17, no. 4, July 2017, pp. 516-558, Cambridge University Press.
Details.
“NASA Formal Methods: 9th International Symposium, NFM 2017”
edited by Clark Barrett, Misty Davies, and Temesghen Kahsai, Springer.
May 2017.
Details.
“Partitioned Memory Models for Program Analysis”
by Wei Wang, Clark Barrett, and Thomas Wies.
In Proceedings of the 18^th International Conference on Verification, Model Checking, and Abstract Interpretion (VMCAI '17), (Ahmed Bouajjani and David Monniaux, eds.), Jan. 2017, pp. 539-558. Paris, France.
Details.
“Symbolic Quick Error Detection for Pre-Silicon and Post-Silicon Validation: Frequently Asked Questions”
by Eshan Singh, David Lin, Clark Barrett, and Subhasish Mitra.
IEEE Design & Test, vol. 33, no. 6, Dec. 2016, pp. 55-62, IEEE.
Details.
“Lazy Proofs for DPLL(T)-Based SMT Solvers”
by Guy Katz, Clark Barrett, Cesare Tinelli, Andrew Reynolds, and Liana Hadarean.
In Proceedings of the 16^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '16), (Ruzica Piskac and Muralidhar Talupur, eds.), Oct. 2016, pp. 93-100. Mountain View, California. Best paper award..
Details.
“An Efficient SMT Solver for String Constraints”
by Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze, Cesare Tinelli, Clark Barrett, and Morgan Deters.
Formal Methods in System Design, vol. 48, no. 3, June 2016, pp. 206-234, Springer US.
Details.
“A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT”
by Kshitij Bansal, Andrew Reynolds, Clark Barrett, and Cesare Tinelli.
In Proceedings of the 8^th International Joint Conference on Automated Reasoning (IJCAR '16), (Nicola Olivetti and Ashish Tiwari, eds.), June 2016, pp. 82-98. Coimbra, Portugal.
Details.
“Fine-grained SMT Proofs for the Theory of Fixed-width Bit-vectors”
by Liana Hadarean, Clark Barrett, Andrew Reynolds, Cesare Tinelli, and Morgan Deters.
In Proceedings of the 20^th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '15), (Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov, eds.), Nov. 2015, pp. 340-355. Suva, Fiji.
Details.
“A Structured Approach to Post-Silicon Validation and Debug using Symbolic Quick Error Detection”
by David Lin, Eshan Singh, Clark Barrett, and Subhasish Mitra.
In Proceedings of the 42^nd International Test Conference (ITC '15), Oct. 2015, pp. 1-10. Anaheim, California. Best paper award..
Details.
“Theory-Aided Model Checking of Concurrent Transition Systems”
by Guy Katz, Clark Barrett, and David Harel.
In Proceedings of the 15^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '15), Sep. 2015, pp. 81-88. Austin, Texas.
Details.
“A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings”
by Tianyi Liang, Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli, and Clark Barrett.
In Proceedings of the 10^th International Symposium on Frontiers of Combining Systems (FroCoS '15), (Carsten Lutz and Silvio Ranise, eds.), Sep. 2015, pp. 135-150. Wroclaw, Poland.
Details.
“Deciding Local Theory Extensions via E-matching”
by Kshitij Bansal, Andrew Reynolds, Tim King, Clark Barrett, and Thomas Wies.
In Proceedings of the 27^th International Conference on Computer Aided Verification (CAV '15), (Daniel Kroening and Corina S. P\u{a}s\u{a}reanu, eds.), July 2015, pp. 87-105. San Francisco, California.
Details.
“Counterexample Guided Quantifier Instantiation for Synthesis in SMT”
by Andrew Reynolds, Morgan Deters, Viktor Kuncak, Clark Barrett, and Cesare Tinelli.
In Proceedings of the 27^th International Conference on Computer Aided Verification (CAV '15), (Daniel Kroening and Corina S. P\u{a}s\u{a}reanu, eds.), July 2015, pp. 198-216. San Francisco, California.
Details.
“Cascade (Competition Contribution)”
by Wei Wang and Clark Barrett.
In Proceedings of the 21^st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '15), (Christel Baier and Cesare Tinelli, eds.), Apr. 2015, pp. 420-422. London, United Kingdom.
Details.
“Proofs in Satisfiability Modulo Theories”
by Clark Barrett, Leonardo de Moura, and Pascal Fontaine.
In All about Proofs, Proofs for All, vol. 55 of Mathematical Logic and Foundations, (David Delahaye and Bruno Woltzenlogel Paleo, eds.), (London, UK), Jan. 2015, pp. 23-44.
Details.
“Leveraging Linear and Mixed Integer Programming for SMT”
by Tim King, Clark Barrett, and Cesare Tinelli.
In Proceedings of the 14^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '14), Oct. 2014, pp. 139-146. Lausanne, Switzerland.
Details.
“A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions”
by Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark Barrett, and Morgan Deters.
In Proceedings of the 26^th International Conference on Computer Aided Verification (CAV '14), (Armin Biere and Roderick Bloem, eds.), July 2014, pp. 646-662. Vienna, Austria.
Details.
“A Tale of Two Solvers: Eager and Lazy Approaches to Bit-vectors”
by Liana Hadarean, Clark Barrett, Dejan Jovanovic, Cesare Tinelli, and Kshitij Bansal.
In Proceedings of the 26^th International Conference on Computer Aided Verification (CAV '14), (Armin Biere and Roderick Bloem, eds.), July 2014, pp. 680-695. Vienna, Austria.
Details.
“Problem Solving for the 21st Century: Efficient Solvers for Satisfiability Modulo Theories”
by Clark Barrett, Daniel Kroening, and Thomas Melham.
London Mathematical Society and Smith Institute for Industrial Mathematics and System Engineering technical report 3, June 2014. Knowledge Transfer Report.
Details.
“Cascade 2.0”
by Wei Wang, Clark Barrett, and Thomas Wies.
In Proceedings of the 15^th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI '14), (Kenneth L. McMillan and Xavier Rival, eds.), Jan. 2014, pp. 142-160. San Diego, California.
Details.
“Quantifier Instantiation Techniques for Finite Model Finding in SMT”
by Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic, Morgan Deters, and Clark Barrett.
In Proceedings of the 24^th International Conference on Automated Deduction (CADE '13), (Maria Paola Bonacina, ed.), 2013, pp. 377-391. Lake Placid, New York.
Details.
““Decision Procedures:An Algorithmic Point of View,”
by Daniel Kroening and Ofer Strichman, Springer-Verlag, 2008” by Clark Barrett.
Journal of Automated Reasoning, vol. 51, no. 4, Dec. 2013, pp. 453-456, Springer Netherlands.
Details.
“The Design and Implementation of the Model Constructing Satisfiability Calculus”
by Dejan Jovanovic, Clark Barrett, and Leonardo de Moura.
In Proceedings of the 13^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '13), Oct. 2013, pp. 173-180. Portland, Oregon.
Details.
“Simplex with Sum of Infeasibilities for SMT”
by Timothy King, Clark Barrett, and Bruno Dutertre.
In Proceedings of the 13^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '13), Oct. 2013, pp. 189-196. Portland, Oregon.
Details.
“Witness Runs for Counter Machines”
by Clark Barrett, Stephané Demri, and Morgan Deters.
In Proceedings of the 9^th International Symposium on Frontiers of Combining Systems (FroCoS '13), (Pascal Fontaine, Christophe Ringeissen, and Renate A. Schmidt, eds.), Sep. 2013, pp. 120-150. Nancy, France.
Details.
“6 Years of SMT-COMP”
by Clark Barrett, Morgan Deters, Leonardo de Moura, Albert Oliveras, and Aaron Stump.
Journal of Automated Reasoning, vol. 50, no. 3, Mar. 2013, pp. 243-277, Springer Netherlands.
Details.
“Being Careful about Theory Combination”
by Dejan Jovanovic and Clark Barrett.
Formal Methods in System Design, vol. 42, no. 1, Feb. 2013, pp. 67-90, Springer US.
Details.
“Sharing is Caring: Combination of Theories”
by Dejan Jovanovic and Clark Barrett.
In Proceedings of the 8^th International Symposium on Frontiers of Combining Systems (FroCoS '11), (Cesare Tinelli and Viorica Sofronie-Stokkermans, eds.), Oct. 2011, pp. 195-210. Saarbrücken, Germany.
Details.
“Sharing is Caring: Combination of Theories”
by Dejan Jovanovic and Clark Barrett, Depatrment of Computer Science.
New York University technical report TR2011-940, Oct. 2011.
Details.
“CVC4”
by Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, and Cesare Tinelli.
In Proceedings of the 23^rd International Conference on Computer Aided Verification (CAV '11), (Ganesh Gopalakrishnan and Shaz Qadeer, eds.), July 2011, pp. 171-177. Snowbird, Utah.
Details.
“Exploring and Categorizing Error Spaces using BMC and SMT”
by Tim King and Clark Barrett.
In Proceedings of the 9^th International Workshop on Satisfiability Modulo Theories (SMT '11), July 2011. Snowbird, Utah.
Details.
“Polite Theories Revisited”
by Dejan Jovanovic and Clark Barrett.
In Proceedings of the 17^th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '10), (Christian G. Fermüller and Andrei Voronkov, eds.), Oct. 2010, pp. 402-416. Yogyakarta, Indonesia.
Details.
“Verifying Low-Level Implementations of High-Level Datatypes”
by Christopher L. Conway and Clark Barrett.
In Proceedings of the 22^nd International Conference on Computer Aided Verification (CAV '10), (Tayssir Touili, Byron Cook, and Paul Jackson, eds.), July 2010, pp. 306-320. Edinburgh, Scotland.
Details.
“The SMT-LIB Standard -- Version 2.0”
by Clark Barrett, Aaron Stump, and Cesare Tinelli.
In Proceedings of the 8^th International Workshop on Satisfiability Modulo Theories (SMT '10), July 2010. Edinburgh, Scotland.
Details.
“Sharing is Caring”
by Dejan Jovanovic and Clark Barrett.
In Proceedings of the 8^th International Workshop on Satisfiability Modulo Theories (SMT '10), July 2010. Edinburgh, Scotland.
Details.
“Design and Results of the 4^th Annual Satisfiability Modulo Theories Competition (SMT-COMP 2008)”
by Clark Barrett, Morgan Deters, Albert Oliveras, and Aaron Stump, Depatrment of Computer Science.
New York University technical report TR2010-931, July 2010.
Details.
“Comparing Proof Systems for Linear Real Arithmetic with LFSC”
by Andrew Reynolds, Liana Hadarean, Cesare Tinelli, Yeting Ge, Aaron Stump, and Clark Barrett.
In Proceedings of the 8^th International Workshop on Satisfiability Modulo Theories (SMT '10), July 2010. Edinburgh, Scotland.
Details.
“Polite Theories Revisited”
by Dejan Jovanovic and Clark Barrett, Depatrment of Computer Science.
New York University technical report TR2010-922, Jan. 2010.
Details.
“Solving Quantified Verification Conditions using Satisfiability Modulo Theories”
by Yeting Ge, Clark Barrett, and Cesare Tinelli.
Annals of Mathematics and Artificial Intelligence, vol. 55, no. 1-2, Feb. 2009, pp. 101-122, Springer.
Details.
“Satisfiability Modulo Theories”
by Clark Barrett, Roberto Sebastiani, Sanjit Seshia, and Cesare Tinelli.
In Handbook of Satisfiability, vol. 185 of Frontiers in Artificial Intelligence and Applications, (Armin Biere, Marijn J. H. Heule, Hans van Maaren, and Toby Walsh, eds.), Feb. 2009, pp. 825-885.
Details.
“Design and Results of the 3^rd Annual Satisfiability Modulo Theories Competition (SMT-COMP 2007)”
by Clark Barrett, Morgan Deters, Albert Oliveras, and Aaron Stump.
International Journal on Artificial Intelligence Tools (IJAIT), vol. 17, no. 4, Aug. 2008, pp. 569-606, World Scientific.
Details.
“Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors”
by Christopher L. Conway, Dennis Dams, Kedar S. Namjoshi, and Clark Barrett.
In Proceedings of the 15^th International Static Analysis Symposium (SAS '08), (Mara Alpuente and Germán Vidal, eds.), July 2008, pp. 62-77. Valencia, Spain.
Details.
“Points-to Analysis, Conditional Soundness, and Proving the Absence of Errors”
by Christopher L. Conway, Dennis Dams, Kedar S. Namjoshi, and Clark Barrett, Depatrment of Computer Science.
New York University technical report TR2008-910, Mar. 2008.
Details.
“An Abstract Decision Procedure for a Theory of Inductive Data Types”
by Clark Barrett, Igor Shikanian, and Cesare Tinelli.
Journal on Satisfiability, Boolean Modeling and Computation, vol. 3, 2007, pp. 21-46, IOS Press.
Details.
“Design and Results of the 2^nd Satisfiability Modulo Theories Competition (SMT-COMP 2006)”
by Clark Barrett, Leonardo de Moura, and Aaron Stump.
Formal Methods in System Design, vol. 31, no. 3, Dec. 2007, pp. 221-239, Springer Netherlands.
Details.
“CVC3”
by Clark Barrett and Cesare Tinelli.
In Proceedings of the 19^th International Conference on Computer Aided Verification (CAV '07), (Werner Damm and Holger Hermanns, eds.), July 2007, pp. 298-302. Berlin, Germany.
Details.
“Solving Quantified Verification Conditions using Satisfiability Modulo Theories”
by Yeting Ge, Clark Barrett, and Cesare Tinelli.
In Proceedings of the 21^st International Conference on Automated Deduction (CADE '07), (Frank Pfenning, ed.), July 2007, pp. 167-182. Bremen, Germany.
Details.
“An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types”
by Clark Barrett, Igor Shikanian, and Cesare Tinelli.
In Combined Proceedings of the 4^th Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR '06) and the 1^st International Workshop on Probabilistic Automata and Logics (PaUL '06), (Byron Cook and Roberto Sebastiani, eds.), June 2007, pp. 23-37. Seattle, Washington.
Details.
“Splitting on Demand in SAT Modulo Theories”
by Clark Barrett, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli.
In Proceedings of the 13^th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '06), (Miki Hermann and Andrei Voronkov, eds.), Nov. 2006, pp. 512-526. Phnom Penh, Cambodia.
Details.
“CASCADE: C Assertion Checker and Deductive Engine”
by Nikhil Sethi and Clark Barrett.
In Proceedings of the 18^th International Conference on Computer Aided Verification (CAV '06), (Thomas Ball and Robert B. Jones, eds.), Aug. 2006, pp. 166-169. Seattle, Washington.
Details.
“Splitting on Demand in SAT Modulo Theories”
by Clark Barrett, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli, Department of Computer Science.
University of Iowa technical report 06-05, Aug. 2006.
Details.
“Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite”
by Sean McLaughlin, Clark Barrett, and Yeting Ge.
In Proceedings of the 3^rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR '05), (Alessandro Armando and Alessandro Cimatti, eds.), Jan. 2006, pp. 43-51. Edinburgh, Scotland.
Details.
“Validating More Loop Optimizations”
by Ying Hu, Clark Barrett, Benjamin Goldberg, and Amir Pnueli.
In Proceedings of the 4^th International Workshop on Compiler Optimization meets Compiler Verificaiton (COCV '05), (J. Knoop, G.C. Necula, and W. Zimmermann, eds.), Dec. 2005, pp. 69-84. Edinburgh, Scotland.
Details.
“Translation and Run-Time Validation of Loop Transformations”
by Lenore Zuck, Amir Pnueli, Benjamin Goldberg, Clark Barrett, Yi Fang, and Ying Hu.
Formal Methods in System Design, vol. 27, no. 3, Nov. 2005, pp. 335-360, Springer Netherlands.
Details.
“Design and Results of the 1^st Satisfiability Modulo Theories Competition (SMT-COMP 2005)”
by Clark Barrett, Leonardo de Moura, and Aaron Stump.
Journal of Automated Reasoning, vol. 35, no. 4, Nov. 2005, pp. 373-390, Springer Netherlands.
Details.
“An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types”
by Clark Barrett, Igor Shikanian, and Cesare Tinelli, Department of Computer Science.
New York University technical report TR2005-878, Nov. 2005.
Details.
“An Industrially Effective Environment for Formal Hardware Verification”
by Carl-Johan H. Seger, Robert B. Jones, John W. O'Leary, Tom Melham, Mark D. Aagaard, Clark Barrett, and Don Syme.
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 24, no. 9, Sep. 2005, pp. 1381-1405.
Details.
“TVOC: A Translation Validator for Optimizing Compilers”
by Clark Barrett, Yi Fang, Ben Goldberg, Ying Hu, Amir Pnueli, and Lenore Zuck.
In Proceedings of the 17^th International Conference on Computer Aided Verification (CAV '05), (Kousha Etessami and Sriram K. Rajamani, eds.), July 2005, pp. 291-295. Edinburgh, Scotland.
Details.
“SMT-COMP: Satisfiability Modulo Theories Competition”
by Clark Barrett, Leonardo de Moura, and Aaron Stump.
In Proceedings of the 17^th International Conference on Computer Aided Verification (CAV '05), (Kousha Etessami and Sriram K. Rajamani, eds.), July 2005, pp. 20-23. Edinburgh, Scotland.
Details.
“Combining SAT Methods with Non-Clausal Decision Heuristics”
by Clark Barrett and Jacob Donham.
In Selected Papers from the Workshops on Disproving and the Second International Workshop on Pragmatics of Decision Procedures (PDPAR '04), (Wolfgang Ahrendt, Peter Baumgartner, Hans de Nivelle, Silvio Ranise, and Cesare Tinelli, eds.), July 2005, pp. 3-12. Cork, Ireland.
Details.
“A Practical Approach to Partial Functions in CVC Lite”
by Sergey Berezin, Clark Barrett, Igor Shikanian, Marsha Chechik, Arie Gurfinkel, and David L. Dill.
In Selected Papers from the Workshops on Disproving and the Second International Workshop on Pragmatics of Decision Procedures (PDPAR '04), (Wolfgang Ahrendt, Peter Baumgartner, Hans de Nivelle, Silvio Ranise, and Cesare Tinelli, eds.), July 2005, pp. 13-23. Cork, Ireland.
Details.
“Into the Loops: Practical Issues in Translation Validation for Optimizing Compilers”
by Benjamin Goldberg, Lenore Zuck, and Clark Barrett.
In Proceedings of the 3^rd International Workshop on Compiler Optimization meets Compiler Verificaiton (COCV '04), (J. Knoop, G.C. Necula, and W. Zimmermann, eds.), May 2005, pp. 53-71. Barcelona, Spain.
Details.
“Theory and Algorithms for the Generation and Validation of Speculative Loop Optimizations”
by Ying Hu, Clark Barrett, and Benjamin Goldberg.
In Proceedings of the 2^nd IEEE International Conference on Software Engineering and Formal Methods (SEFM '04), Sep. 2004, pp. 281-289. Beijing, China.
Details.
“CVC Lite: A New Implementation of the Cooperating Validity Checker”
by Clark Barrett and Sergey Berezin.
In Proceedings of the 16^th International Conference on Computer Aided Verification (CAV '04), (Rajeev Alur and Doron A. Peled, eds.), July 2004, pp. 515-518. Boston, Massachusetts.
Details.
“Run-Time Validation of Speculative Optimizations using CVC”
by Clark Barrett, Benjamin Goldberg, and Lenore Zuck.
In Proceedings of the 3^rd International Workshop on Run-time Verification (RV '03), (Oleg Sokolsky and Mahesh Viswanathan, eds.), Oct. 2003, pp. 89-107. Boulder, Colorado.
Details.
“A Proof-Producing Boolean Search Engine”
by Clark Barrett and Sergey Berezin.
In Proceedings of the 1^st International Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR '03), July 2003. Miami, Florida.
Details.
“Checking Validity of Quantifier-Free Formulas in Combinations of First-Order Theories”
by Clark W. Barrett.
Ph.D. dissertation, Stanford University, Jan. 2003. Stanford, California.
Details.
“CVC: A Cooperating Validity Checker”
by Aaron Stump, Clark W. Barrett, and David L. Dill.
In Proceedings of the 14^th International Conference on Computer Aided Verification (CAV '02), (Ed Brinksma and Kim Guldstrand Larsen, eds.), July 2002, pp. 500-504. Copenhagen, Denmark.
Details.
“Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF”
by Aaron Stump, Clark W. Barrett, and David L. Dill.
In Proceedings of the 3^rd International Workshop on Logical Frameworks and Meta-Languages (LFM '02), (Frank Pfenning, ed.), July 2002, pp. 29-41. Copenhagen, Denmark.
Details.
“Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT”
by Clark W. Barrett, David L. Dill, and Aaron Stump.
In Proceedings of the 14^th International Conference on Computer Aided Verification (CAV '02), (Ed Brinksma and Kim Guldstrand Larsen, eds.), July 2002, pp. 236-249. Copenhagen, Denmark.
Details.
“A Generalization of Shostak's Method for Combining Decision Procedures”
by Clark W. Barrett, David L. Dill, and Aaron Stump.
In Proceedings of the 4^th International Workshop on Frontiers of Combining Systems (FroCoS '02), (Alessandro Armando, ed.), Apr. 2002, pp. 132-146. Santa Margherita Ligure, Italy.
Details.
“A Decision Procedure for an Extensional Theory of Arrays”
by Aaron Stump, Clark W. Barrett, David L. Dill, and Jeremy Levitt.
In Proceedings of the 16^th IEEE Symposium on Logic in Computer Science (LICS '01), June 2001, pp. 29-37. Boston, Massachusetts.
Details.
“A Framework for Cooperating Decision Procedures”
by Clark W. Barrett, David L. Dill, and Aaron Stump.
In Proceedings of the 17^th International Conference on Computer-Aided Deduction (CADE '00), (David McAllester, ed.), June 2000, pp. 79-97. Pittsburgh, Pennsylvania.
Details.
“A Decision Procedure for Bit-vector Arithmetic”
by Clark W. Barrett, David L. Dill, and Jeremy R. Levitt.
In Proceedings of the 35^th Design Automation Conference (DAC '98), June 1998, pp. 522-527. San Francisco, California. Best paper award..
Details.
“Validity Checking for Combinations of Theories with Equality”
by Clark W. Barrett, David L. Dill, and Jeremy R. Levitt.
In Proceedings of the 1^st International Conference on Formal Methods In Computer-Aided Design (FMCAD '96), (Mandayam Srivas and Albert Camilleri, eds.), Nov. 1996, pp. 187-201. Palo Alto, California.
Details.
“Automatic Generation of Invariants in Processor Verification”
by Jeffrey X. Su, David L. Dill, and Clark W. Barrett.
In Proceedings of the 1^st International Conference on Formal Methods In Computer-Aided Design (FMCAD '96), (Mandayam Srivas and Albert Camilleri, eds.), Nov. 1996, pp. 377-388. Palo Alto, California.
Details.
(This webpage was created with bibtex2web.)