BibSLEIGH — Clark_W

Travelled to:

1 × China
1 × Denmark
1 × United Kingdom
5 × USA

Collaborated with:

A.Reynolds C.Tinelli D.L.Dill A.Stump B.Goldberg Y.Hu H.Barbosa J.R.Levitt A.Niemetz M.Preiner S.Berezin K.Bansal A.Nötzli G.Katz A.Pnueli L.M.d.Moura E.Singh S.Mitra K.Julian M.J.Kochenderfer B.Meng T.King T.Wies M.Deters V.Kuncak A.Viswanathan D.E.Ouraoui Y.Fang L.D.Zuck M.Woo D.Brumley T.Liang Y.Zohar M.Brain B.Ekici A.Mebsout C.Keller D.A.Huang D.Ibeling C.Lazarus R.Lim P.Shah S.Thakoor H.W.0001 A.Zeljic

Talks about:

smt (10) valid (6) solver (5) procedur (4) theori (4) decis (4) constraint (3) cooper (3) optim (3) cvc (3)

Person: Clark W. Barrett

DBLP: Barrett:Clark_W=

Contributed to:

2015

2005

2004

2002

2001

2000

1998

2016

2017

2018

2019

Wrote 26 papers:

CAV-2015-BansalR0BW: Deciding Local Theory Extensions via E-matching (KB, AR, TK, CWB, TW), pp. 87–105.
CAV-2015-ReynoldsDKTB #quantifier #smt #synthesis: Counterexample-Guided Quantifier Instantiation for Synthesis in SMT (AR, MD, VK, CT, CWB), pp. 198–216.
CAV-2005-BarrettFGHPZ #compilation #named #optimisation #validation: TVOC: A Translation Validator for Optimizing Compilers (CWB, YF, BG, YH, AP, LDZ), pp. 291–295.
CAV-2005-BarrettMS #contest #modulo theories #named #satisfiability: SMT-COMP: Satisfiability Modulo Theories Competition (CWB, LMdM, AS), pp. 20–23.
COCV-J-2005-HuBGP #optimisation #validation: Validating More Loop Optimizations (YH, CWB, BG, AP), pp. 69–84.
CAV-2004-BarrettB #implementation: CVC Lite: A New Implementation of the Cooperating Validity Checker Category B (CWB, SB), pp. 515–518.
SEFM-2004-HuBG #algorithm #generative #optimisation #validation: Theory and Algorithms for the Generation and Validation of Speculative Loop Optimizations (YH, CWB, BG), pp. 281–289.
CAV-2002-BarrettDS #first-order #incremental #satisfiability: Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT (CWB, DLD, AS), pp. 236–249.
CAV-2002-StumpBD #named: CVC: A Cooperating Validity Checker (AS, CWB, DLD), pp. 500–504.
LICS-2001-StumpBDL #array: A Decision Procedure for an Extensional Theory of Arrays (AS, CWB, DLD, JRL), pp. 29–37.
CADE-2000-BarrettDS #framework: A Framework for Cooperating Decision Procedures (CWB, DLD, AS), pp. 79–98.
DAC-1998-BarrettDL: A Decision Procedure for Bit-Vector Arithmetic (CWB, DLD, JRL), pp. 522–527.
IJCAR-2016-BansalRBT #constraints #finite #set #smt: A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT (KB, AR, CWB, CT), pp. 82–98.
CADE-2017-MengRTB #constraints #relational #smt #theorem proving: Relational Constraint Solving in SMT (BM, AR, CT, CWB), pp. 148–165.
CAV-2017-KatzBDJK #named #network #performance #smt #verification: Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks (GK, CWB, DLD, KJ, MJK), pp. 97–117.
CAV-2017-EkiciMTKKRB #coq #named #plugin #smt: SMTCoq: A Plug-In for Integrating SMT Solvers into Coq (BE, AM, CT, CK, GK, AR, CWB), pp. 126–133.
CAV-2017-ReynoldsWBBLT #scalability #string #using: Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification (AR, MW, CWB, DB, TL, CT), pp. 453–474.
CAV-2017-SinghBM #debugging #detection #fault #formal method #locality #named #validation: E-QED: Electrical Bug Localization During Post-silicon Validation Enabled by Quick Error Detection and Formal Methods (ES, CWB, SM), pp. 104–125.
CAV-2018-NiemetzPRBT #quantifier #using: Solving Quantified Bit-Vectors Using Invertibility Conditions (AN, MP, AR, CWB, CT), pp. 236–255.
IJCAR-2018-ReynoldsVBTB #data type: Datatypes with Shared Selectors (AR, AV, HB, CT, CWB), pp. 591–608.
CADE-2019-BarbosaROTB #higher-order #logic #smt: Extending SMT Solvers to Higher-Order Logic (HB, AR, DEO, CT, CWB), pp. 35–54.
CADE-2019-NiemetzPRZBT #independence #proving #smt #towards: Towards Bit-Width-Independent Proofs in SMT Solvers (AN, MP, AR, YZ, CWB, CT), pp. 366–384.
CAV-2019-KatzHIJLLSTWZDK #analysis #framework #network #verification: The Marabou Framework for Verification and Analysis of Deep Neural Networks (GK, DAH, DI, KJ, CL, RL, PS, ST, HW0, AZ, DLD, MJK, CWB), pp. 443–452.
CAV-2019-BrainNPRBT #float: Invertibility Conditions for Floating-Point Formulas (MB, AN, MP, AR, CWB, CT), pp. 116–136.
CAV-2019-ReynoldsBNBT #named #performance #synthesis: cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis (AR, HB, AN, CWB, CT), pp. 74–83.
CAV-2019-ReynoldsNBT #abstraction #constraints #smt #string: High-Level Abstractions for Simplifying Extended String Constraints in SMT (AR, AN, CWB, CT), pp. 23–42.