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

Co-Authors

1 single-authored
40 Tinelli, Cesare
33 Reynolds, Andrew
14 Zohar, Yoni
10 Dill, David L.
9 Niemetz, Aina
9 Preiner, Mathias
8 Stump, Aaron
7 Deters, Morgan
7 Katz, Guy
7 Nötzli, Andres
6 Barbosa, Haniel
6 Sheng, Ying
4 de Moura, Leonardo
4 Jovanović, Dejan
4 Mann, Makai
4 Ringeissen, Christophe
3 Bansal, Kshitij
3 Fontaine, Pascal
3 Ge, Yeting
3 Irfan, Ahmed
3 Julian, Kyle D.
3 Kochenderfer, Mykel J.
3 Liang, Tianyi
3 Shikanian, Igor
3 Viswanathan, Arjun
2 Berezin, Sergey
2 Demri, Stéphane P.
2 Ekici, Burak
2 Fang, Yi
2 Goldberg, Benjamin
2 Grieskamp, Wolfgang
2 Griggio, Alberto
2 Hu, Ying
2 Kremer, Gereon
2 Kuncak, Viktor
2 Lange, Jane
2 Ozdemir, Alex
2 Padon, Oded
2 Park, Junkil
2 Pnueli, Amir
2 Qadeer, Shaz
2 Toledo, Guilherme V.
2 Tsiskaridze, Nestan
2 Wies, Thomas
2 Wu, Haoze
2 Zuck, Lenore D.
1 Abate, Alessandro
1 Amir, Guy
1 Brain, Martin
1 Brown, Kristopher
1 Brumley, David
1 Chechik, Marsha
1 Conway, Christopher L.
1 Dams, Dennis René
1 David, Cristina
1 Donham, Jacob
1 Donovick, Caleb
1 El Ouraoui, Daniel
1 Goel, Amit
1 Gopinath, Divya
1 Guman, Allison
1 Gurfinkel, Arie
1 Hadarean, Liana
1 Jacoby, Yuval
1 Kahsai, Temesghen
1 Keller, Chantal
1 Kesseli, Pascal
1 King, Tim
1 Kröning, Daniel
1 Krstic, Sava A.
1 Lachnitt, Hanna
1 McLaughlin, Sean
1 Mebsout, Alain
1 Meng, Baoluo
1 Namjoshi, Kedar S.
1 Nieuwenhuis, Robert
1 Oliveras, Albert
1 Păsăreanu, Corina S.
1 Polgreen, Elizabeth
1 Strong, Christopher A.
1 Stuntz, Lindsey
1 Viteri, Scott
1 Wang, Wei
1 Wilson, Amalee
1 Woo, Maverick
1 Zeljić, Aleksandar

Publications by Year

Citations contained in zbMATH Open

59 Publications have been cited 532 times in 349 Documents Cited by Year
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.
76
2017
Satisfiability modulo theories. Zbl 1392.68379
Barrett, Clark; Tinelli, Cesare
39
2018
Splitting on demand in SAT modulo theories. Zbl 1165.68480
Barrett, Clark; Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare
29
2006
CVC Lite: A new implementation of the cooperating validity checker – Category B. Zbl 1103.68605
Barrett, Clark; Berezin, Sergey
25
2004
An abstract decision procedure for a theory of inductive data types. Zbl 1129.68022
Barrett, Clack; Shikanian, Igor; Tinelli, Cesare
20
2007
Solving quantified verification conditions using satisfiability modulo theories. Zbl 1213.68376
Ge, Yeting; Barrett, Clark; Tinelli, Cesare
20
2007
Polite theories revisited. Zbl 1306.68147
Jovanović, Dejan; Barrett, Clark
20
2010
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
Counterexample-guided quantifier instantiation for synthesis in SMT. Zbl 1381.68059
Reynolds, Andrew; Deters, Morgan; Kuncak, Viktor; Tinelli, Cesare; Barrett, Clark
16
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
A generalization of Shostak’s method for combining decision procedures. Zbl 1057.68109
Barrett, Clark W.; Dill, David L.; Stump, Aaron
14
2002
Cooperating theorem provers: a case study combining HOL-Light and CVC Lite. Zbl 1272.68362
Mclaughlin, Sean; Barrett, Clark; Ge, Yeting
14
2006
Extending SMT solvers to higher-order logic. Zbl 07178968
Barbosa, Haniel; Reynolds, Andrew; El Ouraoui, Daniel; Tinelli, Cesare; Barrett, Clark
12
2019
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
12
2017
TVOC: A translation validator for optimizing compilers. Zbl 1081.68606
Barrett, Clark; Fang, Yi; Goldberg, Benjamin; Hu, Ying; Pnueli, Amir; Zuck, Lenore
10
2005
SMT-COMP: Satisfiability modulo theories competition. Zbl 1081.68607
Barrett, Clark; Moura, Leonardo; Stump, Aaron
10
2005
Solving quantified verification conditions using satisfiability modulo theories. Zbl 1184.68461
Ge, Yeting; Barrett, Clark; Tinelli, Cesare
9
2009
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
9
2017
An efficient SMT solver for string constraints. Zbl 1404.68135
Liang, Tianyi; Reynolds, Andrew; Tsiskaridze, Nestan; Tinelli, Cesare; Barrett, Clark; Deters, Morgan
9
2016
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
7
2015
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.
6
2005
Solving quantified bit-vectors using invertibility conditions. Zbl 1511.68255
Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare
6
2018
DeepSafe: a data-driven approach for assessing robustness of neural networks. Zbl 1517.68342
Gopinath, Divya; Katz, Guy; Păsăreanu, Corina S.; Barrett, Clark
6
2018
Refutation-based synthesis in SMT. Zbl 1427.68051
Reynolds, Andrew; Kuncak, Viktor; Tinelli, Cesare; Barrett, Clark; Deters, Morgan
5
2019
Designing theory solvers with extensions. Zbl 1495.68239
Reynolds, Andrew; Tinelli, Cesare; Jovanović, Dejan; Barrett, Clark
5
2017
Deciding local theory extensions via E-matching. Zbl 1381.68280
Bansal, Kshitij; Reynolds, Andrew; King, Tim; Barrett, Clark; Wies, Thomas
5
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
Sharing is caring: combination of theories. Zbl 1348.68220
Jovanović, Dejan; Barrett, Clark
5
2011
Counterexample-guided prophecy for model checking modulo the theory of arrays. Zbl 1467.68089
Mann, Makai; Irfan, Ahmed; Griggio, Alberto; Padon, Oded; Barrett, Clark
5
2021
A framework for cooperating decision procedures. Zbl 0963.68177
Barrett, Clark W.; Dill, David L.; Stump, Aaron
4
2000
Datatypes with shared selectors. Zbl 1511.68175
Reynolds, Andrew; Viswanathan, Arjun; Barbosa, Haniel; Tinelli, Cesare; Barrett, Clark
4
2018
Towards bit-width-independent proofs in SMT solvers. Zbl 07178987
Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Zohar, Yoni; Barrett, Clark; Tinelli, Cesare
4
2019
Verifying recurrent neural networks using invariant inference. Zbl 1517.68241
Jacoby, Yuval; Barrett, Clark; Katz, Guy
4
2020
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
Politeness and stable infiniteness: stronger together. Zbl 07437077
Sheng, Ying; Zohar, Yoni; Ringeissen, Christophe; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare
4
2021
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
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
Proofs in satisfiability modulo theories. Zbl 1431.68111
Barrett, Clark; de Moura, Leonardo; Fontaine, Pascal
3
2015
DRAT-based bit-vector proofs in CVC4. Zbl 1441.68235
Ozdemir, Alex; Niemetz, Aina; Preiner, Mathias; Zohar, Yoni; Barrett, Clark
3
2019
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 1519.68236
Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare
3
2021
Politeness for the theory of algebraic datatypes. Zbl 07614516
Sheng, Ying; Zohar, Yoni; Ringeissen, Christophe; Lange, Jane; Fontaine, Pascal; Barrett, Clark
3
2020
Flexible proof production in an industrial-strength SMT solver. Zbl 07628179
Barbosa, Haniel; Reynolds, Andrew; Kremer, Gereon; Lachnitt, Hanna; Niemetz, Aina; Nötzli, Andres; Ozdemir, Alex; Preiner, Mathias; Viswanathan, Arjun; Viteri, Scott; Zohar, Yoni; Tinelli, Cesare; Barrett, Clark
3
2022
Relational constraint solving in SMT. Zbl 1494.68289
Meng, Baoluo; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark
3
2017
Reasoning with finite sets and cardinality constraints in SMT. Zbl 1403.68044
Bansal, Kshitij; Barrett, Clark; Reynolds, Andrew; Tinelli, Cesare
2
2018
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
Towards satisfiability modulo parametric bit-vectors. Zbl 07433026
Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Zohar, Yoni; Barrett, Clark; Tinelli, Cesare
2
2021
Witness runs for counter machines. Zbl 1397.68122
Barrett, Clark; Demri, Stéphane; Deters, Morgan
2
2013
Reluplex: a calculus for reasoning about deep neural networks. Zbl 1522.68328
Katz, Guy; Barrett, Clark; Dill, David L.; Julian, Kyle; Kochenderfer, Mykel J.
2
2022
Even faster conflicts and lazier reductions for string solvers. Zbl 1514.68274
Nötzli, Andres; Reynolds, Andrew; Barbosa, Haniel; Barrett, Clark; Tinelli, Cesare
2
2022
Reasoning about vectors using an SMT theory of sequences. Zbl 07628185
Sheng, Ying; Nötzli, Andres; Reynolds, Andrew; Zohar, Yoni; Dill, David; Grieskamp, Wolfgang; Park, Junkil; Qadeer, Shaz; Barrett, Clark; Tinelli, Cesare
2
2022
High-level abstractions for simplifying extended string constraints in SMT. Zbl 07805814
Reynolds, Andrew; Nötzli, Andres; Barrett, Clark; Tinelli, Cesare
2
2019
Being careful about theory combination. Zbl 1284.68518
Jovanović, Dejan; Barrett, Clark
1
2013
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
Polite combination of algebraic datatypes. Zbl 07606342
Sheng, Ying; Zohar, Yoni; Ringeissen, Christophe; Lange, Jane; Fontaine, Pascal; Barrett, Clark
1
2022
Combining SAT methods with non-clausal decision heuristics. Zbl 1272.68370
Barrett, Clark; Donham, Jacob
1
2005
Flexible proof production in an industrial-strength SMT solver. Zbl 07628179
Barbosa, Haniel; Reynolds, Andrew; Kremer, Gereon; Lachnitt, Hanna; Niemetz, Aina; Nötzli, Andres; Ozdemir, Alex; Preiner, Mathias; Viswanathan, Arjun; Viteri, Scott; Zohar, Yoni; Tinelli, Cesare; Barrett, Clark
3
2022
Reluplex: a calculus for reasoning about deep neural networks. Zbl 1522.68328
Katz, Guy; Barrett, Clark; Dill, David L.; Julian, Kyle; Kochenderfer, Mykel J.
2
2022
Even faster conflicts and lazier reductions for string solvers. Zbl 1514.68274
Nötzli, Andres; Reynolds, Andrew; Barbosa, Haniel; Barrett, Clark; Tinelli, Cesare
2
2022
Reasoning about vectors using an SMT theory of sequences. Zbl 07628185
Sheng, Ying; Nötzli, Andres; Reynolds, Andrew; Zohar, Yoni; Dill, David; Grieskamp, Wolfgang; Park, Junkil; Qadeer, Shaz; Barrett, Clark; Tinelli, Cesare
2
2022
Polite combination of algebraic datatypes. Zbl 07606342
Sheng, Ying; Zohar, Yoni; Ringeissen, Christophe; Lange, Jane; Fontaine, Pascal; Barrett, Clark
1
2022
Counterexample-guided prophecy for model checking modulo the theory of arrays. Zbl 1467.68089
Mann, Makai; Irfan, Ahmed; Griggio, Alberto; Padon, Oded; Barrett, Clark
5
2021
Politeness and stable infiniteness: stronger together. Zbl 07437077
Sheng, Ying; Zohar, Yoni; Ringeissen, Christophe; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare
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 1519.68236
Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare
3
2021
Towards satisfiability modulo parametric bit-vectors. Zbl 07433026
Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Zohar, Yoni; Barrett, Clark; Tinelli, Cesare
2
2021
Verifying recurrent neural networks using invariant inference. Zbl 1517.68241
Jacoby, Yuval; Barrett, Clark; Katz, Guy
4
2020
Politeness for the theory of algebraic datatypes. Zbl 07614516
Sheng, Ying; Zohar, Yoni; Ringeissen, Christophe; Lange, Jane; Fontaine, Pascal; Barrett, Clark
3
2020
Extending SMT solvers to higher-order logic. Zbl 07178968
Barbosa, Haniel; Reynolds, Andrew; El Ouraoui, Daniel; Tinelli, Cesare; Barrett, Clark
12
2019
Refutation-based synthesis in SMT. Zbl 1427.68051
Reynolds, Andrew; Kuncak, Viktor; Tinelli, Cesare; Barrett, Clark; Deters, Morgan
5
2019
Towards bit-width-independent proofs in SMT solvers. Zbl 07178987
Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Zohar, Yoni; Barrett, Clark; Tinelli, Cesare
4
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
DRAT-based bit-vector proofs in CVC4. Zbl 1441.68235
Ozdemir, Alex; Niemetz, Aina; Preiner, Mathias; Zohar, Yoni; Barrett, Clark
3
2019
High-level abstractions for simplifying extended string constraints in SMT. Zbl 07805814
Reynolds, Andrew; Nötzli, Andres; Barrett, Clark; Tinelli, Cesare
2
2019
Satisfiability modulo theories. Zbl 1392.68379
Barrett, Clark; Tinelli, Cesare
39
2018
Solving quantified bit-vectors using invertibility conditions. Zbl 1511.68255
Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare
6
2018
DeepSafe: a data-driven approach for assessing robustness of neural networks. Zbl 1517.68342
Gopinath, Divya; Katz, Guy; Păsăreanu, Corina S.; Barrett, Clark
6
2018
Datatypes with shared selectors. Zbl 1511.68175
Reynolds, Andrew; Viswanathan, Arjun; Barbosa, Haniel; Tinelli, Cesare; Barrett, Clark
4
2018
Reasoning with finite sets and cardinality constraints in SMT. Zbl 1403.68044
Bansal, Kshitij; Barrett, Clark; Reynolds, Andrew; Tinelli, Cesare
2
2018
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.
76
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
12
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
9
2017
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
An efficient SMT solver for string constraints. Zbl 1404.68135
Liang, Tianyi; Reynolds, Andrew; Tsiskaridze, Nestan; Tinelli, Cesare; Barrett, Clark; Deters, Morgan
9
2016
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
Counterexample-guided quantifier instantiation for synthesis in SMT. Zbl 1381.68059
Reynolds, Andrew; Deters, Morgan; Kuncak, Viktor; Tinelli, Cesare; Barrett, Clark
16
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
7
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
3
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
20
2010
Solving quantified verification conditions using satisfiability modulo theories. Zbl 1184.68461
Ge, Yeting; Barrett, Clark; Tinelli, Cesare
9
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
An abstract decision procedure for a theory of inductive data types. Zbl 1129.68022
Barrett, Clack; Shikanian, Igor; Tinelli, Cesare
20
2007
Solving quantified verification conditions using satisfiability modulo theories. Zbl 1213.68376
Ge, Yeting; Barrett, Clark; Tinelli, Cesare
20
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
29
2006
Cooperating theorem provers: a case study combining HOL-Light and CVC Lite. Zbl 1272.68362
Mclaughlin, Sean; Barrett, Clark; Ge, Yeting
14
2006
TVOC: A translation validator for optimizing compilers. Zbl 1081.68606
Barrett, Clark; Fang, Yi; Goldberg, Benjamin; Hu, Ying; Pnueli, Amir; Zuck, Lenore
10
2005
SMT-COMP: Satisfiability modulo theories competition. Zbl 1081.68607
Barrett, Clark; Moura, Leonardo; Stump, Aaron
10
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.
6
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
25
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
14
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 738 Authors

39 Barrett, Clark W.
29 Tinelli, Cesare
27 Reynolds, Andrew
12 Zohar, Yoni
11 Blanchette, Jasmin Christian
11 Fontaine, Pascal
9 Bonacina, Maria Paola
9 Ringeissen, Christophe
8 Griggio, Alberto
7 Barbosa, Haniel
7 Sebastiani, Roberto
6 Cimatti, Alessandro
6 Kröning, Daniel
6 Niemetz, Aina
6 Preiner, Mathias
6 Ranise, Silvio
6 Sheng, Ying
6 Tran, Hoang-Dung
5 Bruttomesso, Roberto
5 de Moura, Leonardo
5 Ghilardi, Silvio
5 Johnson, Taylor T.
5 Kuncak, Viktor
5 Nötzli, Andres
5 Stump, Aaron
5 Yang, Xiaodong
4 Ábrahám, Erika
4 Déharbe, David
4 Deters, Morgan
4 Echenim, Mnacho
4 Hoxha, Bardh
4 Jovanović, Dejan
4 Katz, Guy
4 Kremer, Gereon
4 Kulczynski, Mitja
4 Mora, Federico
4 Nowotka, Dirk
4 Prokhorov, Danil V.
4 Sharygina, Natasha
4 Strichman, Ofer
4 Tourret, Sophie
3 Alberti, Francesco
3 Alur, Rajeev
3 Bak, Stanley
3 Bansal, Kshitij
3 Bentkamp, Alexander
3 Berzish, Murphy
3 Böhme, Sascha
3 Bromberger, Martin
3 Chen, Taolue
3 Chocron, Paula
3 Conchon, Sylvain
3 Cristiá, Maximiliano
3 Cruanes, Simon
3 Day, Joel D.
3 Demri, Stéphane P.
3 Dill, David L.
3 Fleury, Mathias
3 Ganesh, Vijay
3 Graham-Lengrand, Stéphane
3 Holík, Lukáš
3 Huang, Xiaowei
3 Iosif, Radu
3 Irfan, Ahmed
3 Ivanov, Radoslav
3 Janota, Mikoláš
3 Julian, Kyle D.
3 Kochenderfer, Mykel J.
3 Kovács, Laura Ildikó
3 Krstic, Sava A.
3 Manea, Florin
3 Manzanas Lopez, Diego
3 Musau, Patrick
3 Nummelin, Visa
3 Padon, Oded
3 Rinard, Martin C.
3 Rossi, Gianfranco
3 Ruan, Wenjie
3 Vukmirović, Petar
3 Weber, Tjark
3 Weidenbach, Christoph
3 Wies, Thomas
2 Abdulla, Parosh Aziz
2 Aref, Mohammad Reza
2 Atig, Mohamed Faouzi
2 Azimi, Seyyed Arash
2 Biere, Armin
2 Bozga, Marius
2 Bozzano, Marco
2 Cai, Shaowei
2 Chen, Guangke
2 Chen, Xin
2 Chen, Yu-Fang
2 Chistikov, Dmitry V.
2 Chockler, Hana
2 Choi, Sungwoo
2 Czerwiński, Wojciech
2 David, Cristina
2 De Angelis, Emanuele
2 de Nivelle, Hans
...and 638 more Authors

Citations by Year