×

zbMATH — the first resource for mathematics

Bruttomesso, Roberto

Compute Distance To:
Author ID: bruttomesso.roberto Recent zbMATH articles by "Bruttomesso, Roberto"
Published as: Bruttomesso, Roberto
Documents Indexed: 18 Publications since 2005

Publications by Year

Citations contained in zbMATH Open

18 Publications have been cited 106 times in 66 Documents Cited by Year
Efficient theory combination via Boolean search. Zbl 1137.68578
Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Junttila, Tommi; Ranise, Silvio; Van Rossum, Peter; Sebastiani, Roberto
14
2006
An incremental and layered procedure for the satisfiability of linear arithmetic logic. Zbl 1087.68630
Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Junttila, Tommi; van Rossum, Peter; Schulz, Stephan; Sebastiani, Roberto
9
2005
Lazy abstraction with interpolants for arrays. Zbl 1352.68141
Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha
9
2012
Rewriting-based quantifier-free interpolation for a theory of arrays. Zbl 1236.68179
Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio
7
2011
Quantifier-free interpolation in combinations of equality interpolating theories. Zbl 1287.03068
Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio
7
2014
Resolution proof transformation for compression and interpolation. Zbl 1317.68123
Rollini, Simone Fulvio; Bruttomesso, Roberto; Sharygina, Natasha; Tsitovich, Aliaksei
7
2014
Efficient satisfiability modulo theories via delayed theory combination. Zbl 1081.68610
Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Junttila, Tommi; Ranise, Silvio; van Rossum, Peter; Sebastiani, Roberto
6
2005
MathSAT: Tight integration of SAT and mathematical decision procedures. Zbl 1109.68101
Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Junttila, Tommi; van Rossum, Peter; Schulz, Stephan; Sebastiani, Roberto
6
2005
An efficient and flexible approach to resolution proof reduction. Zbl 1325.68215
Rollini, Simone Fulvio; Bruttomesso, Roberto; Sharygina, Natasha
6
2011
From strong amalgamability to modularity of quantifier-free interpolation. Zbl 1358.68183
Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio
6
2012
Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: A comparative analysis. Zbl 1165.68483
Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Griggio, Alberto; Sebastiani, Roberto
5
2006
To Ackermann-ize or not to Ackermann-ize? On efficiently handling uninterpreted function symbols in SMT\((\mathcal{EUF} \cup \mathcal{T})\). Zbl 1165.68482
Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Griggio, Alberto; Santuari, Alessandro; Sebastiani, Roberto
5
2006
Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis. Zbl 1192.68627
Bruttomesso, Roberto; Cimatti, Alessandro; Franzen, Anders; Griggio, Alberto; Sebastiani, Roberto
5
2009
Quantifier-free interpolation of a theory of arrays. Zbl 1237.68123
Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio
4
2012
An extension of lazy abstraction with interpolation for programs with arrays. Zbl 1317.68107
Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha
4
2014
Verifying heap-manipulating programs in an SMT framework. Zbl 1141.68484
Rakamarić, Zvonimir; Bruttomesso, Roberto; Hu, Alan J.; Cimatti, Alessandro
3
2007
A combination of rewriting and constraint solving for the quantifier-free interpolation of arrays with integer difference constraints. Zbl 1348.68123
Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio
2
2011
Encoding RTL constructs for MathSAT: a preliminary report. Zbl 1272.68230
Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Hanna, Ziyad; Khasidashvili, Zurab; Palti, Amit; Sebastiani, Roberto
1
2006
Quantifier-free interpolation in combinations of equality interpolating theories. Zbl 1287.03068
Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio
7
2014
Resolution proof transformation for compression and interpolation. Zbl 1317.68123
Rollini, Simone Fulvio; Bruttomesso, Roberto; Sharygina, Natasha; Tsitovich, Aliaksei
7
2014
An extension of lazy abstraction with interpolation for programs with arrays. Zbl 1317.68107
Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha
4
2014
Lazy abstraction with interpolants for arrays. Zbl 1352.68141
Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha
9
2012
From strong amalgamability to modularity of quantifier-free interpolation. Zbl 1358.68183
Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio
6
2012
Quantifier-free interpolation of a theory of arrays. Zbl 1237.68123
Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio
4
2012
Rewriting-based quantifier-free interpolation for a theory of arrays. Zbl 1236.68179
Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio
7
2011
An efficient and flexible approach to resolution proof reduction. Zbl 1325.68215
Rollini, Simone Fulvio; Bruttomesso, Roberto; Sharygina, Natasha
6
2011
A combination of rewriting and constraint solving for the quantifier-free interpolation of arrays with integer difference constraints. Zbl 1348.68123
Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio
2
2011
Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis. Zbl 1192.68627
Bruttomesso, Roberto; Cimatti, Alessandro; Franzen, Anders; Griggio, Alberto; Sebastiani, Roberto
5
2009
Verifying heap-manipulating programs in an SMT framework. Zbl 1141.68484
Rakamarić, Zvonimir; Bruttomesso, Roberto; Hu, Alan J.; Cimatti, Alessandro
3
2007
Efficient theory combination via Boolean search. Zbl 1137.68578
Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Junttila, Tommi; Ranise, Silvio; Van Rossum, Peter; Sebastiani, Roberto
14
2006
Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: A comparative analysis. Zbl 1165.68483
Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Griggio, Alberto; Sebastiani, Roberto
5
2006
To Ackermann-ize or not to Ackermann-ize? On efficiently handling uninterpreted function symbols in SMT\((\mathcal{EUF} \cup \mathcal{T})\). Zbl 1165.68482
Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Griggio, Alberto; Santuari, Alessandro; Sebastiani, Roberto
5
2006
Encoding RTL constructs for MathSAT: a preliminary report. Zbl 1272.68230
Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Hanna, Ziyad; Khasidashvili, Zurab; Palti, Amit; Sebastiani, Roberto
1
2006
An incremental and layered procedure for the satisfiability of linear arithmetic logic. Zbl 1087.68630
Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Junttila, Tommi; van Rossum, Peter; Schulz, Stephan; Sebastiani, Roberto
9
2005
Efficient satisfiability modulo theories via delayed theory combination. Zbl 1081.68610
Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Junttila, Tommi; Ranise, Silvio; van Rossum, Peter; Sebastiani, Roberto
6
2005
MathSAT: Tight integration of SAT and mathematical decision procedures. Zbl 1109.68101
Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Junttila, Tommi; van Rossum, Peter; Schulz, Stephan; Sebastiani, Roberto
6
2005
all top 5

Cited by 124 Authors

7 Bruttomesso, Roberto
7 Ghilardi, Silvio
6 Ranise, Silvio
6 Sebastiani, Roberto
5 Barrett, Clark W.
5 Cimatti, Alessandro
4 Bonacina, Maria Paola
4 Sharygina, Natasha
3 Bozzano, Marco
3 de Moura, Leonardo
3 Hoenicke, Jochen
3 Johansson, Moa
3 Tinelli, Cesare
2 Alberti, Francesco
2 Christ, Jürgen
2 De Oliveira, Diego Caminha B.
2 Déharbe, David
2 Fontaine, Pascal
2 Gianola, Alessandro
2 Jovanović, Dejan
2 Junttila, Tommi A.
2 Nicolini, Enrica
2 Ringeissen, Christophe
2 Sofronie-Stokkermans, Viorica
2 Song, Xiaoyu
2 van Rossum, Peter
2 Woltzenlogel Paleo, Bruno
1 Abdulla, Parosh Aziz
1 Alt, Leonardo S.
1 Banković, Milan
1 Beyer, Dirk
1 Bjørner, Nikolaj S.
1 Bodirsky, Manuel
1 Bofill, Miquel
1 Bromberger, Martin
1 Cabodi, Gianpiero
1 Calvanese, Diego
1 Cheng, Xi
1 Chin, Wei-Ngan
1 Dangl, Matthias
1 Daniel, Jakub
1 Davis, Ernest E.
1 Demri, Stéphane P.
1 Deters, Morgan
1 Echenim, Mnacho
1 Ermis, Evren
1 Faymonville, Peter
1 Fedyukovich, Grigory
1 Finkbeiner, Bernd
1 Franzén, Anders
1 Garg, Pranav
1 Goel, Amit
1 Gorzny, Jan
1 Greiner, Johannes
1 Griggio, Alberto
1 Gu, Ming
1 Hajdu, Ákos
1 He, Guanhua
1 He, Kai-Duo
1 Holík, Lukáš
1 Hyvärinen, Antti E. J.
1 Jančík, Pavel
1 Jin, HoonSang
1 Jonsson, Bengt
1 Kim, Hyondeuk
1 Kirchner, Hélène
1 Kofroň, Jan
1 Krstic, Sava A.
1 Lengál, Ondřej
1 Leroux, Jérôme
1 Löding, Christof
1 Loiacono, Carmelo
1 Madhusudan, Parthasarathy
1 Mattarei, Cristian
1 McMillan, Kenneth L.
1 Micheli, Andrea
1 Micskei, Zoltán
1 Montali, Marco
1 Nadel, Alexander
1 Neider, Daniel
1 Niemelä, Ilkka N. F.
1 Nieuwenhuis, Robert
1 Oliveras, Albert
1 Palahí, Miquel
1 Parízek, Pavel
1 Passmore, Grant Olney
1 Podelski, Andreas
1 Qin, Shengchao
1 Rabe, Markus N.
1 Reynolds, Andrew
1 Rivkin, Andrey
1 Rollini, Simone Fulvio
1 Roveri, Marco
1 Rümmer, Philipp
1 Rusinowitch, Michaël
1 Ryvchin, Vadim
1 Schlaipfer, Matthias
1 Schulz, Stephan
1 Schuppan, Viktor
1 Shin, Ji-Ae
...and 24 more Authors

Citations by Year