BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Spain
2 × Austria
2 × Germany
2 × United Kingdom
4 × USA
Collaborated with:
C.Tinelli C.L.Conway W.Wang N.Sethi A.Reynolds M.Deters T.King T.Wies Y.Ge I.Shikanian L.Hadarean D.Jovanovic D.Dams K.S.Namjoshi K.Bansal T.Liang A.Goel S.Krstic
Talks about:
theori (4) cascad (3) smt (3) quantifi (2) solver (2) condit (2) level (2) cvc (2) implement (1) contribut (1)

Person: Clark Barrett

DBLP DBLP: Barrett:Clark

Contributed to:

TACAS 20152015
CAV 20142014
SMT 20142014
VMCAI 20142014
CADE 20132013
CAV 20112011
CAV 20102010
SAS 20082008
CADE 20072007
CAV 20072007
CAV 20062006
SMT 20062007

Wrote 15 papers:

TACAS-2015-WangB #contest #named
Cascade — (Competition Contribution) (WW, CB), pp. 420–422.
CAV-2014-HadareanBJBT #lazy evaluation
A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors (LH, KB, DJ, CB, CT), pp. 680–695.
CAV-2014-LiangRTBD #formal method #regular expression #string
A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions (TL, AR, CT, CB, MD), pp. 646–662.
SMT-2014-Barrett #named #question #smt
SMT: Where do we go from here? (CB), p. 1.
SMT-2014-KingBT #integer #linear #programming #smt
Leveraging Linear and Mixed Integer Programming for SMT (TK, CB, CT), p. 65.
Cascade 2.0 (WW, CB, TW), pp. 142–160.
CADE-2013-ReynoldsTGKDB #finite #quantifier #smt
Quantifier Instantiation Techniques for Finite Model Finding in SMT (AR, CT, AG, SK, MD, CB), pp. 377–391.
CVC4 (CB, CLC, MD, LH, DJ, TK, AR, CT), pp. 171–177.
CAV-2010-ConwayB #data type #implementation #low level #verification
Verifying Low-Level Implementations of High-Level Datatypes (CLC, CB), pp. 306–320.
SAS-2008-ConwayDNB #analysis #fault #pointer #proving
Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors (CLC, DD, KSN, CB), pp. 62–77.
CADE-2007-GeBT #modulo theories #quantifier #satisfiability #using #verification
Solving Quantified Verification Conditions Using Satisfiability Modulo Theories (YG, CB, CT), pp. 167–182.
CVC3 (CB, CT), pp. 298–302.
CAV-2006-SethiB #c #deduction #named
cascade: C Assertion Checker and Deductive Engine (NS, CB), pp. 166–169.
SMT-J-2006-BarrettST #data type #formal method #induction
An Abstract Decision Procedure for a Theory of Inductive Data Types (CB, IS, CT), pp. 21–46.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.