×
Compute Distance To:
Author ID: barrett.clark-w Recent zbMATH articles by "Barrett, Clark W."
Published as: Barrett, Clark; Barrett, Clark W.; Barrett, Clack
External Links: MGP

Publications by Year

Citations contained in zbMATH Open

47 Publications have been cited 345 times in 231 Documents Cited by Year
Satisfiability modulo theories. Zbl 1392.68379
Barrett, Clark; Tinelli, Cesare
29
2018
Splitting on demand in SAT modulo theories. Zbl 1165.68480
Barrett, Clark; Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare
24
2006
CVC Lite: A new implementation of the cooperating validity checker – Category B. Zbl 1103.68605
Barrett, Clark; Berezin, Sergey
22
2004
CVC: A cooperating validity checker. Zbl 1010.68720
Stump, Aaron; Barrett, Clark W.; Dill, David L.
19
2002
Checking satisfiability of first-order formulas by incremental translation to SAT. Zbl 1010.68531
Barrett, Clark W.; Dill, David L.; Stump, Aaron
18
2002
Solving quantified verification conditions using satisfiability modulo theories. Zbl 1213.68376
Ge, Yeting; Barrett, Clark; Tinelli, Cesare
17
2007
Quantifier instantiation techniques for finite model finding in SMT. Zbl 1381.68275
Reynolds, Andrew; Tinelli, Cesare; Goel, Amit; Krstić, Sava; Deters, Morgan; Barrett, Clark
16
2013
Counterexample-guided quantifier instantiation for synthesis in SMT. Zbl 1381.68059
Reynolds, Andrew; Deters, Morgan; Kuncak, Viktor; Tinelli, Cesare; Barrett, Clark
15
2015
Polite theories revisited. Zbl 1306.68147
Jovanović, Dejan; Barrett, Clark
14
2010
An abstract decision procedure for a theory of inductive data types. Zbl 1129.68022
Barrett, Clack; Shikanian, Igor; Tinelli, Cesare
14
2007
A generalization of Shostak’s method for combining decision procedures. Zbl 1057.68109
Barrett, Clark W.; Dill, David L.; Stump, Aaron
13
2002
Cooperating theorem provers: a case study combining HOL-Light and CVC Lite. Zbl 1272.68362
Mclaughlin, Sean; Barrett, Clark; Ge, Yeting
12
2006
Extending SMT solvers to higher-order logic. Zbl 07178968
Barbosa, Haniel; Reynolds, Andrew; El Ouraoui, Daniel; Tinelli, Cesare; Barrett, Clark
10
2019
TVOC: A translation validator for optimizing compilers. Zbl 1081.68606
Barrett, Clark; Fang, Yi; Goldberg, Benjamin; Hu, Ying; Pnueli, Amir; Zuck, Lenore
9
2005
Solving quantified verification conditions using satisfiability modulo theories. Zbl 1184.68461
Ge, Yeting; Barrett, Clark; Tinelli, Cesare
8
2009
SMT-COMP: Satisfiability modulo theories competition. Zbl 1081.68607
Barrett, Clark; Moura, Leonardo; Stump, Aaron
8
2005
An abstract decision procedure for satisfiability in the theory of recursive data types. Zbl 1277.68132
Barrett, Clark; Shikanian, Igor; Tinelli, Cesare
7
2007
A decision procedure for regular membership and length constraints over unbounded strings. Zbl 1471.68119
Liang, Tianyi; Tsiskaridze, Nestan; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark
6
2015
A new decision procedure for finite sets and cardinality constraints in SMT. Zbl 1475.68430
Bansal, Kshitij; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare
5
2016
Deciding local theory extensions via E-matching. Zbl 1381.68280
Bansal, Kshitij; Reynolds, Andrew; King, Tim; Barrett, Clark; Wies, Thomas
5
2015
Designing theory solvers with extensions. Zbl 1495.68239
Reynolds, Andrew; Tinelli, Cesare; Jovanović, Dejan; Barrett, Clark
5
2017
Sharing is caring: combination of theories. Zbl 1348.68220
Jovanović, Dejan; Barrett, Clark
5
2011
Fine grained SMT proofs for the theory of fixed-width bit-vectors. Zbl 1471.68143
Hadarean, Liana; Barrett, Clark; Reynolds, Andrew; Tinelli, Cesare; Deters, Morgan
4
2015
A framework for cooperating decision procedures. Zbl 0963.68177
Barrett, Clark W.; Dill, David L.; Stump, Aaron
4
2000
Syntax-guided rewrite rule enumeration for SMT solvers. Zbl 1441.68233
Nötzli, Andres; Reynolds, Andrew; Barbosa, Haniel; Niemetz, Aina; Preiner, Mathias; Barrett, Clark; Tinelli, Cesare
4
2019
A practical approach to partial functions in CVC Lite. Zbl 1272.03136
Berezin, Sergey; Barrett, Clark; Shikanian, Igor; Chechik, Marsha; Gurfinkel, Arie; Dill, David L.
4
2005
Counterexample-guided prophecy for model checking modulo the theory of arrays. Zbl 1467.68089
Mann, Makai; Irfan, Ahmed; Griggio, Alberto; Padon, Oded; Barrett, Clark
4
2021
Refutation-based synthesis in SMT. Zbl 1427.68051
Reynolds, Andrew; Kuncak, Viktor; Tinelli, Cesare; Barrett, Clark; Deters, Morgan
3
2019
Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005). Zbl 1104.68719
Barrett, Clark; de Moura, Leonardo; Stump, Aaron
3
2005
An efficient SMT solver for string constraints. Zbl 1404.68135
Liang, Tianyi; Reynolds, Andrew; Tsiskaridze, Nestan; Tinelli, Cesare; Barrett, Clark; Deters, Morgan
3
2016
Relational constraint solving in SMT. Zbl 1494.68289
Meng, Baoluo; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark
3
2017
Datatypes with shared selectors. Zbl 06958125
Reynolds, Andrew; Viswanathan, Arjun; Barbosa, Haniel; Tinelli, Cesare; Barrett, Clark
3
2018
An SMT-based approach for verifying binarized neural networks. Zbl 1474.68188
Amir, Guy; Wu, Haoze; Barrett, Clark; Katz, Guy
3
2021
DRAT-based bit-vector proofs in CVC4. Zbl 1441.68235
Ozdemir, Alex; Niemetz, Aina; Preiner, Mathias; Zohar, Yoni; Barrett, Clark
3
2019
Reluplex: an efficient SMT solver for verifying deep neural networks. Zbl 1494.68167
Katz, Guy; Barrett, Clark; Dill, David L.; Julian, Kyle; Kochenderfer, Mykel J.
3
2017
SMTCoq: a plug-in for integrating SMT solvers into Coq. Zbl 1494.68285
Ekici, Burak; Mebsout, Alain; Tinelli, Cesare; Keller, Chantal; Katz, Guy; Reynolds, Andrew; Barrett, Clark
3
2017
Proofs in satisfiability modulo theories. Zbl 1431.68111
Barrett, Clark; de Moura, Leonardo; Fontaine, Pascal
2
2015
Towards bit-width-independent proofs in SMT solvers. Zbl 07178987
Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Zohar, Yoni; Barrett, Clark; Tinelli, Cesare
2
2019
Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006). Zbl 1129.68498
Barrett, Clark; de Moura, Leonardo; Stump, Aaron
2
2007
On solving quantified bit-vector constraints using invertibility conditions. Zbl 07388006
Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare
2
2021
Witness runs for counter machines. Zbl 1397.68122
Barrett, Clark; Demri, Stéphane; Deters, Morgan
2
2013
Scaling up DPLL(T) string solvers using context-dependent simplification. Zbl 1494.68255
Reynolds, Andrew; Woo, Maverick; Barrett, Clark; Brumley, David; Liang, Tianyi; Tinelli, Cesare
2
2017
Translation and run-time validation of loop transformations. Zbl 1083.68555
Zuck, Lenore; Pnueli, Amir; Goldberg, Benjamin; Barrett, Clark; Fang, Yi; Hu, Ying
1
2005
Pointer analysis, conditional soundness, and proving the absence of errors. Zbl 1149.68348
Conway, Christopher L.; Dams, Dennis; Namjoshi, Kedar S.; Barrett, Clark
1
2008
Combining SAT methods with non-clausal decision heuristics. Zbl 1272.68370
Barrett, Clark; Donham, Jacob
1
2005
Being careful about theory combination. Zbl 1284.68518
Jovanović, Dejan; Barrett, Clark
1
2013
Politeness and stable infiniteness: stronger together. Zbl 07437077
Sheng, Ying; Zohar, Yoni; Ringeissen, Christophe; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare
1
2021
Counterexample-guided prophecy for model checking modulo the theory of arrays. Zbl 1467.68089
Mann, Makai; Irfan, Ahmed; Griggio, Alberto; Padon, Oded; Barrett, Clark
4
2021
An SMT-based approach for verifying binarized neural networks. Zbl 1474.68188
Amir, Guy; Wu, Haoze; Barrett, Clark; Katz, Guy
3
2021
On solving quantified bit-vector constraints using invertibility conditions. Zbl 07388006
Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare
2
2021
Politeness and stable infiniteness: stronger together. Zbl 07437077
Sheng, Ying; Zohar, Yoni; Ringeissen, Christophe; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare
1
2021
Extending SMT solvers to higher-order logic. Zbl 07178968
Barbosa, Haniel; Reynolds, Andrew; El Ouraoui, Daniel; Tinelli, Cesare; Barrett, Clark
10
2019
Syntax-guided rewrite rule enumeration for SMT solvers. Zbl 1441.68233
Nötzli, Andres; Reynolds, Andrew; Barbosa, Haniel; Niemetz, Aina; Preiner, Mathias; Barrett, Clark; Tinelli, Cesare
4
2019
Refutation-based synthesis in SMT. Zbl 1427.68051
Reynolds, Andrew; Kuncak, Viktor; Tinelli, Cesare; Barrett, Clark; Deters, Morgan
3
2019
DRAT-based bit-vector proofs in CVC4. Zbl 1441.68235
Ozdemir, Alex; Niemetz, Aina; Preiner, Mathias; Zohar, Yoni; Barrett, Clark
3
2019
Towards bit-width-independent proofs in SMT solvers. Zbl 07178987
Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Zohar, Yoni; Barrett, Clark; Tinelli, Cesare
2
2019
Satisfiability modulo theories. Zbl 1392.68379
Barrett, Clark; Tinelli, Cesare
29
2018
Datatypes with shared selectors. Zbl 06958125
Reynolds, Andrew; Viswanathan, Arjun; Barbosa, Haniel; Tinelli, Cesare; Barrett, Clark
3
2018
Designing theory solvers with extensions. Zbl 1495.68239
Reynolds, Andrew; Tinelli, Cesare; Jovanović, Dejan; Barrett, Clark
5
2017
Relational constraint solving in SMT. Zbl 1494.68289
Meng, Baoluo; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark
3
2017
Reluplex: an efficient SMT solver for verifying deep neural networks. Zbl 1494.68167
Katz, Guy; Barrett, Clark; Dill, David L.; Julian, Kyle; Kochenderfer, Mykel J.
3
2017
SMTCoq: a plug-in for integrating SMT solvers into Coq. Zbl 1494.68285
Ekici, Burak; Mebsout, Alain; Tinelli, Cesare; Keller, Chantal; Katz, Guy; Reynolds, Andrew; Barrett, Clark
3
2017
Scaling up DPLL(T) string solvers using context-dependent simplification. Zbl 1494.68255
Reynolds, Andrew; Woo, Maverick; Barrett, Clark; Brumley, David; Liang, Tianyi; Tinelli, Cesare
2
2017
A new decision procedure for finite sets and cardinality constraints in SMT. Zbl 1475.68430
Bansal, Kshitij; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare
5
2016
An efficient SMT solver for string constraints. Zbl 1404.68135
Liang, Tianyi; Reynolds, Andrew; Tsiskaridze, Nestan; Tinelli, Cesare; Barrett, Clark; Deters, Morgan
3
2016
Counterexample-guided quantifier instantiation for synthesis in SMT. Zbl 1381.68059
Reynolds, Andrew; Deters, Morgan; Kuncak, Viktor; Tinelli, Cesare; Barrett, Clark
15
2015
A decision procedure for regular membership and length constraints over unbounded strings. Zbl 1471.68119
Liang, Tianyi; Tsiskaridze, Nestan; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark
6
2015
Deciding local theory extensions via E-matching. Zbl 1381.68280
Bansal, Kshitij; Reynolds, Andrew; King, Tim; Barrett, Clark; Wies, Thomas
5
2015
Fine grained SMT proofs for the theory of fixed-width bit-vectors. Zbl 1471.68143
Hadarean, Liana; Barrett, Clark; Reynolds, Andrew; Tinelli, Cesare; Deters, Morgan
4
2015
Proofs in satisfiability modulo theories. Zbl 1431.68111
Barrett, Clark; de Moura, Leonardo; Fontaine, Pascal
2
2015
Quantifier instantiation techniques for finite model finding in SMT. Zbl 1381.68275
Reynolds, Andrew; Tinelli, Cesare; Goel, Amit; Krstić, Sava; Deters, Morgan; Barrett, Clark
16
2013
Witness runs for counter machines. Zbl 1397.68122
Barrett, Clark; Demri, Stéphane; Deters, Morgan
2
2013
Being careful about theory combination. Zbl 1284.68518
Jovanović, Dejan; Barrett, Clark
1
2013
Sharing is caring: combination of theories. Zbl 1348.68220
Jovanović, Dejan; Barrett, Clark
5
2011
Polite theories revisited. Zbl 1306.68147
Jovanović, Dejan; Barrett, Clark
14
2010
Solving quantified verification conditions using satisfiability modulo theories. Zbl 1184.68461
Ge, Yeting; Barrett, Clark; Tinelli, Cesare
8
2009
Pointer analysis, conditional soundness, and proving the absence of errors. Zbl 1149.68348
Conway, Christopher L.; Dams, Dennis; Namjoshi, Kedar S.; Barrett, Clark
1
2008
Solving quantified verification conditions using satisfiability modulo theories. Zbl 1213.68376
Ge, Yeting; Barrett, Clark; Tinelli, Cesare
17
2007
An abstract decision procedure for a theory of inductive data types. Zbl 1129.68022
Barrett, Clack; Shikanian, Igor; Tinelli, Cesare
14
2007
An abstract decision procedure for satisfiability in the theory of recursive data types. Zbl 1277.68132
Barrett, Clark; Shikanian, Igor; Tinelli, Cesare
7
2007
Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006). Zbl 1129.68498
Barrett, Clark; de Moura, Leonardo; Stump, Aaron
2
2007
Splitting on demand in SAT modulo theories. Zbl 1165.68480
Barrett, Clark; Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare
24
2006
Cooperating theorem provers: a case study combining HOL-Light and CVC Lite. Zbl 1272.68362
Mclaughlin, Sean; Barrett, Clark; Ge, Yeting
12
2006
TVOC: A translation validator for optimizing compilers. Zbl 1081.68606
Barrett, Clark; Fang, Yi; Goldberg, Benjamin; Hu, Ying; Pnueli, Amir; Zuck, Lenore
9
2005
SMT-COMP: Satisfiability modulo theories competition. Zbl 1081.68607
Barrett, Clark; Moura, Leonardo; Stump, Aaron
8
2005
A practical approach to partial functions in CVC Lite. Zbl 1272.03136
Berezin, Sergey; Barrett, Clark; Shikanian, Igor; Chechik, Marsha; Gurfinkel, Arie; Dill, David L.
4
2005
Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005). Zbl 1104.68719
Barrett, Clark; de Moura, Leonardo; Stump, Aaron
3
2005
Translation and run-time validation of loop transformations. Zbl 1083.68555
Zuck, Lenore; Pnueli, Amir; Goldberg, Benjamin; Barrett, Clark; Fang, Yi; Hu, Ying
1
2005
Combining SAT methods with non-clausal decision heuristics. Zbl 1272.68370
Barrett, Clark; Donham, Jacob
1
2005
CVC Lite: A new implementation of the cooperating validity checker – Category B. Zbl 1103.68605
Barrett, Clark; Berezin, Sergey
22
2004
CVC: A cooperating validity checker. Zbl 1010.68720
Stump, Aaron; Barrett, Clark W.; Dill, David L.
19
2002
Checking satisfiability of first-order formulas by incremental translation to SAT. Zbl 1010.68531
Barrett, Clark W.; Dill, David L.; Stump, Aaron
18
2002
A generalization of Shostak’s method for combining decision procedures. Zbl 1057.68109
Barrett, Clark W.; Dill, David L.; Stump, Aaron
13
2002
A framework for cooperating decision procedures. Zbl 0963.68177
Barrett, Clark W.; Dill, David L.; Stump, Aaron
4
2000
all top 5

Cited by 477 Authors

30 Barrett, Clark W.
24 Tinelli, Cesare
23 Reynolds, Andrew
10 Blanchette, Jasmin Christian
10 Fontaine, Pascal
7 Bonacina, Maria Paola
7 Griggio, Alberto
7 Ringeissen, Christophe
7 Sebastiani, Roberto
7 Zohar, Yoni
6 Niemetz, Aina
6 Preiner, Mathias
6 Ranise, Silvio
5 Barbosa, Haniel
5 Bruttomesso, Roberto
5 Cimatti, Alessandro
5 Ghilardi, Silvio
5 Stump, Aaron
4 de Moura, Leonardo
4 Déharbe, David
4 Deters, Morgan
4 Echenim, Mnacho
4 Kremer, Gereon
4 Kröning, Daniel
4 Kuncak, Viktor
4 Mora, Federico
4 Sharygina, Natasha
4 Sheng, Ying
4 Strichman, Ofer
4 Tourret, Sophie
3 Ábrahám, Erika
3 Alberti, Francesco
3 Bansal, Kshitij
3 Bentkamp, Alexander
3 Berzish, Murphy
3 Böhme, Sascha
3 Bromberger, Martin
3 Conchon, Sylvain
3 Cruanes, Simon
3 Day, Joel D.
3 Demri, Stéphane P.
3 Fleury, Mathias
3 Ganesh, Vijay
3 Irfan, Ahmed
3 Jovanović, Dejan
3 Krstic, Sava A.
3 Kulczynski, Mitja
3 Manea, Florin
3 Nötzli, Andres
3 Nowotka, Dirk
3 Padon, Oded
3 Vukmirović, Petar
3 Weidenbach, Christoph
2 Biere, Armin
2 Bozzano, Marco
2 Chistikov, Dmitry V.
2 Chocron, Paula
2 Claessen, Koen
2 Cristiá, Maximiliano
2 Czerwiński, Wojciech
2 de Nivelle, Hans
2 De Oliveira, Diego Caminha B.
2 Giunchiglia, Enrico
2 Grégoire, Benjamin
2 Gu, Ming
2 Gupta, Ashutosh
2 Hofman, Piotr
2 Iosif, Radu
2 Janota, Mikoláš
2 Järvisalo, Matti
2 Johansen, Christian
2 Johansson, Moa
2 Johnson, Taylor T.
2 Junttila, Tommi A.
2 Lange, Jane
2 Liang, Tianyi
2 Lierler, Yuliya
2 Luteberget, Bjørnar
2 Mann, Makai
2 Maratea, Marco
2 Marques-Silva, João P.
2 Meier, Andreas
2 Meseguer Guaita, José
2 Nguyen, Huu Hai
2 Nummelin, Visa
2 Pagani, Elena
2 Paulson, Lawrence Charles
2 Pilipczuk, Michał
2 Pnueli, Amir
2 Rossi, Gianfranco
2 Schurr, Hans-Jörg
2 Shankar, Natarajan
2 Siegel, Stephen F.
2 Skeirik, Stephen
2 Solar-Lezama, Armando
2 Sorge, Volker
2 Steffen, Martin
2 Sturm, Thomas
2 Sutcliffe, Geoff
2 Tran, Duc-Khanh
...and 377 more Authors

Citations by Year