Clark Barrett's Publications

Also see publications by category


2020

“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.
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2020, IEEE. under review.
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, 2020, Springer US. to appear.
Details.

“Counterexample Guided Inductive Synthesis Modulo Theories” by Alessandro Abate, Haniel Barbosa, Clark Barrett, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, Andrew Reynolds, and Cesare Tinelli, 2020. under review.
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.

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.

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, to appear.
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, to appear.
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.

2019

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), 2019.
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.

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.

2018

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.

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, Mathia Preiner, Clark Barrett, and Cesare Tinelli.
In Proceedings of the 26^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.
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.

2017

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.

2016

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.

2015

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.

2014

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.

2013

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.

2011

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.

2010

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.

2009

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.

2008

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.

2007

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.

2006

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.

2005

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.

2004

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.

2003

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.

2002

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.

2001

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.

2000

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.

1998

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.

1996

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.)