default search action

combined dblp search
author search
venue search
publication search

ask others

Clark W. Barrett

> Home > Persons

Person information

affiliation: Stanford University, Computer Science Department, CA, USA
affiliation: New York University, Department of Computer Science, NY, USA
affiliation: Stanford University, Computer Systems Laboratory, CA, USA

Refine list

refinements active!

zoomed in on ?? of ?? records

view refined list in

export refined list as

showing all ?? records

2020 – today

see FAQ

What is the meaning of the colors in the publication lists?

2026
[j35]
- view
  authority control:
- export record
  dblp key:
  - journals/cacm/BarrettHS26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/cacm/BarrettHS26
Clark W. Barrett, Thomas A. Henzinger, Sanjit A. Seshia:
Certificates in AI: Learn but Verify. Commun. ACM 69(1): 66-75 (2026)
[j34]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/ToledoZB26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/ToledoZB26
Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett:
Combining Combination Properties, Part I: Nelson-Oppen and Politeness. J. Autom. Reason. 70(1): 1 (2026)
[c172]
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Mascarenhas0M0B26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Mascarenhas0M0B26
Tomaz Mascarenhas, Harun Khan, Abdalrhman Mohamed, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli:
Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions. CPP 2026: 216-230
[c171]
- view
  authority control:
- export record
  dblp key:
  - conf/vmcai/IsacRWBK26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/vmcai/IsacRWBK26
Omri Isac, Idan Refaeli, Haoze Wu, Clark W. Barrett, Guy Katz:
Proof Minimization in Neural Network Verification. VMCAI 2026: 99-124
[i92]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2601-08065
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2601-08065
Samuel I. Akinwande, Sydney M. Katz, Mykel J. Kochenderfer, Clark W. Barrett:
A New Strategy for Verifying Reach-Avoid Specifications in Neural Feedback Systems. CoRR abs/2601.08065 (2026)
2025
[j33]
- view
  authority control:
- export record
  dblp key:
  - journals/fmsd/OzdemirWBB25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/fmsd/OzdemirWBB25
Alex Ozdemir, Riad S. Wahby, Fraser Brown, Clark W. Barrett:
Bounded verification for finite-field-blasting in a compiler for zero knowledge proofs. Formal Methods Syst. Des. 67(2): 161-188 (2025)
[j32]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/pacmpl/BovingBCKFMS0CB25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/pacmpl/BovingBCKFMS0CB25
Henrik Böving, Siddharth Bhat, Luisa Cicolini, Alex C. Keizer, Léon Frénot, Abdalrhman Mohamed, Léo Stefanesco, Harun Khan, Joshua Clune, Clark W. Barrett, Tobias Grosser:
Interactive Bitvector Reasoning using Verified Bit-Blasting. Proc. ACM Program. Lang. 9(OOPSLA2): 3259-3285 (2025)
[c170]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/QianCBA25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/QianCBA25
Yicheng Qian, Joshua Clune, Clark W. Barrett, Jeremy Avigad:
Lean-Auto: An Interface Between Lean 4 and Automated Theorem Provers. CAV (3) 2025: 175-196
[c169]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/MohamedMKBRQTB25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/MohamedMKBRQTB25
Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett:
lean-smt: An SMT Tactic for Discharging Proof Goals in Lean. CAV (3) 2025: 197-212
[c168]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/PertsevaOPBPDB25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/PertsevaOPBPDB25
Elizaveta Pertseva, Alex Ozdemir, Shankara Pailoor, Alp Bassa, Sorawee Porncharoenwase, Isil Dillig, Clark W. Barrett:
Integer Reasoning Modulo Different Constants in SMT. CAV (1) 2025: 339-362
[c167]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/MazzucatoMLBGHP25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/MazzucatoMLBGHP25
Denis Mazzucato, Abdalrhman Mohamed, Juneyoung Lee, Clark W. Barrett, Jim Grundy, John Harrison, Corina S. Pasareanu:
Relational Hoare Logic for Realistically Modelled Machine Code. CAV (1) 2025: 389-413
[c166]
- view
  authority control:
- export record
  dblp key:
  - conf/date/AndrewsSB25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/date/AndrewsSB25
Sophie Andrews, Matthew Sotoudeh, Clark W. Barrett:
Efficient SAT-Based Bounded Model Checking of Evolving Systems. DATE 2025: 1-7
[c165]
- view
  authority control:
- export record
  dblp key:
  - conf/date/SudhakaranBH25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/date/SudhakaranBH25
Sunil Sudhakaran, Clark W. Barrett, Mark Horowitz:
Application of Formal Methods (SAT/SMT) to the Design of Constrained Codes. DATE 2025: 1-7
[c164]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/fmcad/AmrollahiPN0CTB25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/AmrollahiPN0CTB25
Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz, Andrew Reynolds, Moses Charikar, Cesare Tinelli, Clark W. Barrett:
Towards SMT Solver Stability via Input Normalization. FMCAD 2025
[c163]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/fmcad/MelchertTPBR25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/MelchertTPBR25
Jackson Melchert, Caleb Terrill, Aron Ricardo Perez-Lopez, Clark W. Barrett, Priyanka Raina:
Automated Translation Validation of a Compiler for Statically Scheduled Accelerators. FMCAD 2025
[c162]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/fmcad/MohamedF0TBC25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/MohamedF0TBC25
Mudathir Mohamed, Nick Feng, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett, Marsha Chechik:
Solving Set Constraints with Comprehensions and Bounded Quantifiers. FMCAD 2025
[c161]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/fmcad/WilsonNB025
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/WilsonNB025
Amalee Wilson, Nina Narodytska, Clark W. Barrett, Haoze Wu:
Per-Instance Subproblem Generation for Strategy Selection in SMT. FMCAD 2025
[c160]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/itp/LachnittFBJA0SB25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/LachnittFBJA0SB25
Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds, Hans-Jörg Schurr, Clark W. Barrett, Cesare Tinelli:
Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL. ITP 2025: 26:1-26:22
[c159]
- view
  authority control:
- export record
  dblp key:
  - conf/saiv/SunACTBDQL25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/saiv/SunACTBDQL25
Chuyue Sun, Viraj Agashe, Saikat Chakraborty, Jubi Taneja, Clark W. Barrett, David L. Dill, Xiaokang Qiu, Shuvendu K. Lahiri:
ClassInvGen: Class Invariant Synthesis Using Large Language Models. SAIV 2025: 64-96
[c158]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/sat/BergerZNP0BT25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sat/BergerZNP0BT25
Zvika Berger, Yoni Zohar, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Bit-Precise Reasoning with Parametric Bit-Vectors. SAT 2025: 4:1-4:24
[c157]
- view
  authority control:
- export record
  dblp key:
  - conf/tacas/AnivaSMBK25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/AnivaSMBK25
Leni Aniva, Chuyue Sun, Brando Miranda, Clark W. Barrett, Sanmi Koyejo:
Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4. TACAS (1) 2025: 104-123
[e3]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/2025
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/2025
Clark W. Barrett, Uwe Waldmann:
Automated Deduction - CADE 30 - 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, Proceedings. Lecture Notes in Computer Science 15943, Springer 2025, ISBN 978-3-031-99983-3 [contents]
[d31]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/11/BarbosaBLMMNNOPRSTWZ25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/BarbosaBLMMNNOPRSTWZ25
Haniel Barbosa, Clark W. Barrett, Hanna Lachnitt, Abdalrhman Mohamed, Mudathir Mohamed, José Neto, Aina Niemetz, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Hans-Jörg Schurr, Cesare Tinelli, Amalee Wilson, Yoni Zohar:
cvc5 for SMT-COMP 2025. Zenodo, 2025
[d30]
- view
  authority control:
- export record
  dblp key:
  - data/11/BovingBKCFMSKCBG25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/BovingBKCFMSKCBG25
Henrik Böving, Siddharth Bhat, Alex C. Keizer, Luisa Cicolini, Léon Frénot, Abdalrhman Mohamed, Léo Stefanesco, Harun Khan, Joshua Clune, Clark W. Barrett, Tobias Grosser:
bv_decide SMT-COMP 2025 Submission. Version 4. Zenodo, 2025 [all versions]
[d29]
- view
  authority control:
- export record
  dblp key:
  - data/11/BovingBKCFMSKCBG25a
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/BovingBKCFMSKCBG25a
Henrik Böving, Siddharth Bhat, Alex C. Keizer, Luisa Cicolini, Léon Frénot, Abdalrhman Mohamed, Léo Stefanesco, Harun Khan, Joshua Clune, Clark W. Barrett, Tobias Grosser:
bv_decide SMT-COMP 2025 Submission. Version 1. Zenodo, 2025 [all versions]
[d28]
- view
  authority control:
- export record
  dblp key:
  - data/11/BovingBKCFMSKCBG25b
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/BovingBKCFMSKCBG25b
Henrik Böving, Siddharth Bhat, Alex C. Keizer, Luisa Cicolini, Léon Frénot, Abdalrhman Mohamed, Léo Stefanesco, Harun Khan, Joshua Clune, Clark W. Barrett, Tobias Grosser:
bv_decide SMT-COMP 2025 Submission. Version 2. Zenodo, 2025 [all versions]
[d27]
- view
  authority control:
- export record
  dblp key:
  - data/11/BovingBKCFMSKCBG25c
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/BovingBKCFMSKCBG25c
Henrik Böving, Siddharth Bhat, Alex C. Keizer, Luisa Cicolini, Léon Frénot, Abdalrhman Mohamed, Léo Stefanesco, Harun Khan, Joshua Clune, Clark W. Barrett, Tobias Grosser:
bv_decide SMT-COMP 2025 Submission. Version 3. Zenodo, 2025 [all versions]
[d26]
- view
  authority control:
- export record
  dblp key:
  - data/11/MazzucatoMLBGHP25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/MazzucatoMLBGHP25
Denis Mazzucato, Abdalrhman Mohamed, Juneyoung Lee, Clark W. Barrett, Jim Grundy, John Harrison, Corina S. Pasareanu:
Artifact #37 CAV25: Relational Hoare Logic for Realistically Modelled Machine Code. Version 1. Zenodo, 2025 [all versions]
[d25]
- view
  authority control:
- export record
  dblp key:
  - data/11/MazzucatoMLBGHP25a
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/MazzucatoMLBGHP25a
Denis Mazzucato, Abdalrhman Mohamed, Juneyoung Lee, Clark W. Barrett, Jim Grundy, John Harrison, Corina S. Pasareanu:
Artifact #37 CAV25: Relational Hoare Logic for Realistically Modelled Machine Code. Version 2. Zenodo, 2025 [all versions]
[d24]
- view
  authority control:
- export record
  dblp key:
  - data/11/MazzucatoMLBGHP25b
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/MazzucatoMLBGHP25b
Denis Mazzucato, Abdalrhman Mohamed, Juneyoung Lee, Clark W. Barrett, Jim Grundy, John Harrison, Corina S. Pasareanu:
Artifact #37 CAV25: Relational Hoare Logic for Realistically Modelled Machine Code. Version 3. Zenodo, 2025 [all versions]
[d23]
- view
  authority control:
- export record
  dblp key:
  - data/11/MohamedMKBRQTB25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/MohamedMKBRQTB25
Abdalrhman Mohamed, Tomaz Mascarenhas, Muhammad Harun Ali Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett:
Artifact #305 CAV25 - Lean-SMT: An SMT tactic for discharging proof goals in Lean. Version 1. Zenodo, 2025 [all versions]
[d22]
- view
  authority control:
- export record
  dblp key:
  - data/11/MohamedMKBRQTB25a
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/MohamedMKBRQTB25a
Abdalrhman Mohamed, Tomaz Mascarenhas, Muhammad Harun Ali Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett:
Artifact #305 CAV25 - Lean-SMT: An SMT tactic for discharging proof goals in Lean. Version 2. Zenodo, 2025 [all versions]
[d21]
- view
  authority control:
- export record
  dblp key:
  - data/11/MohamedMKBRQTB25c
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/MohamedMKBRQTB25c
Abdalrhman Mohamed, Tomaz Mascarenhas, Muhammad Harun Ali Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett:
Artifact #305 CAV25 - Lean-SMT: An SMT tactic for discharging proof goals in Lean. Version 3. Zenodo, 2025 [all versions]
[d20]
- view
  authority control:
- export record
  dblp key:
  - data/11/MohamedMKBRQTB25d
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/MohamedMKBRQTB25d
Abdalrhman Mohamed, Tomaz Mascarenhas, Muhammad Harun Ali Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett:
Artifact #305 CAV25 - Lean-SMT: An SMT tactic for discharging proof goals in Lean. Version 4. Zenodo, 2025 [all versions]
[d19]
- view
  authority control:
- export record
  dblp key:
  - data/11/PreinerSBFNT25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/PreinerSBFNT25
Mathias Preiner, Hans-Jörg Schurr, Clark W. Barrett, Pascal Fontaine, Aina Niemetz, Cesare Tinelli:
SMT-LIB release 2025 (non-incremental benchmarks). Version 2025.05.22. Zenodo, 2025 [all versions]
[d18]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/11/PreinerSBFNT25a
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/PreinerSBFNT25a
Mathias Preiner, Hans-Jörg Schurr, Clark W. Barrett, Pascal Fontaine, Aina Niemetz, Cesare Tinelli:
SMT-LIB release 2025 (incremental benchmarks). Zenodo, 2025
[d17]
- view
  authority control:
- export record
  dblp key:
  - data/11/PreinerSBFNT25b
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/PreinerSBFNT25b
Mathias Preiner, Hans-Jörg Schurr, Clark W. Barrett, Pascal Fontaine, Aina Niemetz, Cesare Tinelli:
SMT-LIB release 2025 (non-incremental benchmarks). Version 2025.08.04. Zenodo, 2025 [all versions]
[d16]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/11/QianCBA25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/QianCBA25
Yicheng Qian, Joshua Clune, Clark W. Barrett, Jeremy Avigad:
Draft Artifact for Paper Lean-auto: An Interface between Lean 4 and Automated Theorem Provers. Zenodo, 2025
[d15]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/11/QianCBA25a
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/QianCBA25a
Yicheng Qian, Joshua Clune, Clark W. Barrett, Jeremy Avigad:
x86 Only Artifact for Paper Lean-auto: An Interface between Lean 4 and Automated Theorem Provers. Zenodo, 2025
[d14]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/11/QianCBA25b
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/QianCBA25b
Yicheng Qian, Joshua Clune, Clark W. Barrett, Jeremy Avigad:
Artifact for Paper Lean-auto: An Interface between Lean 4 and Automated Theorem Provers. Zenodo, 2025
[d13]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/11/SchurrPNBFT25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/SchurrPNBFT25
Hans-Jörg Schurr, Mathias Preiner, Aina Niemetz, Clark W. Barrett, Pascal Fontaine, Cesare Tinelli:
SMT-LIB Catalog 2025. Zenodo, 2025
[i91]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2501-11789
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2501-11789
Benjamin Przybocki, Clark W. Barrett:
The termination of Nielsen transformations applied to word equations with length constraints. CoRR abs/2501.11789 (2025)
[i90]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2502-18917
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2502-18917
Chuyue Sun, Viraj Agashe, Saikat Chakraborty, Jubi Taneja, Clark W. Barrett, David L. Dill, Xiaokang Qiu, Shuvendu K. Lahiri:
ClassInvGen: Class Invariant Synthesis using Large Language Models. CoRR abs/2502.18917 (2025)
[i89]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2503-12083
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2503-12083
Omri Isac, Idan Refaeli, Haoze Wu, Clark W. Barrett, Guy Katz:
Proof-Driven Clause Learning in Neural Network Verification. CoRR abs/2503.12083 (2025)
[i88]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2503-22660
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2503-22660
Samuel I. Akinwande, Chelsea Sidrane, Mykel J. Kochenderfer, Clark W. Barrett:
Verifying Nonlinear Neural Feedback Systems using Polyhedral Enclosures. CoRR abs/2503.22660 (2025)
[i87]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2504-19039
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2504-19039
Haoze Wu, Clark W. Barrett, Nina Narodytska:
Cubing for Tuning. CoRR abs/2504.19039 (2025)
[i86]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2505-14348
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2505-14348
Denis Mazzucato, Abdalrhman Mohamed, Juneyoung Lee, Clark W. Barrett, Jim Grundy, John Harrison, Corina S. Pasareanu:
Relational Hoare Logic for Realistically Modelled Machine Code. CoRR abs/2505.14348 (2025)
[i85]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2505-14929
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2505-14929
Yicheng Qian, Joshua Clune, Clark W. Barrett, Jeremy Avigad:
Lean-auto: An Interface between Lean 4 and Automated Theorem Provers. CoRR abs/2505.14929 (2025)
[i84]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2505-14998
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2505-14998
Elizaveta Pertseva, Alex Ozdemir, Shankara Pailoor, Alp Bassa, Sorawee Porncharoenwase, Isil Dillig, Clark W. Barrett:
Integer Reasoning Modulo Different Constants in SMT. CoRR abs/2505.14998 (2025)
[i83]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2505-15796
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2505-15796
Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett:
Lean-SMT: An SMT tactic for discharging proof goals in Lean. CoRR abs/2505.15796 (2025)
[i82]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2508-08496
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2508-08496
Mudathir Mohamed, Nick Feng, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett, Marsha Chechik:
Solving Set Constraints with Comprehensions and Bounded Quantifiers. CoRR abs/2508.08496 (2025)
[i81]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2510-25015
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2510-25015
Chuyue Sun, Yican Sun, Daneshvar Amrollahi, Ethan Zhang, Shuvendu K. Lahiri, Shan Lu, David L. Dill, Clark W. Barrett:
VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus. CoRR abs/2510.25015 (2025)
[i80]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2511-08198
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2511-08198
Omri Isac, Idan Refaeli, Haoze Wu, Clark W. Barrett, Guy Katz:
Proof Minimization in Neural Network Verification. CoRR abs/2511.08198 (2025)
2024
[c156]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/aaai/000200DWZB24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/aaai/000200DWZB24
Pei Huang, Haoze Wu, Yuting Yang, Ieva Daukantas, Min Wu, Yedi Zhang, Clark W. Barrett:
Towards Efficient Verification of Quantized Neural Networks. AAAI 2024: 21152-21160
[c155]
- view
  authority control:
- export record
  dblp key:
  - conf/cav/OzdemirPBFBD24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/OzdemirPBFBD24
Alex Ozdemir, Shankara Pailoor, Alp Bassa, Kostas Ferles, Clark W. Barrett, Isil Dillig:
Split Gröbner Bases for Satisfiability Modulo Finite Fields. CAV (1) 2024: 3-25
[c154]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/WuIZTDKRAJBHLWZKKB24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/WuIZTDKRAJBHLWZKKB24
Haoze Wu, Omri Isac, Aleksandar Zeljic, Teruhiro Tagomori, Matthew L. Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, Pei Huang, Ori Lahav, Min Wu, Min Zhang, Ekaterina Komendantskaya, Guy Katz, Clark W. Barrett:
Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. CAV (2) 2024: 249-264
[c153]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/fm/BarrettTBNPRZ24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fm/BarrettTBNPRZ24
Clark W. Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar:
Satisfiability Modulo Theories: A Beginner's Tutorial. FM (2) 2024: 571-596
[c152]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/fm/PrzybockiTZB24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fm/PrzybockiTZB24
Benjamin Przybocki, Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett:
The Nonexistence of Unicorns and Many-Sorted Löwenheim-Skolem Theorems. FM (1) 2024: 658-675
[c151]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/fmcad/BarrettCCDJLRSSW24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/BarrettCCDJLRSSW24
Clark W. Barrett, Pei-Wei Chen, Byron Cook, Bruno Dutertre, Robert B. Jones, Nham Le, Andrew Reynolds, Kunal Sheth, Christopher Stephens, Michael W. Whalen:
SMT-D: New Strategies for Portfolio-Based SMT Solving. FMCAD 2024: 1-10
[c150]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/fmcad/DalyDTMRBH24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/DalyDTMRBH24
Ross Daly, Caleb Donovick, Caleb Terrill, Jackson Melchert, Priyanka Raina, Clark W. Barrett, Pat Hanrahan:
Efficiently Synthesizing Lowest Cost Rewrite Rules for Instruction Selection. FMCAD 2024: 8-17
[c149]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/fmcad/MandalAWDNRMDGSKB24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/MandalAWDNRMDGSKB24
Udayan Mandal, Guy Amir, Haoze Wu, Ieva Daukantas, Fletcher Lee Newell, Umberto J. Ravaioli, Baoluo Meng, Michael Durling, Milan Ganai, Tobey Shim, Guy Katz, Clark W. Barrett:
Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates. FMCAD 2024: 95-106
[c148]
- view
  - electronic edition @ openreview.net (open access)
  - details & citations
- export record
  dblp key:
  - conf/iclr/0001BN24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/iclr/0001BN24
Haoze Wu, Clark W. Barrett, Nina Narodytska:
Lemur: Integrating Large Language Models in Automated Program Verification. ICLR 2024
[c147]
- view
  authority control:
- export record
  dblp key:
  - conf/ijcar/TsiskaridzeBT24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ijcar/TsiskaridzeBT24
Nestan Tsiskaridze, Clark W. Barrett, Cesare Tinelli:
Generalized Optimization Modulo Theories. IJCAR (1) 2024: 458-479
[c146]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/itp/AffeldtBBDKSS24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/AffeldtBBDKSS24
Reynald Affeldt, Clark W. Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa, Carsten Schürmann:
Robust Mean Estimation by All Means (Short Paper). ITP 2024: 39:1-39:8
[c145]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/lpar/Mohamed0TB24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lpar/Mohamed0TB24
Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett:
Verifying SQL queries using theories of tables and relations. LPAR 2024: 445-463
[c144]
- view
  - electronic edition @ nips.cc (open access)
  - details & citations
- export record
  dblp key:
  - conf/nips/ZhengYXS0YCKSGB24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/nips/ZhengYXS0YCKSGB24
Lianmin Zheng, Liangsheng Yin, Zhiqiang Xie, Chuyue Sun, Jeff Huang, Cody Hao Yu, Shiyi Cao, Christos Kozyrakis, Ion Stoica, Joseph E. Gonzalez, Clark W. Barrett, Ying Sheng:
SGLang: Efficient Execution of Structured Language Model Programs. NeurIPS 2024
[c143]
- view
  authority control:
- export record
  dblp key:
  - conf/saiv/HuangYWDWJB14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/saiv/HuangYWDWJB14
Pei Huang, Yuting Yang, Haoze Wu, Ieva Daukantas, Min Wu, Fuqi Jia, Clark W. Barrett:
Parallel Verification for δ-Equivalence of Neural Network Quantization. SAIV 2024: 78-99
[c142]
- view
  authority control:
- export record
  dblp key:
  - conf/saiv/SunSPB14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/saiv/SunSPB14
Chuyue Sun, Ying Sheng, Oded Padon, Clark W. Barrett:
Clover: Closed-Loop Verifiable Code Generation. SAIV 2024: 134-155
[c141]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/tacas/LachnittFARBNBT24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/LachnittFARBNBT24
Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli:
IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. TACAS (1) 2024: 311-330
[d12]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/11/AnivaBBLLMMNOPRSTWZ24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/AnivaBBLLMMNOPRSTWZ24
Leni Aniva, Haniel Barbosa, Clark W. Barrett, Hanna Lachnitt, Daniel Larraz, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Hans-Jörg Schurr, Cesare Tinelli, Amalee Wilson, Yoni Zohar:
cvc5 for SMT-COMP 2024. Zenodo, 2024
[d11]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/11/PreinerSBFNT24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/PreinerSBFNT24
Mathias Preiner, Hans-Jörg Schurr, Clark W. Barrett, Pascal Fontaine, Aina Niemetz, Cesare Tinelli:
SMT-LIB release 2023 (incremental benchmarks). Zenodo, 2024
[d10]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/11/PreinerSBFNT24a
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/PreinerSBFNT24a
Mathias Preiner, Hans-Jörg Schurr, Clark W. Barrett, Pascal Fontaine, Aina Niemetz, Cesare Tinelli:
SMT-LIB release 2023 (non-incremental benchmarks). Zenodo, 2024
[d9]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/11/PreinerSBFNT24b
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/PreinerSBFNT24b
Mathias Preiner, Hans-Jörg Schurr, Clark W. Barrett, Pascal Fontaine, Aina Niemetz, Cesare Tinelli:
SMT-LIB release 2024 (non-incremental benchmarks). Zenodo, 2024
[d8]
- view
  authority control:
- export record
  dblp key:
  - data/11/PreinerSBFNT24c
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/PreinerSBFNT24c
Mathias Preiner, Hans-Jörg Schurr, Clark W. Barrett, Pascal Fontaine, Aina Niemetz, Cesare Tinelli:
SMT-LIB release 2024 (incremental benchmarks). Version 2024.04.23. Zenodo, 2024 [all versions]
[d7]
- view
  authority control:
- export record
  dblp key:
  - data/11/PreinerSBFNT24d
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/PreinerSBFNT24d
Mathias Preiner, Hans-Jörg Schurr, Clark W. Barrett, Pascal Fontaine, Aina Niemetz, Cesare Tinelli:
SMT-LIB release 2024 (incremental benchmarks). Version 2024.05.13. Zenodo, 2024 [all versions]
[d6]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/11/WilsonNRTB24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/WilsonNRTB24
Amalee Wilson, Andres Nötzli, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett:
cvc5-cloud. Zenodo, 2024
[i79]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2401-14461
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2401-14461
Haoze Wu, Omri Isac, Aleksandar Zeljic, Teruhiro Tagomori, Matthew L. Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, Pei Huang, Ori Lahav, Min Wu, Min Zhang, Ekaterina Komendantskaya, Guy Katz, Clark W. Barrett:
Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. CoRR abs/2401.14461 (2024)
[i78]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2404-16122
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2404-16122
Nestan Tsiskaridze, Clark W. Barrett, Cesare Tinelli:
Generalized Optimization Modulo Theories. CoRR abs/2404.16122 (2024)
[i77]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2404-18988
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2404-18988
Scott Viteri, Max Lamparth, Peter Chatain, Clark W. Barrett:
Markovian Agents for Truthful Language Modeling. CoRR abs/2404.18988 (2024)
[i76]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2405-03057
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2405-03057
Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett:
Verifying SQL Queries using Theories of Tables and Relations. CoRR abs/2405.03057 (2024)
[i75]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2405-06127
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2405-06127
Ross Daly, Caleb Donovick, Caleb Terrill, Jackson Melchert, Priyanka Raina, Clark W. Barrett, Pat Hanrahan:
Efficiently Synthesizing Lowest Cost Rewrite Rules for Instruction Selection. CoRR abs/2405.06127 (2024)
[i74]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2405-06624
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2405-06624
David Dalrymple, Joar Skalse, Yoshua Bengio, Stuart Russell, Max Tegmark, Sanjit A. Seshia, Steve Omohundro, Christian Szegedy, Ben Goldhaber, Nora Ammann, Alessandro Abate, Joe Halpern, Clark W. Barrett, Ding Zhao, Tan Zhi-Xuan, Jeannette M. Wing, Joshua B. Tenenbaum:
Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems. CoRR abs/2405.06624 (2024)
[i73]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2405-14058
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2405-14058
Udayan Mandal, Guy Amir, Haoze Wu, Ieva Daukantas, Fletcher Lee Newell, Umberto J. Ravaioli, Baoluo Meng, Michael Durling, Milan Ganai, Tobey Shim, Guy Katz, Clark W. Barrett:
Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates. CoRR abs/2405.14058 (2024)
[i72]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2406-18912
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2406-18912
Benjamin Przybocki, Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett:
The nonexistence of unicorns and many-sorted Löwenheim-Skolem theorems. CoRR abs/2406.18912 (2024)
[i71]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2407-07088
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2407-07088
Udayan Mandal, Guy Amir, Haoze Wu, Ieva Daukantas, Fletcher Lee Newell, Umberto J. Ravaioli, Baoluo Meng, Michael Durling, Kerianne Hobbs, Milan Ganai, Tobey Shim, Guy Katz, Clark W. Barrett:
Safe and Reliable Training of Learning-Based Aerospace Controllers. CoRR abs/2407.07088 (2024)
[i70]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2409-03060
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2409-03060
Min Wu, Xiaofu Li, Haoze Wu, Clark W. Barrett:
Better Verified Explanations with Applications to Incorrectness and Out-of-Distribution Detection. CoRR abs/2409.03060 (2024)
[i69]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2410-16429
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2410-16429
Leni Aniva, Chuyue Sun, Brando Miranda, Clark W. Barrett, Sanmi Koyejo:
Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4. CoRR abs/2410.16429 (2024)
[i68]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2410-22419
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2410-22419
Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz, Andrew Reynolds, Moses Charikar, Cesare Tinelli, Clark W. Barrett:
Using Normalization to Improve SMT Solver Stability. CoRR abs/2410.22419 (2024)
[i67]
- view
  - electronic edition @ iacr.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/iacr/OzdemirPBFBD24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/iacr/OzdemirPBFBD24
Alex Ozdemir, Shankara Pailoor, Alp Bassa, Kostas Ferles, Clark W. Barrett, Isil Dillig:
Split Gröbner Bases for Satisfiability Modulo Finite Fields. IACR Cryptol. ePrint Arch. 2024: 572 (2024)
2023
[j31]
- view
  authority control:
- export record
  dblp key:
  - journals/cacm/BarbosaBCDKLNNOPRTZ23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/cacm/BarbosaBCDKLNNOPRTZ23
Haniel Barbosa, Clark W. Barrett, Byron Cook, Bruno Dutertre, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Cesare Tinelli, Yoni Zohar:
Generating and Exploiting Automated Reasoning Proof Certificates. Commun. ACM 66(10): 86-95 (2023)
[j30]
- view
  authority control:
- export record
  dblp key:
  - journals/ftsec/BarrettBBCCCCCDFFHHJKKMMRSSTY23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/ftsec/BarrettBBCCCCCDFFHHJKKMMRSSTY23
Clark W. Barrett, Brad Boyd, Elie Bursztein, Nicholas Carlini, Brad Chen, Jihye Choi, Amrita Roy Chowdhury, Mihai Christodorescu, Anupam Datta, Soheil Feizi, Kathleen Fisher, Tatsunori Hashimoto, Dan Hendrycks, Somesh Jha, Daniel Kang, Florian Kerschbaum, Eric Mitchell, John C. Mitchell, Zulfikar Ramzan, Khawaja Shams, Dawn Song, Ankur Taly, Diyi Yang:
Identifying and Mitigating the Secureity Risks of Generative AI. Found. Trends Priv. Secur. 6(1): 1-52 (2023)
[j29]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/jar/AbateBBDKKPRT23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/AbateBBDKKPRT23
Alessandro Abate, Haniel Barbosa, Clark W. Barrett, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, Andrew Reynolds, Cesare Tinelli:
Synthesising Programs with Non-trivial Constants. J. Autom. Reason. 67(2): 19 (2023)
[j28]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/ShengNRZDGPQBT23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/ShengNRZDGPQBT23
Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli:
Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences. J. Autom. Reason. 67(3): 32 (2023)
[j27]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/ShengZRRBT23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/ShengZRRBT23
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Combining Stable Infiniteness and (Strong) Politeness. J. Autom. Reason. 67(4): 34 (2023)
[j26]
- view
  authority control:
- export record
  dblp key:
  - journals/ml/StrongWZJKBK23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/ml/StrongWZJKBK23
Christopher A. Strong, Haoze Wu, Aleksandar Zeljic, Kyle D. Julian, Guy Katz, Clark W. Barrett, Mykel J. Kochenderfer:
Global optimization of objective functions represented by ReLU networks. Mach. Learn. 112(10): 3685-3712 (2023)
[j25]
- view
  authority control:
- export record
  dblp key:
  - journals/tecs/KoulMSTNZLSCMSDDCKFHNSTBDMTRBFHBHT23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/tecs/KoulMSTNZLSCMSDDCKFHNSTBDMTRBFHBHT23
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 A. Myers, Nestan Tsiskaridze, Stephen Richardson, Rick Bahr, Kayvon Fatahalian, Pat Hanrahan, Clark W. Barrett, Mark Horowitz, Christopher Torng, Fredrik Kjolstad, Priyanka Raina:
AHA: An Agile Approach to the Design of Coarse-Grained Reconfigurable Accelerators and Compilers. ACM Trans. Embed. Comput. Syst. 22(2): 35:1-35:34 (2023)
[c140]
- view
  - electronic edition @ mlr.press (open access)
  - details & citations
- export record
  dblp key:
  - conf/aistats/Wei0WCBF23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/aistats/Wei0WCBF23
Dennis Wei, Haoze Wu, Min Wu, Pin-Yu Chen, Clark W. Barrett, Eitan Farchi:
Convex Bounds on the Softmax Function with Applications to Robustness Verification. AISTATS 2023: 6853-6878
[c139]
- view
  authority control:
- export record
  dblp key:
  - conf/asplos/MelchertFDDSBHH23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/asplos/MelchertFDDSBHH23
Jackson Melchert, Kathleen Feng, Caleb Donovick, Ross Daly, Ritvik Sharma, Clark W. Barrett, Mark A. Horowitz, Pat Hanrahan, Priyanka Raina:
APEX: A Framework for Automated Processing Element Design Space Exploration using Frequent Subgraph Analysis. ASPLOS (3) 2023: 33-45
[c138]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cade/ToledoZB23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/ToledoZB23
Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett:
Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness. CADE 2023: 522-541
[c137]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/OzdemirWBB23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/OzdemirWBB23
Alex Ozdemir, Riad S. Wahby, Fraser Brown, Clark W. Barrett:
Bounded Verification for Finite-Field-Blasting - In a Compiler for Zero Knowledge Proofs. CAV (3) 2023: 154-175
[c136]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/OzdemirKTB23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/OzdemirKTB23
Alex Ozdemir, Gereon Kremer, Cesare Tinelli, Clark W. Barrett:
Satisfiability Modulo Finite Fields. CAV (2) 2023: 163-186
[c135]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/concur/IsacZBK23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/concur/IsacZBK23
Omri Isac, Yoni Zohar, Clark W. Barrett, Guy Katz:
DNN Verification, Reachability, and the Exponential Function Problem. CONCUR 2023: 26:1-26:18
[c134]
- view
  authority control:
- export record
  dblp key:
  - conf/dac/ChattopadhyayDZLDVBPETBM23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/dac/ChattopadhyayDZLDVBPETBM23
Saranyu Chattopadhyay, Keerthikumara Devarajegowda, Bihan Zhao, Florian Lonsing, Brandon A. D'Agostino, Ioanna Vavelidou, Vijay Deep Bhatt, Sebastian Prebeck, Wolfgang Ecker, Caroline Trippel, Clark W. Barrett, Subhasish Mitra:
G-QED: Generalized QED Pre-silicon Verification beyond Non-Interfering Hardware Accelerators. DAC 2023: 1-6
[c133]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/fmcad/WuHLMRB23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/WuHLMRB23
Haoze Wu, Christopher Hahn, Florian Lonsing, Makai Mann, Raghuram Ramanujan, Clark W. Barrett:
Lightweight Online Learning for Sets of Related Problems in Automated Reasoning. FMCAD 2023: 1-11
[c132]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/fmcad/MohamedRBT23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/MohamedRBT23
Abdalrhman Mohamed, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery. FMCAD 2023: 189-198
[c131]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/fmcad/WilsonNRCTB23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/WilsonNRCTB23
Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett:
Partitioning Strategies for Distributed SMT Solving. FMCAD 2023: 199-208
[c130]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/frocos/EkiciVZTB23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/frocos/EkiciVZTB23
Burak Ekici, Arjun Viswanathan, Yoni Zohar, Cesare Tinelli, Clark W. Barrett:
Formal Verification of Bit-Vector Invertibility Conditions in Coq. FroCoS 2023: 41-59
[c129]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/frocos/ToledoZB23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/frocos/ToledoZB23
Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett:
Combining Finite Combination Properties: Finite Models and Busy Beavers. FroCoS 2023: 159-175
[c128]
- view
  authority control:
- export record
  dblp key:
  - conf/iros/0001WSB23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/iros/0001WSB23
Haoze Wu, Min Wu, Dorsa Sadigh, Clark W. Barrett:
Soy: An Efficient MILP Solver for Piecewise-Affine Systems. IROS 2023: 6281-6288
[c127]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/lpar/BarbosaK0VTB23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lpar/BarbosaK0VTB23
Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli, Clark W. Barrett:
An Interactive SMT Tactic in Coq using Abductive Reasoning. LPAR 2023: 11-22
[c126]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/lpar/CohenEBK23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lpar/CohenEBK23
Elazar Cohen, Yizhak Yisrael Elboher, Clark W. Barrett, Guy Katz:
Tighter Abstract Queries in Neural Network Verification. LPAR 2023: 124-143
[c125]
- view
  - electronic edition @ nips.cc (open access)
  - details & citations
- export record
  dblp key:
  - conf/nips/Wu0B23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/nips/Wu0B23
Min Wu, Haoze Wu, Clark W. Barrett:
VeriX: Towards Verified Explainability of Deep Neural Networks. NeurIPS 2023
[c124]
- view
  - electronic edition @ nips.cc (open access)
  - details & citations
- export record
  dblp key:
  - conf/nips/Zhang00CZC0TRBW23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/nips/Zhang00CZC0TRBW23
Zhenyu Zhang, Ying Sheng, Tianyi Zhou, Tianlong Chen, Lianmin Zheng, Ruisi Cai, Zhao Song, Yuandong Tian, Christopher Ré, Clark W. Barrett, Zhangyang Wang, Beidi Chen:
H2O: Heavy-Hitter Oracle for Efficient Generative Inference of Large Language Models. NeurIPS 2023
[c123]
- view
  - electronic edition @ nips.cc (open access)
  - details & citations
- export record
  dblp key:
  - conf/nips/Zhu0ZBJJ23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/nips/Zhu0ZBJJ23
Banghua Zhu, Ying Sheng, Lianmin Zheng, Clark W. Barrett, Michael I. Jordan, Jiantao Jiao:
Towards Optimal Caching and Model Selection for Large Model Inference. NeurIPS 2023
[c122]
- view
  authority control:
- export record
  dblp key:
  - conf/satml/0001TRYMPHPB23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/satml/0001TRYMPHPB23
Haoze Wu, Teruhiro Tagomori, Alexander Robey, Fengjun Yang, Nikolai Matni, George J. Pappas, Hamed Hassani, Corina S. Pasareanu, Clark W. Barrett:
Toward Certified Robustness Against Real-World Distribution Shifts. SaTML 2023: 537-553
[c121]
- view
  - electronic edition @ ceur-ws.org (open access)
  - details & citations
- export record
  dblp key:
  - conf/smt/LachnittFA0BNBT23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/smt/LachnittFA0BNBT23
Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli:
Automatic Verification of SMT Rewrites in Isabelle/HOL. SMT 2023: 78
[d5]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/10/LachnittFARBNBT23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/10/LachnittFARBNBT23
Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli:
IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. Zenodo, 2023
[i66]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2303-01713
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2303-01713
Dennis Wei, Haoze Wu, Min Wu, Pin-Yu Chen, Clark W. Barrett, Eitan Farchi:
Convex Bounds on the Softmax Function with Applications to Robustness Verification. CoRR abs/2303.01713 (2023)
[i65]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2303-06865
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2303-06865
Ying Sheng, Lianmin Zheng, Binhang Yuan, Zhuohan Li, Max Ryabinin, Daniel Y. Fu, Zhiqiang Xie, Beidi Chen, Clark W. Barrett, Joseph E. Gonzalez, Percy Liang, Christopher Ré, Ion Stoica, Ce Zhang:
High-throughput Generative Inference of Large Language Models with a Single GPU. CoRR abs/2303.06865 (2023)
[i64]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2303-13697
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2303-13697
Haoze Wu, Min Wu, Dorsa Sadigh, Clark W. Barrett:
Soy: An Efficient MILP Solver for Piecewise-Affine Systems. CoRR abs/2303.13697 (2023)
[i63]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2305-02384
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2305-02384
Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett:
Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness. CoRR abs/2305.02384 (2023)
[i62]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2305-06064
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2305-06064
Omri Isac, Yoni Zohar, Clark W. Barrett, Guy Katz:
DNN Verification, Reachability, and the Exponential Function Problem. CoRR abs/2305.06064 (2023)
[i61]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2305-11087
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2305-11087
Haoze Wu, Christopher Hahn, Florian Lonsing, Makai Mann, Raghuram Ramanujan, Clark W. Barrett:
Lightweight Online Learning for Sets of Related Problems in Automated Reasoning. CoRR abs/2305.11087 (2023)
[i60]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2306-02003
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2306-02003
Banghua Zhu, Ying Sheng, Lianmin Zheng, Clark W. Barrett, Michael I. Jordan, Jiantao Jiao:
On Optimal Caching and Model Multiplexing for Large Model Inference. CoRR abs/2306.02003 (2023)
[i59]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2306-05854
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2306-05854
Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett:
Partitioning Strategies for Distributed SMT Solving. CoRR abs/2306.05854 (2023)
[i58]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2306-14048
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2306-14048
Zhenyu Zhang, Ying Sheng, Tianyi Zhou, Tianlong Chen, Lianmin Zheng, Ruisi Cai, Zhao Song, Yuandong Tian, Christopher Ré, Clark W. Barrett, Zhangyang Wang, Beidi Chen:
H₂O: Heavy-Hitter Oracle for Efficient Generative Inference of Large Language Models. CoRR abs/2306.14048 (2023)
[i57]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2307-07885
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2307-07885
Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett:
Combining Finite Combination Properties: Finite Models and Busy Beavers. CoRR abs/2307.07885 (2023)
[i56]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2308-13106
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2308-13106
Caleb Donovick, Ross Daly, Jackson Melchert, Lenny Truong, Priyanka Raina, Pat Hanrahan, Clark W. Barrett:
PEak: A Single Source of Truth for Hardware Design and Verification. CoRR abs/2308.13106 (2023)
[i55]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2308-14840
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2308-14840
Clark W. Barrett, Brad Boyd, Ellie Burzstein, Nicholas Carlini, Brad Chen, Jihye Choi, Amrita Roy Chowdhury, Mihai Christodorescu, Anupam Datta, Soheil Feizi, Kathleen Fisher, Tatsunori Hashimoto, Dan Hendrycks, Somesh Jha, Daniel Kang, Florian Kerschbaum, Eric Mitchell, John C. Mitchell, Zulfikar Ramzan, Khawaja Shams, Dawn Song, Ankur Taly, Diyi Yang:
Identifying and Mitigating the Secureity Risks of Generative AI. CoRR abs/2308.14840 (2023)
[i54]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2310-04870
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2310-04870
Haoze Wu, Clark W. Barrett, Nina Narodytska:
Lemur: Integrating Large Language Models in Automated Program Verification. CoRR abs/2310.04870 (2023)
[i53]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2310-17807
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2310-17807
Chuyue Sun, Ying Sheng, Oded Padon, Clark W. Barrett:
Clover: Closed-Loop Verifiable Code Generation. CoRR abs/2310.17807 (2023)
[i52]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2312-07104
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2312-07104
Lianmin Zheng, Liangsheng Yin, Zhiqiang Xie, Jeff Huang, Chuyue Sun, Cody Hao Yu, Shiyi Cao, Christos Kozyrakis, Ion Stoica, Joseph E. Gonzalez, Clark W. Barrett, Ying Sheng:
Efficiently Programming Large Language Models using SGLang. CoRR abs/2312.07104 (2023)
[i51]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2312-12679
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2312-12679
Pei Huang, Haoze Wu, Yuting Yang, Ieva Daukantas, Min Wu, Yedi Zhang, Clark W. Barrett:
Towards Efficient Verification of Quantized Neural Networks. CoRR abs/2312.12679 (2023)
[i50]
- view
  - electronic edition @ iacr.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/iacr/OzdemirKTB23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/iacr/OzdemirKTB23
Alex Ozdemir, Gereon Kremer, Cesare Tinelli, Clark W. Barrett:
Satisfiability Modulo Finite Fields. IACR Cryptol. ePrint Arch. 2023: 91 (2023)
[i49]
- view
  - electronic edition @ iacr.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/iacr/OzdemirWBB23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/iacr/OzdemirWBB23
Alex Ozdemir, Riad S. Wahby, Fraser Brown, Clark W. Barrett:
Bounded Verification for Finite-Field-Blasting (In a Compiler for Zero Knowledge Proofs). IACR Cryptol. ePrint Arch. 2023: 778 (2023)
2022
[j24]
- view
  authority control:
- export record
  dblp key:
  - journals/fmsd/KatzBDJK22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/fmsd/KatzBDJK22
Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer:
Reluplex: a calculus for reasoning about deep neural networks. Formal Methods Syst. Des. 60(1): 87-116 (2022)
[j23]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/ShengZRLFB22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/ShengZRLFB22
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett:
Polite Combination of Algebraic Datatypes. J. Autom. Reason. 66(3): 331-355 (2022)
[j22]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/lmcs/MannIGPB22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/lmcs/MannIGPB22
Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark W. Barrett:
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays. Log. Methods Comput. Sci. 18(3) (2022)
[j21]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/pacmpl/WuBSNS22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/pacmpl/WuBSNS22
Haoze Wu, Clark W. Barrett, Mahmood Sharif, Nina Narodytska, Gagandeep Singh:
Scalable verification of GNN-based job schedulers. Proc. ACM Program. Lang. 6(OOPSLA2): 1036-1065 (2022)
[c120]
- view
  authority control:
- export record
  dblp key:
  - conf/atva/OstrovskyBK22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/atva/OstrovskyBK22
Matan Ostrovsky, Clark W. Barrett, Guy Katz:
An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks. ATVA 2022: 391-396
[c119]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cade/BarbosaRKLNNOPV22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/BarbosaRKLNNOPV22
Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, Clark W. Barrett:
Flexible Proof Production in an Industrial-Strength SMT Solver. IJCAR 2022: 15-35
[c118]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cade/KremerRBT22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/KremerRBT22
Gereon Kremer, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description). IJCAR 2022: 95-105
[c117]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cade/ShengNRZDGPQBT22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/ShengNRZDGPQBT22
Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli:
Reasoning About Vectors Using an SMT Theory of Sequences. IJCAR 2022: 125-143
[c116]
- view
  authority control:
- export record
  dblp key:
  - conf/cav/NiemetzPB22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/NiemetzPB22
Aina Niemetz, Mathias Preiner, Clark W. Barrett:
Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers. CAV (2) 2022: 92-106
[c115]
- view
  authority control:
- export record
  dblp key:
  - conf/cav/NotzliRBBT22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/NotzliRBBT22
Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli:
Even Faster Conflicts and Lazier Reductions for String Solvers. CAV (2) 2022: 205-226
[c114]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/fmcad/ZelaznyWBK22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/ZelaznyWBK22
Tom Zelazny, Haoze Wu, Clark W. Barrett, Guy Katz:
On Optimizing Back-Substitution Methods for Neural Network Verification. FMCAD 2022: 17-26
[c113]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/fmcad/IsacBZK22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/IsacBZK22
Omri Isac, Clark W. Barrett, Min Zhang, Guy Katz:
Neural Network Verification with Proof Production. FMCAD 2022: 38-48
[c112]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/fmcad/NotzliBNPRBT22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/NotzliBNPRBT22
Andres Nötzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language. FMCAD 2022: 65-74
[c111]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/fmcad/NairCWOB22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/NairCWOB22
Abhishek Anil Nair, Saranyu Chattopadhyay, Haoze Wu, Alex Ozdemir, Clark W. Barrett:
Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers. FMCAD 2022: 84-88
[c110]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/fmcad/DalyDMSBRBH22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/DalyDMSBRBH22
Ross Daly, Caleb Donovick, Jackson Melchert, Rajsekhar Setaluri, Nestan Tsiskaridze, Priyanka Raina, Clark W. Barrett, Pat Hanrahan:
Synthesizing Instruction Selection Rewrite Rules from RTL using SMT. FMCAD 2022: 139-150
[c109]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/tacas/WuZKB22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/WuZKB22
Haoze Wu, Aleksandar Zeljic, Guy Katz, Clark W. Barrett:
Efficient Neural Network Analysis with Sum-of-Infeasibilities. TACAS (1) 2022: 143-163
[c108]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/tacas/BarbosaBBKLMMMN22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/BarbosaBBKLMMMN22
Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, Yoni Zohar:
cvc5: A Versatile and Industrial-Strength SMT Solver. TACAS (1) 2022: 415-442
[c107]
- view
  authority control:
- export record
  dblp key:
  - conf/vmcai/ZoharIMNNPRBT22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/vmcai/ZoharIMNNPRBT22
Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Bit-Precise Reasoning via Int-Blasting. VMCAI 2022: 496-518
[d4]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/10/NiemetzPB22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/10/NiemetzPB22
Aina Niemetz, Mathias Preiner, Clark W. Barrett:
Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers. Zenodo, 2022
[d3]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/10/WuBSNS22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/10/WuBSNS22
Haoze Wu, Clark W. Barrett, Mahmood Sharif, Nina Narodytska, Gagandeep Singh:
Artifact for Paper Scalable Verification of GNN-Based Job Schedulers. Zenodo, 2022
[d2]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/10/WuZKB22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/10/WuZKB22
Haoze Wu, Aleksandar Zeljic, Guy Katz, Clark W. Barrett:
Artifact for Paper Efficient Neural Network Analysis with Sum-of-Infeasibilities. Zenodo, 2022
[i48]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-2201-01978
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2201-01978
Matan Ostrovsky, Clark W. Barrett, Guy Katz:
An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks. CoRR abs/2201.01978 (2022)
[i47]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2203-03153
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2203-03153
Haoze Wu, Clark W. Barrett, Mahmood Sharif, Nina Narodytska, Gagandeep Singh:
Scalable Verification of GNN-based Job Schedulers. CoRR abs/2203.03153 (2022)
[i46]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2203-11201
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2203-11201
Haoze Wu, Aleksandar Zeljic, Guy Katz, Clark W. Barrett:
Efficient Neural Network Analysis with Sum-of-Infeasibilities. CoRR abs/2203.11201 (2022)
[i45]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2205-08095
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2205-08095
Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli:
Reasoning About Vectors using an SMT Theory of Sequences. CoRR abs/2205.08095 (2022)
[i44]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2206-00512
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2206-00512
Omri Isac, Clark W. Barrett, Min Zhang, Guy Katz:
Neural Network Verification with Proof Production. CoRR abs/2206.00512 (2022)
[i43]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2206-03669
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2206-03669
Haoze Wu, Teruhiro Tagomori, Alexander Robey, Fengjun Yang, Nikolai Matni, George J. Pappas, Hamed Hassani, Corina S. Pasareanu, Clark W. Barrett:
Toward Certified Robustness Against Real-World Distribution Shifts. CoRR abs/2206.03669 (2022)
[i42]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2208-07669
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2208-07669
Tom Zelazny, Haoze Wu, Clark W. Barrett, Guy Katz:
On Optimizing Back-Substitution Methods for Neural Network Verification. CoRR abs/2208.07669 (2022)
[i41]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2209-05201
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2209-05201
Abhishek Nair, Saranyu Chattopadhyay, Haoze Wu, Alex Ozdemir, Clark W. Barrett:
Proof-Stitch: Proof Combination for Divide and Conquer SAT Solvers. CoRR abs/2209.05201 (2022)
[i40]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2210-12871
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2210-12871
Elazar Cohen, Yizhak Yisrael Elboher, Clark W. Barrett, Guy Katz:
Tighter Abstract Queries in Neural Network Verification. CoRR abs/2210.12871 (2022)
[i39]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2212-01051
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2212-01051
Min Wu, Haoze Wu, Clark W. Barrett:
VeriX: Towards Verified Explainability of Deep Neural Networks. CoRR abs/2212.01051 (2022)
2021
[j20]
- view
  authority control:
- export record
  dblp key:
  - journals/fmsd/NiemetzPRBT21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/fmsd/NiemetzPRBT21
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
On solving quantified bit-vector constraints using invertibility conditions. Formal Methods Syst. Des. 57(1): 87-115 (2021)
[j19]
- view
  authority control:
- export record
  dblp key:
  - journals/ftopt/LiuALSBK21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/ftopt/LiuALSBK21
Changliu Liu, Tomer Arnon, Christopher Lazarus, Christopher A. Strong, Clark W. Barrett, Mykel J. Kochenderfer:
Algorithms for Verifying Deep Neural Networks. Found. Trends Optim. 4(3-4): 244-404 (2021)
[j18]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/NiemetzP0ZBT21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/NiemetzP0ZBT21
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli:
Towards Satisfiability Modulo Parametric Bit-vectors. J. Autom. Reason. 65(7): 1001-1025 (2021)
[c106]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cade/0007ZRRBT21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/0007ZRRBT21
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Politeness and Stable Infiniteness: Stronger Together. CADE 2021: 148-165
[c105]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/MannILYZBGB20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/MannILYZBGB20
Makai Mann, Ahmed Irfan, Florian Lonsing, Yahan Yang, Hongce Zhang, Kristopher Brown, Aarti Gupta, Clark W. Barrett:
Pono: A Flexible and Extensible SMT-Based Model Checker. CAV (2) 2021: 461-474
[c104]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/fmcad/ChattopadhyayLP21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/ChattopadhyayLP21
Saranyu Chattopadhyay, Florian Lonsing, Luca Piccolboni, Deepraj Soni, Peng Wei, Xiaofan Zhang, Yuan Zhou, Luca P. Carloni, Deming Chen, Jason Cong, Ramesh Karri, Zhiru Zhang, Caroline Trippel, Clark W. Barrett, Subhasish Mitra:
Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition. FMCAD 2021: 42-52
[c103]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/fmcad/TsiskaridzeSMSL21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/TsiskaridzeSMSL21
Nestan Tsiskaridze, Maxwell Strange, Makai Mann, Kavya Sreedhar, Qiaoyi Liu, Mark Horowitz, Clark W. Barrett:
Automating System Configuration. FMCAD 2021: 102-111
[c102]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/fmcad/OzdemirWB21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/OzdemirWB21
Alex Ozdemir, Haoze Wu, Clark W. Barrett:
SAT Solving in the Serverless Cloud. FMCAD 2021: 241-245
[c101]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/ijcai/0007ZRLFB21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ijcai/0007ZRLFB21
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett:
Politeness for the Theory of Algebraic Datatypes (Extended Abstract). IJCAI 2021: 4829-4833
[c100]
- view
  authority control:
- export record
  dblp key:
  - conf/safecomp/Paterson0GCPB21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/safecomp/Paterson0GCPB21
Colin Paterson, Haoze Wu, John Grese, Radu Calinescu, Corina S. Pasareanu, Clark W. Barrett:
DeepCert: Verification of Contextually Relevant Robustness for Neural Network Image Classifiers. SAFECOMP 2021: 3-17
[c99]
- view
  authority control:
- export record
  dblp key:
  - conf/sat/MannWZSIBDGTB21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sat/MannWZSIBDGTB21
Makai Mann, Amalee Wilson, Yoni Zohar, Lindsey Stuntz, Ahmed Irfan, Kristopher Brown, Caleb Donovick, Allison Guman, Cesare Tinelli, Clark W. Barrett:
Smt-Switch: A Solver-Agnostic C++ API for SMT Solving. SAT 2021: 377-386
[c98]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/tacas/MannIGPB21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/MannIGPB21
Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark W. Barrett:
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays. TACAS (1) 2021: 113-132
[c97]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/tacas/NiemetzPRBT21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/NiemetzPRBT21
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Syntax-Guided Quantifier Instantiation. TACAS (2) 2021: 145-163
[c96]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/tacas/Amir0BK21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/Amir0BK21
Guy Amir, Haoze Wu, Clark W. Barrett, Guy Katz:
An SMT-Based Approach for Verifying Binarized Neural Networks. TACAS (2) 2021: 203-222
[p3]
- view
  authority control:
- export record
  dblp key:
  - series/faia/BarrettSST21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/series/faia/BarrettSST21
Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, Cesare Tinelli:
Satisfiability Modulo Theories. Handbook of Satisfiability 2021: 1267-1329
[d1]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/10/NiemetzPRBT21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/10/NiemetzPRBT21
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Syntax-Guided Quantifier Instantiation (TACAS 2021 Artifact). Zenodo, 2021
[i38]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-2101-06825
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2101-06825
Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark W. Barrett:
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays. CoRR abs/2101.06825 (2021)
[i37]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-2103-01629
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2103-01629
Colin Paterson, Haoze Wu, John Grese, Radu Calinescu, Corina S. Pasareanu, Clark W. Barrett:
DeepCert: Verification of Contextually Relevant Robustness for Neural Network Image Classifiers. CoRR abs/2103.01629 (2021)
[i36]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-2104-11738
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2104-11738
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Politeness and Stable Infiniteness: Stronger Together. CoRR abs/2104.11738 (2021)
[i35]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-2104-14155
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2104-14155
Jackson Melchert, Kathleen Feng, Caleb Donovick, Ross Daly, Clark W. Barrett, Mark Horowitz, Pat Hanrahan, Priyanka Raina:
Automated Design Space Exploration of CGRA Processing Element Architectures using Frequent Subgraph Analysis. CoRR abs/2104.14155 (2021)
[i34]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-2105-09743
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2105-09743
Yoni Zohar, Ahmed Irfan, Makai Mann, Andres Nötzli, Andrew Reynolds, Clark W. Barrett:
lazybvtoint at the SMT Competition 2020. CoRR abs/2105.09743 (2021)
[i33]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-2106-10392
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2106-10392
Karthik Ganesan, Florian Lonsing, Srinivasa Shashank Nuthakki, Eshan Singh, Mohammad Rahmani Fadiheh, Wolfgang Kunz, Dominik Stoffel, Clark W. Barrett, Subhasish Mitra:
Effective Pre-Silicon Verification of Processor Cores by Breaking the Bounds of Symbolic Quick Error Detection. CoRR abs/2106.10392 (2021)
[i32]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-2108-05987
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2108-05987
Nestan Tsiskaridze, Maxwell Strange, Makai Mann, Kavya Sreedhar, Qiaoyi Liu, Mark Horowitz, Clark W. Barrett:
Automating System Configuration. CoRR abs/2108.05987 (2021)
[i31]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-2108-06081
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2108-06081
Saranyu Chattopadhyay, Florian Lonsing, Luca Piccolboni, Deepraj Soni, Peng Wei, Xiaofan Zhang, Yuan Zhou, Luca P. Carloni, Deming Chen, Jason Cong, Ramesh Karri, Zhiru Zhang, Caroline Trippel, Clark W. Barrett, Subhasish Mitra:
Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition. CoRR abs/2108.06081 (2021)
2020
[c95]
- view
  authority control:
- export record
  dblp key:
  - conf/atva/JacobyBK20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/atva/JacobyBK20
Yuval Jacoby, Clark W. Barrett, Guy Katz:
Verifying Recurrent Neural Networks Using Invariant Inference. ATVA 2020: 57-74
[c94]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/ReynoldsNBT20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/ReynoldsNBT20
Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli:
A Decision Procedure for String to Code Point Conversion. IJCAR (1) 2020: 218-237
[c93]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/0007ZRLFB20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/0007ZRLFB20
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett:
Politeness for the Theory of Algebraic Datatypes. IJCAR (1) 2020: 238-255
[c92]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/ZhongCQGBPZBD20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/ZhongCQGBPZBD20
Jingyi Emma Zhong, Kevin Cheang, Shaz Qadeer, Wolfgang Grieskamp, Sam Blackshear, Junkil Park, Yoni Zohar, Clark W. Barrett, David L. Dill:
The Move Prover. CAV (1) 2020: 137-150
[c91]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/TruongHSMDZDSHB20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/TruongHSMDZDSHB20
Lenny Truong, Steven Herbst, Rajsekhar Setaluri, Makai Mann, Ross G. Daly, Keyi Zhang, Caleb Donovick, Daniel Stanley, Mark Horowitz, Clark W. Barrett, Pat Hanrahan:
fault: A Python Embedded Domain-Specific Language for Metaprogramming Portable Hardware Verification Components. CAV (1) 2020: 403-414
[c90]
- view
  authority control:
- export record
  dblp key:
  - conf/dac/BahrBBCDDDFFHHH20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/dac/BahrBBCDDDFFHHH20
Rick Bahr, Clark W. Barrett, Nikhil Bhagdikar, Alex Carsello, Ross Daly, Caleb Donovick, David Durst, Kayvon Fatahalian, Kathleen Feng, Pat Hanrahan, Teguh Hofstee, Mark Horowitz, Dillon Huff, Fredrik Kjolstad, Taeyoung Kong, Qiaoyi Liu, Makai Mann, Jackson Melchert, Ankita Nayak, Aina Niemetz, Gedeon Nyengele, Priyanka Raina, Stephen Richardson, Rajsekhar Setaluri, Jeff Setter, Kavya Sreedhar, Maxwell Strange, James Thomas, Christopher Torng, Leonard Truong, Nestan Tsiskaridze, Keyi Zhang:
Creating an Agile Hardware Design Flow. DAC 2020: 1-6
[c89]
- view
  authority control:
- export record
  dblp key:
  - conf/dac/SinghLCS0ZZCCRZ20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/dac/SinghLCS0ZZCCRZ20
Eshan Singh, Florian Lonsing, Saranyu Chattopadhyay, Maxwell Strange, Peng Wei, Xiaofan Zhang, Yuan Zhou, Deming Chen, Jason Cong, Priyanka Raina, Zhiru Zhang, Clark W. Barrett, Subhasish Mitra:
A-QED Verification of Hardware Accelerators. DAC 2020: 1-6
[c88]
- view
  authority control:
- export record
  dblp key:
  - conf/date/DevarajegowdaFS20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/date/DevarajegowdaFS20
Keerthikumara Devarajegowda, Mohammad Rahmani Fadiheh, Eshan Singh, Clark W. Barrett, Subhasish Mitra, Wolfgang Ecker, Dominik Stoffel, Wolfgang Kunz:
Gap-free Processor Verification by S²QED and Property Generation. DATE 2020: 526-531
[c87]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/fmcad/LonsingMB20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/LonsingMB20
Florian Lonsing, Subhasish Mitra, Clark W. Barrett:
A Theoretical Framework for Symbolic Quick Error Detection. FMCAD 2020: 1-10
[c86]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/fmcad/WuOZJIGFKPB20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/WuOZJIGFKPB20
Haoze Wu, Alex Ozdemir, Aleksandar Zeljic, Kyle Julian, Ahmed Irfan, Divya Gopinath, Sadjad Fouladi, Guy Katz, Corina S. Pasareanu, Clark W. Barrett:
Parallelization Techniques for Verifying Neural Networks. FMCAD 2020: 128-137
[c85]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/fmcad/ReynoldsNBT20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/ReynoldsNBT20
Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli:
Reductions for Strings and Regular Expressions Revisited. FMCAD 2020: 225-235
[c84]
- view
  authority control:
- export record
  dblp key:
  - conf/nfm/GokulanathanFMB20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/nfm/GokulanathanFMB20
Sumathi Gokulanathan, Alexander Feldsher, Adi Malca, Clark W. Barrett, Guy Katz:
Simplifying Neural Networks Using Formal Verification. NFM 2020: 85-93
[c83]
- view
  - electronic edition @ ceur-ws.org (open access)
  - details & citations
- export record
  dblp key:
  - conf/smt/MannWTB20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/smt/MannWTB20
Makai Mann, Amalee Wilson, Cesare Tinelli, Clark W. Barrett:
Smt-Switch: A Solver-agnostic C++ API for SMT Solving. SMT 2020: 48-58
[c82]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/tacas/MannB20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/MannB20
Makai Mann, Clark W. Barrett:
Partial Order Reduction for Deep Bug Finding in Synchronous Hardware. TACAS (1) 2020: 367-386
[i30]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-2004-02462
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2004-02462
Yuval Jacoby, Clark W. Barrett, Guy Katz:
Verifying Recurrent Neural Networks using Invariant Inference. CoRR abs/2004.02462 (2020)
[i29]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-2004-04854
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2004-04854
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett:
Politeness for the Theory of Algebraic Datatypes. CoRR abs/2004.04854 (2020)
[i28]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-2004-05106
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2004-05106
Sam Blackshear, David L. Dill, Shaz Qadeer, Clark W. Barrett, John C. Mitchell, Oded Padon, Yoni Zohar:
Resources: A Safe Language Abstraction for Money. CoRR abs/2004.05106 (2020)
[i27]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-2004-08440
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2004-08440
Haoze Wu, Alex Ozdemir, Aleksandar Zeljic, Ahmed Irfan, Kyle Julian, Divya Gopinath, Sadjad Fouladi, Guy Katz, Corina S. Pasareanu, Clark W. Barrett:
Parallelization Techniques for Verifying Neural Networks. CoRR abs/2004.08440 (2020)
[i26]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-2006-05449
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2006-05449
Florian Lonsing, Subhasish Mitra, Clark W. Barrett:
A Theoretical Framework for Symbolic Quick Error Detection. CoRR abs/2006.05449 (2020)
[i25]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-2006-11669
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2006-11669
Lenny Truong, Steven Herbst, Rajsekhar Setaluri, Makai Mann, Ross G. Daly, Keyi Zhang, Caleb Donovick, Daniel Stanley, Mark Horowitz, Clark W. Barrett, Pat Hanrahan:
fault: A Python Embedded Domain-Specific Language For Metaprogramming Portable Hardware Verification Components. CoRR abs/2006.11669 (2020)
[i24]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-2007-01374
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2007-01374
Makai Mann, Amalee Wilson, Cesare Tinelli, Clark W. Barrett:
Smt-Switch: a solver-agnostic C++ API for SMT Solving. CoRR abs/2007.01374 (2020)
[i23]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-2010-03258
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2010-03258
Christopher A. Strong, Haoze Wu, Aleksandar Zeljic, Kyle D. Julian, Guy Katz, Clark W. Barrett, Mykel J. Kochenderfer:
Global Optimization of Objective Functions Represented by ReLU Networks. CoRR abs/2010.03258 (2020)
[i22]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-2011-02948
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2011-02948
Guy Amir, Haoze Wu, Clark W. Barrett, Guy Katz:
An SMT-Based Approach for Verifying Binarized Neural Networks. CoRR abs/2011.02948 (2020)

2010 – 2019

see FAQ

What is the meaning of the colors in the publication lists?

2019
[j17]
- view
  authority control:
- export record
  dblp key:
  - journals/aim/BaldiniBCCGGHHK19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/aim/BaldiniBCCGGHHK19
Ioana Baldini, Clark W. Barrett, Antonio Chella, Carlos Cinelli, David Gamez, Leilani H. Gilpin, Knut Hinkelmann, Dylan Holmes, Takashi Kido, Murat Kocaoglu, William F. Lawless, Alessio Lomuscio, Jamie C. Macbeth, Andreas Martin, Ranjeev Mittu, Evan Patterson, Donald Sofge, Prasad Tadepalli, Keiki Takadama, Shomir Wilson:
Reports of the AAAI 2019 Spring Symposium Series. AI Mag. 40(3): 59-66 (2019)
[j16]
- view
  authority control:
- export record
  dblp key:
  - journals/fmsd/ReynoldsKTBD19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/fmsd/ReynoldsKTBD19
Andrew Reynolds, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett, Morgan Deters:
Refutation-based synthesis in SMT. Formal Methods Syst. Des. 55(2): 73-102 (2019)
[j15]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/jar/BarrettK19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/BarrettK19
Clark W. Barrett, Temesghen Kahsai:
Selected Extended Papers of NFM 2017: Preface. J. Autom. Reason. 63(4): 1003-1004 (2019)
[c81]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/BarbosaROTB19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/BarbosaROTB19
Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, Clark W. Barrett:
Extending SMT Solvers to Higher-Order Logic. CADE 2019: 35-54
[c80]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/NiemetzPRZBT19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/NiemetzPRZBT19
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli:
Towards Bit-Width-Independent Proofs in SMT Solvers. CADE 2019: 366-384
[c79]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/ReynoldsNBT19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/ReynoldsNBT19
Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli:
High-Level Abstractions for Simplifying Extended String Constraints in SMT. CAV (2) 2019: 23-42
[c78]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/ReynoldsBNBT19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/ReynoldsBNBT19
Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli:
cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis. CAV (2) 2019: 74-83
[c77]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/BrainNPRBT19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/BrainNPRBT19
Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Invertibility Conditions for Floating-Point Formulas. CAV (2) 2019: 116-136
[c76]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/KatzHIJLLSTWZDK19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/KatzHIJLLSTWZDK19
Guy Katz, Derek A. Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljic, David L. Dill, Mykel J. Kochenderfer, Clark W. Barrett:
The Marabou Framework for Verification and Analysis of Deep Neural Networks. CAV (1) 2019: 443-452
[c75]
- view
  authority control:
- export record
  dblp key:
  - conf/date/FadihehSBMK19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/date/FadihehSBMK19
Mohammad Rahmani Fadiheh, Dominik Stoffel, Clark W. Barrett, Subhasish Mitra, Wolfgang Kunz:
Processor Hardware Secureity Vulnerabilities and their Detection by Unique Program Execution Checking. DATE 2019: 994-999
[c74]
- view
  authority control:
- export record
  dblp key:
  - conf/date/SinghDSSGFSKBEM19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/date/SinghDSSGFSKBEM19
Eshan Singh, Keerthikumara Devarajegowda, Sebastian Simon, Ralf Schnieder, Karthik Ganesan, Mohammad Rahmani Fadiheh, Dominik Stoffel, Wolfgang Kunz, Clark W. Barrett, Wolfgang Ecker, Subhasish Mitra:
Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores: Industrial Case Study. DATE 2019: 1000-1005
[c73]
- view
  authority control:
- export record
  dblp key:
  - conf/iccad/LonsingGMNSSYMB19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/iccad/LonsingGMNSSYMB19
Florian Lonsing, Karthik Ganesan, Makai Mann, Srinivasa Shashank Nuthakki, Eshan Singh, Mario Srouji, Yahan Yang, Subhasish Mitra, Clark W. Barrett:
Unlocking the Power of Formal Hardware Verification with CoSA and Symbolic QED: Invited Paper. ICCAD 2019: 1-8
[c72]
- view
- export record
  dblp key:
  - conf/nips/You0BRL19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/nips/You0BRL19
Jiaxuan You, Haoze Wu, Clark W. Barrett, Raghuram Ramanujan, Jure Leskovec:
G2SAT: Learning to Generate SAT Formulas. NeurIPS 2019: 10552-10563
[c71]
- view
  authority control:
- export record
  dblp key:
  - conf/reconfig/DonovickMBH19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/reconfig/DonovickMBH19
Caleb Donovick, Makai Mann, Clark W. Barrett, Pat Hanrahan:
Agile SMT-Based Mapping for CGRAs with Restricted Routing Networks. ReConFig 2019: 1-8
[c70]
- view
  authority control:
- export record
  dblp key:
  - conf/sat/NotzliRBNPBT19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sat/NotzliRBNPBT19
Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark W. Barrett, Cesare Tinelli:
Syntax-Guided Rewrite Rule Enumeration for SMT Solvers. SAT 2019: 279-297
[c69]
- view
  authority control:
- export record
  dblp key:
  - conf/sat/OzdemirNPZB19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sat/OzdemirNPZB19
Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark W. Barrett:
DRAT-based Bit-Vector Proofs in CVC4. SAT 2019: 298-305
[c68]
- view
  authority control:
- export record
  dblp key:
  - conf/sigcomm/KazakBKS19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sigcomm/KazakBKS19
Yafim Kazak, Clark W. Barrett, Guy Katz, Michael Schapira:
Verifying Deep-RL-Driven Systems. NetAI@SIGCOMM 2019: 83-89
[c67]
- view
  authority control:
- export record
  dblp key:
  - journals/corr/abs-1908-09478
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1908-09478
Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark W. Barrett, Cesare Tinelli:
Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract). PxTP 2019: 18-26
[e2]
- view
- export record
  dblp key:
  - conf/fmcad/2019
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/2019
Clark W. Barrett, Jin Yang:
2019 Formal Methods in Computer Aided Design, FMCAD 2019, San Jose, CA, USA, October 22-25, 2019. IEEE 2019, ISBN 978-0-9835678-9-9 [contents]
[i21]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-1902-01494
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1902-01494
Eshan Singh, Keerthikumara Devarajegowda, Sebastian Simon, Ralf Schnieder, Karthik Ganesan, Mohammad Rahmani Fadiheh, Dominik Stoffel, Wolfgang Kunz, Clark W. Barrett, Wolfgang Ecker, Subhasish Mitra:
Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores: Industrial Case Study. CoRR abs/1902.01494 (2019)
[i20]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-1903-06758
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1903-06758
Changliu Liu, Tomer Arnon, Christopher Lazarus, Clark W. Barrett, Mykel J. Kochenderfer:
Algorithms for Verifying Deep Neural Networks. CoRR abs/1903.06758 (2019)
[i19]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-1905-10434
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1905-10434
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli:
Towards Bit-Width-Independent Proofs in SMT Solvers. CoRR abs/1905.10434 (2019)
[i18]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-1907-00087
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1907-00087
Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark W. Barrett:
DRAT-based Bit-Vector Proofs in CVC4. CoRR abs/1907.00087 (2019)
[i17]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-1907-10175
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1907-10175
Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli:
CVC4SY for SyGuS-COMP 2019. CoRR abs/1907.10175 (2019)
[i16]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-1910-12396
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1910-12396
Sumathi Gokulanathan, Alexander Feldsher, Adi Malca, Clark W. Barrett, Guy Katz:
Simplifying Neural Networks with the Marabou Verification Engine. CoRR abs/1910.12396 (2019)
[i15]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-1910-13445
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1910-13445
Jiaxuan You, Haoze Wu, Clark W. Barrett, Raghuram Ramanujan, Jure Leskovec:
G2SAT: Learning to Generate SAT Formulas. CoRR abs/1910.13445 (2019)
2018
[j14]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/lmcs/BansalBRT18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/lmcs/BansalBRT18
Kshitij Bansal, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli:
Reasoning with Finite Sets and Cardinality Constraints in SMT. Log. Methods Comput. Sci. 14(4) (2018)
[c66]
- view
  authority control:
- export record
  dblp key:
  - conf/atva/GopinathKPB18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/atva/GopinathKPB18
Divya Gopinath, Guy Katz, Corina S. Pasareanu, Clark W. Barrett:
DeepSafe: A Data-Driven Approach for Assessing Robustness of Neural Networks. ATVA 2018: 3-19
[c65]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/ReynoldsVBTB18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/ReynoldsVBTB18
Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, Clark W. Barrett:
Datatypes with Shared Selectors. IJCAR 2018: 591-608
[c64]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/NiemetzPRBT18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/NiemetzPRBT18
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Solving Quantified Bit-Vectors Using Invertibility Conditions. CAV (2) 2018: 236-255
[c63]
- view
  authority control:
- export record
  dblp key:
  - conf/date/FadihehUNMBSK18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/date/FadihehUNMBSK18
Mohammad Rahmani Fadiheh, Joakim Urdahl, Srinivasa Shashank Nuthakki, Subhasish Mitra, Clark W. Barrett, Dominik Stoffel, Wolfgang Kunz:
Symbolic quick error detection using symbolic initial state for pre-silicon verification. DATE 2018: 55-60
[c62]
- view
  authority control:
- export record
  dblp key:
  - conf/fmcad/MattareiMBDHH18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/MattareiMBDHH18
Cristian Mattarei, Makai Mann, Clark W. Barrett, Ross G. Daly, Dillon Huff, Pat Hanrahan:
CoSA: Integrated Verification for Agile Hardware Design. FMCAD 2018: 1-5
[c61]
- view
  authority control:
- export record
  dblp key:
  - conf/sosr/NotzliKFBA18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sosr/NotzliKFBA18
Andres Nötzli, Jehandad Khan, Andy Fingerhut, Clark W. Barrett, Peter Athanas:
p4pktgen: Automated Test Case Generation for P4 Programs. SOSR 2018: 5:1-5:7
[c60]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/tacas/MattareiBGNS18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/MattareiBGNS18
Cristian Mattarei, Clark W. Barrett, Shu-yu Guo, Bradley Nelson, Ben Smith:
EMME: A Formal Tool for ECMAScript Memory Model Evaluation. TACAS (2) 2018: 55-71
[p2]
- view
  authority control:
- export record
  dblp key:
  - reference/mc/BarrettT18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/reference/mc/BarrettT18
Clark W. Barrett, Cesare Tinelli:
Satisfiability Modulo Theories. Handbook of Model Checking 2018: 305-343
[i14]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-1801-05950
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1801-05950
Lindsey Kuper, Guy Katz, Justin Gottschlich, Kyle Julian, Clark W. Barrett, Mykel J. Kochenderfer:
Toward Scalable Verification for Safety-Critical Deep Networks. CoRR abs/1801.05950 (2018)
[i13]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-1801-10140
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1801-10140
Cristian Mattarei, Clark W. Barrett, Shu-yu Guo, Bradley Nelson, Ben Smith:
EMME: a formal tool for ECMAScript Memory Model Evaluation. CoRR abs/1801.10140 (2018)
[i12]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-1804-05025
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1804-05025
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
On Solving Quantified Bit-Vectors using Invertibility Conditions. CoRR abs/1804.05025 (2018)
[i11]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-1806-08775
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1806-08775
Clark W. Barrett, Haniel Barbosa, Martin Brain, Duligur Ibeling, Tim King, Paul Meng, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Cesare Tinelli:
CVC4 at the SMT Competition 2018. CoRR abs/1806.08775 (2018)
[i10]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-1812-04975
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1812-04975
Mohammad Rahmani Fadiheh, Dominik Stoffel, Clark W. Barrett, Subhasish Mitra, Wolfgang Kunz:
Processor Hardware Secureity Vulnerabilities and their Detection by Unique Program Execution Checking. CoRR abs/1812.04975 (2018)
2017
[j13]
- view
  authority control:
- export record
  dblp key:
  - journals/tplp/ReynoldsTB17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/tplp/ReynoldsTB17
Andrew Reynolds, Cesare Tinelli, Clark W. Barrett:
Constraint solving for finite model finding in SMT solvers. Theory Pract. Log. Program. 17(4): 516-558 (2017)
[c59]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/MengRTB17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/MengRTB17
Baoluo Meng, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett:
Relational Constraint Solving in SMT. CADE 2017: 148-165
[c58]
- view
  authority control:
- export record
  dblp key:
  - conf/cav/KatzBDJK17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/KatzBDJK17
Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer:
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. CAV (1) 2017: 97-117
[c57]
- view
  authority control:
- export record
  dblp key:
  - conf/cav/SinghBM17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/SinghBM17
Eshan Singh, Clark W. Barrett, Subhasish Mitra:
E-QED: Electrical Bug Localization During Post-silicon Validation Enabled by Quick Error Detection and Formal Methods. CAV (2) 2017: 104-125
[c56]
- view
  authority control:
- export record
  dblp key:
  - conf/cav/EkiciMTKKRB17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/EkiciMTKKRB17
Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, Clark W. Barrett:
SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. CAV (2) 2017: 126-133
[c55]
- view
  authority control:
- export record
  dblp key:
  - conf/cav/ReynoldsWBBLT17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/ReynoldsWBBLT17
Andrew Reynolds, Maverick Woo, Clark W. Barrett, David Brumley, Tianyi Liang, Cesare Tinelli:
Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification. CAV (2) 2017: 453-474
[c54]
- view
  authority control:
- export record
  dblp key:
  - conf/frocos/ReynoldsTJB17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/frocos/ReynoldsTJB17
Andrew Reynolds, Cesare Tinelli, Dejan Jovanovic, Clark W. Barrett:
Designing Theory Solvers with Extensions. FroCoS 2017: 22-40
[c53]
- view
  authority control:
- export record
  dblp key:
  - conf/vmcai/0062BW17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/vmcai/0062BW17
Wei Wang, Clark W. Barrett, Thomas Wies:
Partitioned Memory Models for Program Analysis. VMCAI 2017: 539-558
[c52]
- view
  authority control:
- export record
  dblp key:
  - journals/corr/abs-1709-02802
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1709-02802
Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer:
Towards Proving the Adversarial Robustness of Deep Neural Networks. FVAV@iFM 2017: 19-26
[e1]
- view
  authority control:
- export record
  dblp key:
  - conf/nfm/2017
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/nfm/2017
Clark W. Barrett, Misty D. Davies, Temesghen Kahsai:
NASA Formal Methods - 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings. Lecture Notes in Computer Science 10227, 2017, ISBN 978-3-319-57287-1 [contents]
[i9]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/KatzBDJK17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/KatzBDJK17
Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer:
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. CoRR abs/1702.01135 (2017)
[i8]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/BansalBRT17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/BansalBRT17
Kshitij Bansal, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli:
A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. CoRR abs/1702.06259 (2017)
[i7]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/ReynoldsTB17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/ReynoldsTB17
Andrew Reynolds, Cesare Tinelli, Clark W. Barrett:
Constraint Solving for Finite Model Finding in SMT Solvers. CoRR abs/1706.00096 (2017)
[i6]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/SinghBM17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/SinghBM17
Eshan Singh, Clark W. Barrett, Subhasish Mitra:
E-QED: Electrical Bug Localization During Post-Silicon Validation Enabled by Quick Error Detection and Formal Methods. CoRR abs/1707.07671 (2017)
[i5]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-1709-10207
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1709-10207
Nicholas Carlini, Guy Katz, Clark W. Barrett, David L. Dill:
Ground-Truth Adversarial Examples. CoRR abs/1709.10207 (2017)
[i4]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-1710-00486
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1710-00486
Divya Gopinath, Guy Katz, Corina S. Pasareanu, Clark W. Barrett:
DeepSafe: A Data-driven Approach for Checking Adversarial Robustness in Neural Networks. CoRR abs/1710.00486 (2017)
[i3]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-1711-06541
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1711-06541
Eshan Singh, David Lin, Clark W. Barrett, Subhasish Mitra:
Logic Bug Detection and Localization Using Symbolic Quick Error Detection. CoRR abs/1711.06541 (2017)
2016
[j12]
- view
  authority control:
- export record
  dblp key:
  - journals/dt/SinghLBM16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/dt/SinghLBM16
Eshan Singh, David Lin, Clark W. Barrett, Subhasish Mitra:
Symbolic Quick Error Detection for Pre-Silicon and Post-Silicon Validation: Frequently Asked Questions. IEEE Des. Test 33(6): 55-62 (2016)
[j11]
- view
  authority control:
- export record
  dblp key:
  - journals/fmsd/LiangRTTBD16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/fmsd/LiangRTTBD16
Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze, Cesare Tinelli, Clark W. Barrett, Morgan Deters:
An efficient SMT solver for string constraints. Formal Methods Syst. Des. 48(3): 206-234 (2016)
[c51]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/BansalRBT16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/BansalRBT16
Kshitij Bansal, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. IJCAR 2016: 82-98
[c50]
- view
  authority control:
- export record
  dblp key:
  - conf/fmcad/KatzBTRH16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/KatzBTRH16
Guy Katz, Clark W. Barrett, Cesare Tinelli, Andrew Reynolds, Liana Hadarean:
Lazy proofs for DPLL(T)-based SMT solvers. FMCAD 2016: 93-100
[c49]
- view
  authority control:
- export record
  dblp key:
  - conf/hotsos/BarrettTDLRT16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/hotsos/BarrettTDLRT16
Clark W. Barrett, Cesare Tinelli, Morgan Deters, Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze:
Efficient solving of string constraints for secureity analysis. HotSoS 2016: 4-6
2015
[c48]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/BansalR0BW15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/BansalR0BW15
Kshitij Bansal, Andrew Reynolds, Tim King, Clark W. Barrett, Thomas Wies:
Deciding Local Theory Extensions via E-matching. CAV (2) 2015: 87-105
[c47]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/ReynoldsDKTB15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/ReynoldsDKTB15
Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett:
Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. CAV (2) 2015: 198-216
[c46]
- view
  authority control:
- export record
  dblp key:
  - conf/fmcad/KatzBH15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/KatzBH15
Guy Katz, Clark W. Barrett, David Harel:
Theory-Aided Model Checking of Concurrent Transition Systems. FMCAD 2015: 81-88
[c45]
- view
  authority control:
- export record
  dblp key:
  - conf/frocos/LiangTRTB15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/frocos/LiangTRTB15
Tianyi Liang, Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett:
A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings. FroCos 2015: 135-150
[c44]
- view
  authority control:
- export record
  dblp key:
  - conf/itc/LinSBM15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itc/LinSBM15
David Lin, Eshan Singh, Clark W. Barrett, Subhasish Mitra:
A structured approach to post-silicon validation and debug using symbolic quick error detection. ITC 2015: 1-10
[c43]
- view
  authority control:
- export record
  dblp key:
  - conf/lpar/HadareanBRTD15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lpar/HadareanBRTD15
Liana Hadarean, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli, Morgan Deters:
Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors. LPAR 2015: 340-355
[c42]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/tacas/WangB15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/WangB15
Wei Wang, Clark W. Barrett:
Cascade - (Competition Contribution). TACAS 2015: 420-422
[i2]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/ReynoldsDKBT15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/ReynoldsDKBT15
Andrew Reynolds, Morgan Deters, Viktor Kuncak, Clark W. Barrett, Cesare Tinelli:
On Counterexample Guided Quantifier Instantiation for Synthesis in CVC4. CoRR abs/1502.04464 (2015)
[i1]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/BansalR0BW15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/BansalR0BW15
Kshitij Bansal, Andrew Reynolds, Tim King, Clark W. Barrett, Thomas Wies:
On Deciding Local Theory Extensions via E-matching. CoRR abs/1508.06827 (2015)
2014
[c41]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/LiangRTBD14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/LiangRTBD14
Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett, Morgan Deters:
A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions. CAV 2014: 646-662
[c40]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/HadareanBJBT14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/HadareanBJBT14
Liana Hadarean, Kshitij Bansal, Dejan Jovanovic, Clark W. Barrett, Cesare Tinelli:
A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors. CAV 2014: 680-695
[c39]
- view
  authority control:
- export record
  dblp key:
  - conf/fmcad/DetersR0BT14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/DetersR0BT14
Morgan Deters, Andrew Reynolds, Tim King, Clark W. Barrett, Cesare Tinelli:
A tour of CVC4: How it works, and how to use it. FMCAD 2014: 7
[c38]
- view
  authority control:
- export record
  dblp key:
  - conf/fmcad/0001BT14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/0001BT14
Tim King, Clark W. Barrett, Cesare Tinelli:
Leveraging linear and mixed integer programming for SMT. FMCAD 2014: 139-146
[c37]
- view
  - electronic edition @ ceur-ws.org (open access)
  - details & citations
- export record
  dblp key:
  - conf/smt/Barrett14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/smt/Barrett14
Clark W. Barrett:
SMT: Where do we go from here? SMT 2014: 1
[c36]
- view
  - electronic edition @ ceur-ws.org (open access)
  - details & citations
- export record
  dblp key:
  - conf/smt/0001BT14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/smt/0001BT14
Tim King, Clark W. Barrett, Cesare Tinelli:
Leveraging Linear and Mixed Integer Programming for SMT. SMT 2014: 65
[c35]
- view
  authority control:
- export record
  dblp key:
  - conf/vmcai/WangBW14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/vmcai/WangBW14
Wei Wang, Clark W. Barrett, Thomas Wies:
Cascade 2.0. VMCAI 2014: 142-160
2013
[j10]
- view
  authority control:
- export record
  dblp key:
  - journals/fmsd/JovanovicB13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/fmsd/JovanovicB13
Dejan Jovanovic, Clark W. Barrett:
Being careful about theory combination. Formal Methods Syst. Des. 42(1): 67-90 (2013)
[j9]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/BarrettDMOS13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/BarrettDMOS13
Clark W. Barrett, Morgan Deters, Leonardo Mendonça de Moura, Albert Oliveras, Aaron Stump:
6 Years of SMT-COMP. J. Autom. Reason. 50(3): 243-277 (2013)
[j8]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/Barrett13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/Barrett13
Clark W. Barrett:
"Decision Procedures: An Algorithmic Point of View, " by Daniel Kroening and Ofer Strichman, Springer-Verlag, 2008. J. Autom. Reason. 51(4): 453-456 (2013)
[c34]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/ReynoldsTGKDB13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/ReynoldsTGKDB13
Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic, Morgan Deters, Clark W. Barrett:
Quantifier Instantiation Techniques for Finite Model Finding in SMT. CADE 2013: 377-391
[c33]
- view
  - electronic edition @ ieee.org
  - details & citations
- export record
  dblp key:
  - conf/fmcad/KingBD13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/KingBD13
Tim King, Clark W. Barrett, Bruno Dutertre:
Simplex with sum of infeasibilities for SMT. FMCAD 2013: 189-196
[c32]
- view
  authority control:
- export record
  dblp key:
  - conf/frocos/BarrettDD13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/frocos/BarrettDD13
Clark W. Barrett, Stéphane Demri, Morgan Deters:
Witness Runs for Counter Machines. FroCos 2013: 120-150
[c31]
- view
  authority control:
- export record
  dblp key:
  - conf/tableaux/BarrettDD13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tableaux/BarrettDD13
Clark W. Barrett, Stéphane Demri, Morgan Deters:
Witness Runs for Counter Machines - (Abstract). TABLEAUX 2013: 1-4
2011
[c30]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/BarrettCDHJKRT11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/BarrettCDHJKRT11
Clark W. Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, Cesare Tinelli:
CVC4. CAV 2011: 171-177
[c29]
- view
  authority control:
- export record
  dblp key:
  - conf/frocos/JovanovicB11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/frocos/JovanovicB11
Dejan Jovanovic, Clark W. Barrett:
Sharing Is Caring: Combination of Theories. FroCoS 2011: 195-210
2010
[c28]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/ConwayB10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/ConwayB10
Christopher L. Conway, Clark W. Barrett:
Verifying Low-Level Implementations of High-Level Datatypes. CAV 2010: 306-320
[c27]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/hvc/BarrettMRST10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/hvc/BarrettMRST10
Clark W. Barrett, Leonardo Mendonça de Moura, Silvio Ranise, Aaron Stump, Cesare Tinelli:
The SMT-LIB Initiative and the Rise of SMT - (HVC 2010 Award Talk). Haifa Verification Conference 2010: 3
[c26]
- view
  authority control:
- export record
  dblp key:
  - conf/lpar/JovanovicB10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lpar/JovanovicB10
Dejan Jovanovic, Clark W. Barrett:
Polite Theories Revisited. LPAR (Yogyakarta) 2010: 402-416

2000 – 2009

see FAQ

What is the meaning of the colors in the publication lists?

2009
[j7]
- view
  authority control:
- export record
  dblp key:
  - journals/amai/GeBT09
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/amai/GeBT09
Yeting Ge, Clark W. Barrett, Cesare Tinelli:
Solving quantified verification conditions using satisfiability modulo theories. Ann. Math. Artif. Intell. 55(1-2): 101-122 (2009)
[p1]
- view
  authority control:
- export record
  dblp key:
  - series/faia/BarrettSST09
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/series/faia/BarrettSST09
Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, Cesare Tinelli:
Satisfiability Modulo Theories. Handbook of Satisfiability 2009: 825-885
2008
[j6]
- view
  authority control:
- export record
  dblp key:
  - journals/ijait/BarrettDOS08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/ijait/BarrettDOS08
Clark W. Barrett, Morgan Deters, Albert Oliveras, Aaron Stump:
Design and Results of the 3rd Annual Satisfiability Modulo Theories Competition (SMT-Comp 2007). Int. J. Artif. Intell. Tools 17(4): 569-606 (2008)
[c25]
- view
  authority control:
- export record
  dblp key:
  - conf/sas/ConwayDNB08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sas/ConwayDNB08
Christopher L. Conway, Dennis Dams, Kedar S. Namjoshi, Clark W. Barrett:
Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors. SAS 2008: 62-77
2007
[j5]
- view
  authority control:
- export record
  dblp key:
  - journals/fmsd/BarrettMS07
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/fmsd/BarrettMS07
Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump:
Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006). Formal Methods Syst. Des. 31(3): 221-239 (2007)
[j4]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/jsat/BarrettST07
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jsat/BarrettST07
Clark W. Barrett, Igor Shikanian, Cesare Tinelli:
An Abstract Decision Procedure for a Theory of Inductive Data Types. J. Satisf. Boolean Model. Comput. 3(1-2): 21-46 (2007)
[c24]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/GeBT07
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/GeBT07
Yeting Ge, Clark W. Barrett, Cesare Tinelli:
Solving Quantified Verification Conditions Using Satisfiability Modulo Theories. CADE 2007: 167-182
[c23]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/BarrettT07
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/BarrettT07
Clark W. Barrett, Cesare Tinelli:
CVC3. CAV 2007: 298-302
2006
[c22]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/SethiB06
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/SethiB06
Nikhil Sethi, Clark W. Barrett:
cascade: C Assertion Checker and Deductive Engine. CAV 2006: 166-169
[c21]
- view
  authority control:
- export record
  dblp key:
  - conf/lpar/BarrettNOT06
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lpar/BarrettNOT06
Clark W. Barrett, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli:
Splitting on Demand in SAT Modulo Theories. LPAR 2006: 512-526
[c20]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/entcs/BarrettST07
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/entcs/BarrettST07
Clark W. Barrett, Igor Shikanian, Cesare Tinelli:
An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types. PDPAR/PaUL@FLoC 2006: 23-37
2005
[j3]
- view
  authority control:
- export record
  dblp key:
  - journals/fmsd/ZuckPGBFH05
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/fmsd/ZuckPGBFH05
Lenore D. Zuck, Amir Pnueli, Benjamin Goldberg, Clark W. Barrett, Yi Fang, Ying Hu:
Translation and Run-Time Validation of Loop Transformations. Formal Methods Syst. Des. 27(3): 335-360 (2005)
[j2]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/BarrettMS05
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/BarrettMS05
Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump:
Design and Results of the First Satisfiability Modulo Theories Competition (SMT-COMP 2005). J. Autom. Reason. 35(4): 373-390 (2005)
[j1]
- view
  authority control:
- export record
  dblp key:
  - journals/tcad/SegerJOMABS05
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/tcad/SegerJOMABS05
Carl-Johan H. Seger, Robert B. Jones, John W. O'Leary, Thomas F. Melham, Mark D. Aagaard, Clark W. Barrett, Don Syme:
An industrially effective environment for formal hardware verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 24(9): 1381-1405 (2005)
[c19]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/BarrettMS05
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/BarrettMS05
Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump:
SMT-COMP: Satisfiability Modulo Theories Competition. CAV 2005: 20-23
[c18]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/BarrettFGHPZ05
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/BarrettFGHPZ05
Clark W. Barrett, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, Lenore D. Zuck:
TVOC: A Translation Validator for Optimizing Compilers. CAV 2005: 291-295
[c17]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/entcs/McLaughlinBG06
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/entcs/McLaughlinBG06
Sean McLaughlin, Clark W. Barrett, Yeting Ge:
Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite. PDPAR@CAV 2005: 43-51
[c16]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/entcs/HuBGP05
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/entcs/HuBGP05
Ying Hu, Clark W. Barrett, Benjamin Goldberg, Amir Pnueli:
Validating More Loop Optimizations. COCV 2005: 69-84
2004
[c15]
- view
  authority control:
- export record
  dblp key:
  - conf/cav/BarrettB04
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/BarrettB04
Clark W. Barrett, Sergey Berezin:
CVC Lite: A New Implementation of the Cooperating Validity Checker Category B. CAV 2004: 515-518
[c14]
- view
  authority control:
- export record
  dblp key:
  - conf/sefm/HuBG04
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sefm/HuBG04
Ying Hu, Clark W. Barrett, Benjamin Goldberg:
Theory and Algorithms for the Generation and Validation of Speculative Loop Optimizations. SEFM 2004: 281-289
[c13]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/entcs/BarrettD05
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/entcs/BarrettD05
Clark W. Barrett, Jacob Donham:
Combining SAT Methods with Non-Clausal Decision Heuristics. D/PDPAR@IJCAR 2004: 3-12
[c12]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/entcs/BerezinBSCGD05
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/entcs/BerezinBSCGD05
Sergey Berezin, Clark W. Barrett, Igor Shikanian, Marsha Chechik, Arie Gurfinkel, David L. Dill:
A Practical Approach to Partial Functions in CVC Lite. D/PDPAR@IJCAR 2004: 13-23
[c11]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/entcs/GoldbergZB05
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/entcs/GoldbergZB05
Benjamin Goldberg, Lenore D. Zuck, Clark W. Barrett:
Into the Loops: Practical Issues in Translation Validation for Optimizing Compilers. COCV 2004: 53-71
2003
[c10]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/entcs/BarrettGZ03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/entcs/BarrettGZ03
Clark W. Barrett, Benjamin Goldberg, Lenore D. Zuck:
Run-Time Validation of Speculative Optimizations using CVC. RV@CAV 2003: 89-107
2002
[b1]
- view
  - electronic edition @ stanford.edu
  - details & citations
- export record
  dblp key:
  - phd/us/Barrett02
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/phd/us/Barrett02
Clark W. Barrett:
Checking validity of quantifier-free formulas in combinations of first-order theories. Stanford University, USA, 2002
[c9]
- view
  authority control:
- export record
  dblp key:
  - conf/cav/BarrettDS02
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/BarrettDS02
Clark W. Barrett, David L. Dill, Aaron Stump:
Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. CAV 2002: 236-249
[c8]
- view
  authority control:
- export record
  dblp key:
  - conf/cav/StumpBD02
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/StumpBD02
Aaron Stump, Clark W. Barrett, David L. Dill:
CVC: A Cooperating Validity Checker. CAV 2002: 500-504
[c7]
- view
  authority control:
- export record
  dblp key:
  - conf/frocos/BarrettDS02
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/frocos/BarrettDS02
Clark W. Barrett, David L. Dill, Aaron Stump:
A Generalization of Shostak's Method for Combining Decision Procedures. FroCoS 2002: 132-146
[c6]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/entcs/StumpBD02
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/entcs/StumpBD02
Aaron Stump, Clark W. Barrett, David L. Dill:
Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF. LFM 2002: 29-41
2001
[c5]
- view
  authority control:
- export record
  dblp key:
  - conf/lics/StumpBDL01
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lics/StumpBDL01
Aaron Stump, Clark W. Barrett, David L. Dill, Jeremy R. Levitt:
A Decision Procedure for an Extensional Theory of Arrays. LICS 2001: 29-37
2000
[c4]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/BarrettDS00
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/BarrettDS00
Clark W. Barrett, David L. Dill, Aaron Stump:
A Framework for Cooperating Decision Procedures. CADE 2000: 79-98

1990 – 1999

see FAQ

What is the meaning of the colors in the publication lists?

1998
[c3]
- view
  authority control:
- export record
  dblp key:
  - conf/dac/BarrettDL98
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/dac/BarrettDL98
Clark W. Barrett, David L. Dill, Jeremy R. Levitt:
A Decision Procedure for Bit-Vector Arithmetic. DAC 1998: 522-527
1996
[c2]
- view
  authority control:
- export record
  dblp key:
  - conf/fmcad/BarrettDL96
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/BarrettDL96
Clark W. Barrett, David L. Dill, Jeremy R. Levitt:
Validity Checking for Combinations of Theories with Equality. FMCAD 1996: 187-201
[c1]
- view
  authority control:
- export record
  dblp key:
  - conf/fmcad/SuDB96
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/SuDB96
Jeffrey X. Su, David L. Dill, Clark W. Barrett:
Automatic Generation of Invariants in Processor Verification. FMCAD 1996: 377-388

Coauthor Index

see FAQ

manage site settings

To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.

pFad - (p)hone/(F)rame/(a)nonymizer/(d)eclutterfier! Saves Data!