×
Compute Distance To:
Author ID: tinelli.cesare Recent zbMATH articles by "Tinelli, Cesare"
Published as: Tinelli, Cesare; Tinelli, C.
External Links: MGP · ORCID · dblp

Publications by Year

Citations contained in zbMATH Open

57 Publications have been cited 613 times in 380 Documents Cited by Year
Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\). Zbl 1326.68164
Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare
141
2006
DPLL(\(T\)): Fast decision procedures. Zbl 1103.68616
Ganzinger, Harald; Hagen, George; Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare
43
2004
A new correctness proof of the Nelson-Oppen combination procedure. Zbl 0893.03001
Tinelli, Cesare; Harandi, Mehdi
30
1996
Unions of non-disjoint theories and combinations of satisfiability procedures. Zbl 1018.68033
Tinelli, Cesare; Ringeissen, Christophe
26
2003
Satisfiability modulo theories. Zbl 1392.68379
Barrett, Clark; Tinelli, Cesare
23
2018
Splitting on demand in SAT modulo theories. Zbl 1165.68480
Barrett, Clark; Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare
22
2006
Combining nonstably infinite theories. Zbl 1108.03014
Tinelli, Cesare; Zarba, Calogero G.
18
2005
The model evolution calculus. Zbl 1278.68249
Baumgartner, Peter; Tinelli, Cesare
18
2003
Solving quantified verification conditions using satisfiability modulo theories. Zbl 1213.68376
Ge, Yeting; Barrett, Clark; Tinelli, Cesare
17
2007
The model evolution calculus as a first-order DPLL method. Zbl 1182.03034
Baumgartner, Peter; Tinelli, Cesare
15
2008
Combining decision procedures for sorted theories. Zbl 1111.68691
Tinelli, Cesare; Zarba, Calogero G.
14
2004
Quantifier instantiation techniques for finite model finding in SMT. Zbl 1381.68275
Reynolds, Andrew; Tinelli, Cesare; Goel, Amit; Krstić, Sava; Deters, Morgan; Barrett, Clark
14
2013
Counterexample-guided quantifier instantiation for synthesis in SMT. Zbl 1381.68059
Reynolds, Andrew; Deters, Morgan; Kuncak, Viktor; Tinelli, Cesare; Barrett, Clark
13
2015
The model evolution calculus with equality. Zbl 1135.03325
Baumgartner, Peter; Tinelli, Cesare
12
2005
An abstract decision procedure for a theory of inductive data types. Zbl 1129.68022
Barrett, Clack; Shikanian, Igor; Tinelli, Cesare
11
2007
Lemma learning in the model evolution calculus. Zbl 1165.03308
Baumgartner, Peter; Fuchs, Alexander; Tinelli, Cesare
11
2006
Ground interpolation for the theory of equality. Zbl 1234.68257
Fuchs, Alexander; Goel, Amit; Grundy, Jim; Krstić, Sava; Tinelli, Cesare
11
2009
Ground interpolation for combined theories. Zbl 1250.68188
Goel, Amit; Krstić, Sava; Tinelli, Cesare
10
2009
Cooperation of background reasoners in theory reasoning by residue sharing. Zbl 1019.03004
Tinelli, Cesare
10
2003
Abstract DPLL and abstract DPLL modulo theories. Zbl 1109.68097
Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare
10
2005
Computing finite models by reduction to function-free clause logic. Zbl 1171.68040
Baumgartner, Peter; Fuchs, Alexander; de Nivelle, Hans; Tinelli, Cesare
9
2009
Deciding the word problem in the union of equational theories. Zbl 1049.03032
Baader, Franz; Tinelli, Cesare
9
2002
SMT proof checking using a logical framework. Zbl 1284.68521
Stump, Aaron; Oe, Duckki; Reynolds, Andrew; Hadarean, Liana; Tinelli, Cesare
7
2013
Solving quantified verification conditions using satisfiability modulo theories. Zbl 1184.68461
Ge, Yeting; Barrett, Clark; Tinelli, Cesare
7
2009
Combined satisfiability modulo parametric theories. Zbl 1186.68297
Krstić, Sava; Goel, Amit; Grundy, Jim; Tinelli, Cesare
7
2007
\(\mathcal {ME}\)(LIA) – model evolution with linear integer arithmetic constraints. Zbl 1182.03033
Baumgartner, Peter; Fuchs, Alexander; Tinelli, Cesare
7
2008
Extending SMT solvers to higher-order logic. Zbl 07178968
Barbosa, Haniel; Reynolds, Andrew; El Ouraoui, Daniel; Tinelli, Cesare; Barrett, Clark
7
2019
A DPLL-based calculus for ground satisfiability modulo theories. Zbl 1013.68192
Tinelli, Cesare
6
2002
Combining non-stably infinite theories. Zbl 1261.03069
Tinelli, Cesare; Zarba, Calogero G.
6
2003
An abstract decision procedure for satisfiability in the theory of recursive data types. Zbl 1277.68132
Barrett, Clark; Shikanian, Igor; Tinelli, Cesare
6
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
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
Model evolution with equality – revised and implemented. Zbl 1258.03020
Baumgartner, Peter; Pelzer, Björn; Tinelli, Cesare
5
2012
A new combination procedure for the word problem that generalizes fusion decidability results in modal logics. Zbl 1098.03048
Baader, Franz; Ghilardi, Silvio; Tinelli, Cesare
5
2006
Deciding the word problem in the union of equational theories sharing constructors. Zbl 0976.03051
Baader, Franz; Tinelli, Cesare
4
1999
Designing theory solvers with extensions. Zbl 06821625
Reynolds, Andrew; Tinelli, Cesare; Jovanović, Dejan; Barrett, Clark
4
2017
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
3
2019
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
3
2015
Model finding for recursive functions in SMT. Zbl 1475.68448
Reynolds, Andrew; Blanchette, Jasmin Christian; Cruanes, Simon; Tinelli, Cesare
3
2016
Tools and algorithms for the construction and analysis of systems. 21st international conference, TACAS 2015, held as part of the European joint conferences on theory and practice of software, ETAPS 2015, London, UK, April 11–18, 2015. Proceedings. Zbl 1360.68006
3
2015
An efficient SMT solver for string constraints. Zbl 1404.68135
Liang, Tianyi; Reynolds, Andrew; Tsiskaridze, Nestan; Tinelli, Cesare; Barrett, Clark; Deters, Morgan
3
2016
Model evolution with equality modulo built-in theories. Zbl 1341.68180
Baumgartner, Peter; Tinelli, Cesare
3
2011
Combining decision procedures for positive theories sharing constructors. Zbl 1045.03013
Baader, Franz; Tinelli, Cesare
3
2002
Refutation-based synthesis in SMT. Zbl 1427.68051
Reynolds, Andrew; Kuncak, Viktor; Tinelli, Cesare; Barrett, Clark; Deters, Morgan
3
2019
Ground interpolation for the theory of equality. Zbl 1239.03022
Fuchs, Alexander; Goel, Amit; Grundy, Jim; Krstić, Sava; Tinelli, Cesare
2
2012
A new combination procedure for the word problem that generalizes fusion decidability results in modal logics. Zbl 1126.03302
Baader, Franz; Ghilardi, Silvio; Tinelli, Cesare
2
2004
Relational constraint solving in SMT. Zbl 06778402
Meng, Baoluo; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark
2
2017
Theory combination: beyond equality sharing. Zbl 1443.68116
Bonacina, Maria Paola; Fontaine, Pascal; Ringeissen, Christophe; Tinelli, Cesare
2
2019
SMTCoq: a plug-in for integrating SMT solvers into Coq. Zbl 07571373
Ekici, Burak; Mebsout, Alain; Tinelli, Cesare; Keller, Chantal; Katz, Guy; Reynolds, Andrew; Barrett, Clark
2
2017
On solving quantified bit-vector constraints using invertibility conditions. Zbl 07388006
Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare
2
2021
Towards bit-width-independent proofs in SMT solvers. Zbl 07178987
Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Zohar, Yoni; Barrett, Clark; Tinelli, Cesare
2
2019
Editorial: Symbolic computation and satisfiability checking. Zbl 1444.68006
2
2020
Datatypes with shared selectors. Zbl 06958125
Reynolds, Andrew; Viswanathan, Arjun; Barbosa, Haniel; Tinelli, Cesare; Barrett, Clark
1
2018
Combining equational theories sharing non-collapse-free constructors. Zbl 0962.03037
Baader, Franz; Tinelli, Cesare
1
2000
Description logic, theory combination, and all that. Essays dedicated to Franz Baader on the occasion of his 60th birthday. Zbl 1428.68036
1
2019
Constraint logic programming over unions of constraint theories. Zbl 0924.68050
Tinelli, Cesare; Harandi, Mehdi T.
1
1998
Selected papers from the workshops on disproving and the second international workshop on pragmatics of decision procedures (PDPAR 2004), Cork, Ireland, 2004. Zbl 1271.68015
1
2005
On solving quantified bit-vector constraints using invertibility conditions. Zbl 07388006
Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare
2
2021
Editorial: Symbolic computation and satisfiability checking. Zbl 1444.68006
2
2020
Extending SMT solvers to higher-order logic. Zbl 07178968
Barbosa, Haniel; Reynolds, Andrew; El Ouraoui, Daniel; Tinelli, Cesare; Barrett, Clark
7
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
3
2019
Refutation-based synthesis in SMT. Zbl 1427.68051
Reynolds, Andrew; Kuncak, Viktor; Tinelli, Cesare; Barrett, Clark; Deters, Morgan
3
2019
Theory combination: beyond equality sharing. Zbl 1443.68116
Bonacina, Maria Paola; Fontaine, Pascal; Ringeissen, Christophe; Tinelli, Cesare
2
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
Description logic, theory combination, and all that. Essays dedicated to Franz Baader on the occasion of his 60th birthday. Zbl 1428.68036
1
2019
Satisfiability modulo theories. Zbl 1392.68379
Barrett, Clark; Tinelli, Cesare
23
2018
Datatypes with shared selectors. Zbl 06958125
Reynolds, Andrew; Viswanathan, Arjun; Barbosa, Haniel; Tinelli, Cesare; Barrett, Clark
1
2018
Designing theory solvers with extensions. Zbl 06821625
Reynolds, Andrew; Tinelli, Cesare; Jovanović, Dejan; Barrett, Clark
4
2017
Relational constraint solving in SMT. Zbl 06778402
Meng, Baoluo; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark
2
2017
SMTCoq: a plug-in for integrating SMT solvers into Coq. Zbl 07571373
Ekici, Burak; Mebsout, Alain; Tinelli, Cesare; Keller, Chantal; Katz, Guy; Reynolds, Andrew; Barrett, Clark
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
Model finding for recursive functions in SMT. Zbl 1475.68448
Reynolds, Andrew; Blanchette, Jasmin Christian; Cruanes, Simon; Tinelli, Cesare
3
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
13
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
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
3
2015
Tools and algorithms for the construction and analysis of systems. 21st international conference, TACAS 2015, held as part of the European joint conferences on theory and practice of software, ETAPS 2015, London, UK, April 11–18, 2015. Proceedings. Zbl 1360.68006
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
14
2013
SMT proof checking using a logical framework. Zbl 1284.68521
Stump, Aaron; Oe, Duckki; Reynolds, Andrew; Hadarean, Liana; Tinelli, Cesare
7
2013
Model evolution with equality – revised and implemented. Zbl 1258.03020
Baumgartner, Peter; Pelzer, Björn; Tinelli, Cesare
5
2012
Ground interpolation for the theory of equality. Zbl 1239.03022
Fuchs, Alexander; Goel, Amit; Grundy, Jim; Krstić, Sava; Tinelli, Cesare
2
2012
Model evolution with equality modulo built-in theories. Zbl 1341.68180
Baumgartner, Peter; Tinelli, Cesare
3
2011
Ground interpolation for the theory of equality. Zbl 1234.68257
Fuchs, Alexander; Goel, Amit; Grundy, Jim; Krstić, Sava; Tinelli, Cesare
11
2009
Ground interpolation for combined theories. Zbl 1250.68188
Goel, Amit; Krstić, Sava; Tinelli, Cesare
10
2009
Computing finite models by reduction to function-free clause logic. Zbl 1171.68040
Baumgartner, Peter; Fuchs, Alexander; de Nivelle, Hans; Tinelli, Cesare
9
2009
Solving quantified verification conditions using satisfiability modulo theories. Zbl 1184.68461
Ge, Yeting; Barrett, Clark; Tinelli, Cesare
7
2009
The model evolution calculus as a first-order DPLL method. Zbl 1182.03034
Baumgartner, Peter; Tinelli, Cesare
15
2008
\(\mathcal {ME}\)(LIA) – model evolution with linear integer arithmetic constraints. Zbl 1182.03033
Baumgartner, Peter; Fuchs, Alexander; Tinelli, Cesare
7
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
11
2007
Combined satisfiability modulo parametric theories. Zbl 1186.68297
Krstić, Sava; Goel, Amit; Grundy, Jim; Tinelli, Cesare
7
2007
An abstract decision procedure for satisfiability in the theory of recursive data types. Zbl 1277.68132
Barrett, Clark; Shikanian, Igor; Tinelli, Cesare
6
2007
Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\). Zbl 1326.68164
Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare
141
2006
Splitting on demand in SAT modulo theories. Zbl 1165.68480
Barrett, Clark; Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare
22
2006
Lemma learning in the model evolution calculus. Zbl 1165.03308
Baumgartner, Peter; Fuchs, Alexander; Tinelli, Cesare
11
2006
A new combination procedure for the word problem that generalizes fusion decidability results in modal logics. Zbl 1098.03048
Baader, Franz; Ghilardi, Silvio; Tinelli, Cesare
5
2006
Combining nonstably infinite theories. Zbl 1108.03014
Tinelli, Cesare; Zarba, Calogero G.
18
2005
The model evolution calculus with equality. Zbl 1135.03325
Baumgartner, Peter; Tinelli, Cesare
12
2005
Abstract DPLL and abstract DPLL modulo theories. Zbl 1109.68097
Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare
10
2005
Selected papers from the workshops on disproving and the second international workshop on pragmatics of decision procedures (PDPAR 2004), Cork, Ireland, 2004. Zbl 1271.68015
1
2005
DPLL(\(T\)): Fast decision procedures. Zbl 1103.68616
Ganzinger, Harald; Hagen, George; Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare
43
2004
Combining decision procedures for sorted theories. Zbl 1111.68691
Tinelli, Cesare; Zarba, Calogero G.
14
2004
A new combination procedure for the word problem that generalizes fusion decidability results in modal logics. Zbl 1126.03302
Baader, Franz; Ghilardi, Silvio; Tinelli, Cesare
2
2004
Unions of non-disjoint theories and combinations of satisfiability procedures. Zbl 1018.68033
Tinelli, Cesare; Ringeissen, Christophe
26
2003
The model evolution calculus. Zbl 1278.68249
Baumgartner, Peter; Tinelli, Cesare
18
2003
Cooperation of background reasoners in theory reasoning by residue sharing. Zbl 1019.03004
Tinelli, Cesare
10
2003
Combining non-stably infinite theories. Zbl 1261.03069
Tinelli, Cesare; Zarba, Calogero G.
6
2003
Deciding the word problem in the union of equational theories. Zbl 1049.03032
Baader, Franz; Tinelli, Cesare
9
2002
A DPLL-based calculus for ground satisfiability modulo theories. Zbl 1013.68192
Tinelli, Cesare
6
2002
Combining decision procedures for positive theories sharing constructors. Zbl 1045.03013
Baader, Franz; Tinelli, Cesare
3
2002
Combining equational theories sharing non-collapse-free constructors. Zbl 0962.03037
Baader, Franz; Tinelli, Cesare
1
2000
Deciding the word problem in the union of equational theories sharing constructors. Zbl 0976.03051
Baader, Franz; Tinelli, Cesare
4
1999
Constraint logic programming over unions of constraint theories. Zbl 0924.68050
Tinelli, Cesare; Harandi, Mehdi T.
1
1998
A new correctness proof of the Nelson-Oppen combination procedure. Zbl 0893.03001
Tinelli, Cesare; Harandi, Mehdi
30
1996
all top 5

Cited by 659 Authors

29 Tinelli, Cesare
21 Barrett, Clark W.
19 Reynolds, Andrew
19 Weidenbach, Christoph
16 Ghilardi, Silvio
12 Blanchette, Jasmin Christian
12 Bonacina, Maria Paola
12 Fontaine, Pascal
10 Ranise, Silvio
10 Sebastiani, Roberto
9 de Moura, Leonardo
9 Ringeissen, Christophe
8 Lierler, Yuliya
7 Baumgartner, Peter
7 Bruttomesso, Roberto
7 Meseguer Guaita, José
7 Waldmann, Uwe
6 Baader, Franz
6 Fleury, Mathias
6 Ganesh, Vijay
6 Griggio, Alberto
6 Nieuwenhuis, Robert
5 Bromberger, Martin
5 Cimatti, Alessandro
5 Echenim, Mnacho
5 Jovanović, Dejan
5 Kuncak, Viktor
5 Niemetz, Aina
5 Preiner, Mathias
5 Sharygina, Natasha
5 Sofronie-Stokkermans, Viorica
5 Sturm, Thomas
4 Bright, Curtis
4 Déharbe, David
4 Deters, Morgan
4 Dodaro, Carmine
4 Gianola, Alessandro
4 Kotsireas, Ilias S.
4 Kröning, Daniel
4 Krstic, Sava A.
4 Plaisted, David Alan
4 Rümmer, Philipp
4 Schaub, Torsten H.
4 Stuckey, Peter James
4 Tourret, Sophie
4 Tran, Duc-Khanh
4 Zarba, Calogero G.
4 Zhou, Min
3 Ábrahám, Erika
3 Alberti, Francesco
3 Bansal, Kshitij
3 Barbosa, Haniel
3 Bentkamp, Alexander
3 Bjørner, Nikolaj S.
3 Calvanese, Diego
3 Chocron, Paula
3 Conchon, Sylvain
3 de Cat, Broes
3 Eggers, Andreas
3 Gebser, Martin
3 Graham-Lengrand, Stéphane
3 He, Fei
3 Hoenicke, Jochen
3 Johansson, Moa
3 Korovin, Konstantin
3 Lynch, Christopher A.
3 Maratea, Marco
3 Montali, Marco
3 Mora, Federico
3 Oliveras, Albert
3 Rivkin, Andrey
3 Schmidt, Renate A.
3 Shankar, Natarajan
3 Song, Xiaoyu
3 Stump, Aaron
3 Sun, Jiaguang
3 Voronkov, Andrei
3 Vukmirović, Petar
3 Wang, Bow-Yaw
3 You, Jia-Huai
3 Zhang, Yan
3 Zohar, Yoni
2 Alviano, Mario
2 Areces, Carlos
2 Banković, Milan
2 Berzish, Murphy
2 Biere, Armin
2 Binh, Nguyen Thanh
2 Bodirsky, Manuel
2 Bofill, Miquel
2 Böhme, Sascha
2 Borgwardt, Stefan
2 Bozzano, Marco
2 Bruynooghe, Maurice
2 Chihani, Zakaria
2 Christ, Jürgen
2 Claessen, Koen
2 Cristiá, Maximiliano
2 Cruanes, Simon
2 Day, Joel D.
...and 559 more Authors

Citations by Year