×

zbMATH — the first resource for mathematics

Ranise, Silvio

Compute Distance To:
Author ID: ranise.silvio Recent zbMATH articles by "Ranise, Silvio"
Published as: Ranise, Silvio; Ranise, S.
Documents Indexed: 52 Publications since 2000, including 2 Books

Publications by Year

Citations contained in zbMATH Open

42 Publications have been cited 251 times in 117 Documents Cited by Year
A rewriting approach to satisfiability procedures. Zbl 1054.68077
Armando, Alessandro; Ranise, Silvio; Rusinowitch, Michaël
31
2003
New results on rewrite-based satisfiability procedures. Zbl 1367.68243
Armando, Alessandro; Bonacina, Maria Paola; Ranise, Silvio; Schulz, Stephan
23
2009
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
MCMT: a model checker modulo theories. Zbl 1291.68257
Ghilardi, Silvio; Ranise, Silvio
13
2010
Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures. Zbl 1222.03011
Bonacina, Maria Paola; Ghilardi, Silvio; Nicolini, Enrica; Ranise, Silvio; Zucchelli, Daniele
11
2006
Combining data structures with nonstably infinite theories using many-sorted logic. Zbl 1171.68439
Ranise, Silvio; Ringeissen, Christophe; Zarba, Calogero G.
10
2005
Backward reachability of array-based systems by SMT solving: termination and invariant synthesis. Zbl 1213.68379
Ghilardi, Silvio; Ranise, Silvio
10
2010
Uniform derivation of decision procedures by superposition. Zbl 1005.03012
Armando, Alessandro; Ranise, Silvio; Rusinowitch, Michaël
9
2001
Towards SMT model checking of array-based systems. Zbl 1165.68406
Ghilardi, Silvio; Nicolini, Enrica; Ranise, Silvio; Zucchelli, Daniele
9
2008
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
Combination methods for satisfiability and model-checking of infinite-state systems. Zbl 1213.68378
Ghilardi, Silvio; Nicolini, Enrica; Ranise, Silvio; Zucchelli, Daniele
6
2007
On a rewriting approach to satisfiability procedures: Extension, combination of theories and an experimental appraisal. Zbl 1171.68507
Armando, Alessandro; Bonacina, Maria Paola; Ranise, Silvio; Schulz, Stephan
6
2005
Nelson-Oppen, Shostak and the extended canonizer: A family picture with a newborn. Zbl 1108.68574
Ranise, Silvio; Ringeissen, Christophe; Tran, Duc-Khanh
6
2005
On superposition-based satisfiability procedures and their combination. Zbl 1169.68509
Kirchner, Hélène; Ranise, Silvio; Ringeissen, Christophe; Tran, Duc Khanh
6
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
From strong amalgamability to modularity of quantifier-free interpolation. Zbl 1358.68183
Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio
6
2012
Decision procedures for extensions of the theory of arrays. Zbl 1125.68115
Ghilardi, Silvio; Nicolini, Enrica; Ranise, Silvio; Zucchelli, Daniele
5
2007
Automatic combinability of rewriting-based satisfiability procedures. Zbl 1165.68490
Kirchner, Hélène; Ranise, Silvio; Ringeissen, Christophe; Tran, Duc-Khanh
5
2006
Universal guards, relativization of quantifiers, and failure models in model checking modulo theories. Zbl 1331.68141
Alberti, Francesco; Ghilardi, Silvio; Pagani, Elena; Ranise, Silvio; Rossi, Gian Paolo
5
2012
Applying light-weight theorem proving to debugging and verifying pointer programs. Zbl 1261.68106
Ranise, Silvio; Déharbe, David
5
2003
Combination of convex theories: modularity, deduction completeness, and explanation. Zbl 1192.68190
Tran, Duc-Khanh; Ringeissen, Christophe; Ranise, Silvio; Kirchner, Hélène
4
2010
Automatic decidability and combinability. Zbl 1216.68163
Lynch, Christopher; Ranise, Silvio; Ringeissen, Christophe; Tran, Duc-Khanh
4
2011
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
Quantifier-free interpolation of a theory of arrays. Zbl 1237.68123
Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio
4
2012
Constraint contextual rewriting. Zbl 1039.68059
Armando, Alessandro; Ranise, Silvio
3
2003
Termination of constraint contextual rewriting. Zbl 0971.68140
Armando, Alessandro; Ranise, Silvio
2
2000
A practical extension mechanism for decision procedures: The case study of universal Presburger arithmetic. Zbl 0970.68110
Armando, Alessandro; Ranise, Silvio
2
2001
System description: RDL: Rewrite and Decision procedure Laboratory. Zbl 0988.68557
Armando, Alessandro; Compagna, Luca; Ranise, Silvio
2
2001
Combining lists with non-stably infinite theories. Zbl 1108.68384
Fontaine, Pascal; Ranise, Silvio; Zarba, Calogero G.
2
2005
Noetherianity and combination problems. Zbl 1148.03010
Ghilardi, Silvio; Nicolini, Enrica; Ranise, Silvio; Zucchelli, Daniele
2
2007
Deciding extensions of the theory of arrays by integrating decision procedures and instantiation strategies. Zbl 1152.68519
Ghilardi, Silvio; Nicolini, Enrica; Ranise, Silvio; Zucchelli, Daniele
2
2006
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
On the verification of security-aware E-services. Zbl 1241.94030
Ranise, Silvio
2
2012
Communication protocols for mathematical services based on KQML and OMRS. Zbl 0986.68003
Armando, Alessandro; Kohlhase, Michael; Ranise, Silvio
1
2001
Abstraction-driven verification of array programs. Zbl 1109.68578
Déharbe, David; Imine, Abdessamad; Ranise, Silvio
1
2004
Combining proof-producing decision procedures. Zbl 1148.68467
Ranise, Silvio; Ringeissen, Christophe; Tran, Duc-Khanh
1
2007
Goal-directed invariant synthesis for model checking modulo theories. Zbl 1260.68230
Ghilardi, Silvio; Ranise, Silvio
1
2009
Automated termination in model checking modulo theories. Zbl 1348.68124
Carioni, Alessandro; Ghilardi, Silvio; Ranise, Silvio
1
2011
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
Ahrendt, Wolfgang (ed.); Baumgartner, P. (ed.); de Nivelle, H. (ed.); Ranise, S. (ed.); Tinelli, C. (ed.)
1
2005
Light-weight SMT-based model checking. Zbl 1335.68138
Ghilardi, Silvio; Ranise, Silvio; Valsecchi, Thomas
1
2009
Quantifier-free interpolation in combinations of equality interpolating theories. Zbl 1287.03068
Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio
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
Universal guards, relativization of quantifiers, and failure models in model checking modulo theories. Zbl 1331.68141
Alberti, Francesco; Ghilardi, Silvio; Pagani, Elena; Ranise, Silvio; Rossi, Gian Paolo
5
2012
Quantifier-free interpolation of a theory of arrays. Zbl 1237.68123
Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio
4
2012
On the verification of security-aware E-services. Zbl 1241.94030
Ranise, Silvio
2
2012
Rewriting-based quantifier-free interpolation for a theory of arrays. Zbl 1236.68179
Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio
7
2011
Automatic decidability and combinability. Zbl 1216.68163
Lynch, Christopher; Ranise, Silvio; Ringeissen, Christophe; Tran, Duc-Khanh
4
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
Automated termination in model checking modulo theories. Zbl 1348.68124
Carioni, Alessandro; Ghilardi, Silvio; Ranise, Silvio
1
2011
MCMT: a model checker modulo theories. Zbl 1291.68257
Ghilardi, Silvio; Ranise, Silvio
13
2010
Backward reachability of array-based systems by SMT solving: termination and invariant synthesis. Zbl 1213.68379
Ghilardi, Silvio; Ranise, Silvio
10
2010
Combination of convex theories: modularity, deduction completeness, and explanation. Zbl 1192.68190
Tran, Duc-Khanh; Ringeissen, Christophe; Ranise, Silvio; Kirchner, Hélène
4
2010
New results on rewrite-based satisfiability procedures. Zbl 1367.68243
Armando, Alessandro; Bonacina, Maria Paola; Ranise, Silvio; Schulz, Stephan
23
2009
Goal-directed invariant synthesis for model checking modulo theories. Zbl 1260.68230
Ghilardi, Silvio; Ranise, Silvio
1
2009
Light-weight SMT-based model checking. Zbl 1335.68138
Ghilardi, Silvio; Ranise, Silvio; Valsecchi, Thomas
1
2009
Towards SMT model checking of array-based systems. Zbl 1165.68406
Ghilardi, Silvio; Nicolini, Enrica; Ranise, Silvio; Zucchelli, Daniele
9
2008
Combination methods for satisfiability and model-checking of infinite-state systems. Zbl 1213.68378
Ghilardi, Silvio; Nicolini, Enrica; Ranise, Silvio; Zucchelli, Daniele
6
2007
Decision procedures for extensions of the theory of arrays. Zbl 1125.68115
Ghilardi, Silvio; Nicolini, Enrica; Ranise, Silvio; Zucchelli, Daniele
5
2007
Noetherianity and combination problems. Zbl 1148.03010
Ghilardi, Silvio; Nicolini, Enrica; Ranise, Silvio; Zucchelli, Daniele
2
2007
Combining proof-producing decision procedures. Zbl 1148.68467
Ranise, Silvio; Ringeissen, Christophe; Tran, Duc-Khanh
1
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
Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures. Zbl 1222.03011
Bonacina, Maria Paola; Ghilardi, Silvio; Nicolini, Enrica; Ranise, Silvio; Zucchelli, Daniele
11
2006
Automatic combinability of rewriting-based satisfiability procedures. Zbl 1165.68490
Kirchner, Hélène; Ranise, Silvio; Ringeissen, Christophe; Tran, Duc-Khanh
5
2006
Deciding extensions of the theory of arrays by integrating decision procedures and instantiation strategies. Zbl 1152.68519
Ghilardi, Silvio; Nicolini, Enrica; Ranise, Silvio; Zucchelli, Daniele
2
2006
Combining data structures with nonstably infinite theories using many-sorted logic. Zbl 1171.68439
Ranise, Silvio; Ringeissen, Christophe; Zarba, Calogero G.
10
2005
On a rewriting approach to satisfiability procedures: Extension, combination of theories and an experimental appraisal. Zbl 1171.68507
Armando, Alessandro; Bonacina, Maria Paola; Ranise, Silvio; Schulz, Stephan
6
2005
Nelson-Oppen, Shostak and the extended canonizer: A family picture with a newborn. Zbl 1108.68574
Ranise, Silvio; Ringeissen, Christophe; Tran, Duc-Khanh
6
2005
On superposition-based satisfiability procedures and their combination. Zbl 1169.68509
Kirchner, Hélène; Ranise, Silvio; Ringeissen, Christophe; Tran, Duc Khanh
6
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
Combining lists with non-stably infinite theories. Zbl 1108.68384
Fontaine, Pascal; Ranise, Silvio; Zarba, Calogero G.
2
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
Ahrendt, Wolfgang; Baumgartner, P.; de Nivelle, H.; Ranise, S.; Tinelli, C.
1
2005
Abstraction-driven verification of array programs. Zbl 1109.68578
Déharbe, David; Imine, Abdessamad; Ranise, Silvio
1
2004
A rewriting approach to satisfiability procedures. Zbl 1054.68077
Armando, Alessandro; Ranise, Silvio; Rusinowitch, Michaël
31
2003
Applying light-weight theorem proving to debugging and verifying pointer programs. Zbl 1261.68106
Ranise, Silvio; Déharbe, David
5
2003
Constraint contextual rewriting. Zbl 1039.68059
Armando, Alessandro; Ranise, Silvio
3
2003
Uniform derivation of decision procedures by superposition. Zbl 1005.03012
Armando, Alessandro; Ranise, Silvio; Rusinowitch, Michaël
9
2001
A practical extension mechanism for decision procedures: The case study of universal Presburger arithmetic. Zbl 0970.68110
Armando, Alessandro; Ranise, Silvio
2
2001
System description: RDL: Rewrite and Decision procedure Laboratory. Zbl 0988.68557
Armando, Alessandro; Compagna, Luca; Ranise, Silvio
2
2001
Communication protocols for mathematical services based on KQML and OMRS. Zbl 0986.68003
Armando, Alessandro; Kohlhase, Michael; Ranise, Silvio
1
2001
Termination of constraint contextual rewriting. Zbl 0971.68140
Armando, Alessandro; Ranise, Silvio
2
2000
all top 5

Cited by 175 Authors

15 Ranise, Silvio
12 Ghilardi, Silvio
10 Bonacina, Maria Paola
10 Ringeissen, Christophe
7 Echenim, Mnacho
6 Bruttomesso, Roberto
6 Rusinowitch, Michaël
5 Armando, Alessandro
5 Cimatti, Alessandro
5 Nicolini, Enrica
5 Sharygina, Natasha
5 Weidenbach, Christoph
4 Barrett, Clark W.
4 de Moura, Leonardo
4 Peltier, Nicolas
4 Sebastiani, Roberto
4 Sofronie-Stokkermans, Viorica
4 Tran, Duc-Khanh
3 Alberti, Francesco
3 Chocron, Paula
3 Conchon, Sylvain
3 Fontaine, Pascal
3 Hoenicke, Jochen
3 Johansson, Moa
3 Meseguer Guaita, José
3 Tinelli, Cesare
2 Christ, Jürgen
2 Déharbe, David
2 Gianola, Alessandro
2 Griggio, Alberto
2 Jovanović, Dejan
2 Junttila, Tommi A.
2 Kanig, Johannes
2 Konnov, Igor V.
2 Kruglov, Evgeniĭ Valentinovich
2 Lynch, Christopher A.
2 Roveri, Marco
2 Skeirik, Stephen
2 Sun, Jiaguang
2 Tonetta, Stefano
2 Veith, Helmut
2 Voronkov, Andrei
2 Widder, Josef
2 Zhou, Min
2 Zucchelli, Daniele
1 Alhiyafi, Jamal
1 Althaus, Ernst
1 Aminof, Benjamin
1 Ballarin, Clemens
1 Belkhir, Walid
1 Beyer, Dirk
1 Bjørner, Nikolaj S.
1 Bliudze, Simon
1 Bodirsky, Manuel
1 Bofill, Miquel
1 Böhme, Sascha
1 Bozzano, Marco
1 Calvanese, Diego
1 Casal, Filipe
1 Cheng, Xi
1 Chevalier, Yannick
1 Claessen, Koen
1 Coglio, Alessandro
1 Contejean, Evelyne
1 Dangl, Matthias
1 Daniel, Jakub
1 Declerck, David
1 Demri, Stéphane P.
1 Deng, Yuxin
1 Dershowitz, Nachum
1 Dhar, Amit Kumar
1 Dross, Claire
1 Dubrovin, Jori
1 Ermis, Evren
1 Fietzke, Arnaud
1 Franke, Andreas
1 Franzén, Anders
1 Ganzinger, Harald
1 Garg, Pranav
1 Giunchiglia, Fausto
1 Gmeiner, Annu
1 Goel, Amit
1 Greiner, Johannes
1 Gu, Ming
1 Hajdu, Ákos
1 He, Fei
1 Heidarian, Faranak
1 Heljanko, Keijo
1 Hillenbrand, Thomas
1 Hou, Zechen
1 Hyvärinen, Antti E. J.
1 Jamnik, Mateja
1 Janičić, Predrag
1 Kapur, Deepak
1 Kazakov, Yevgeny
1 Kirchner, Hélène
1 Kohlhase, Michael
1 Kortelainen, Juha
1 Kovács, Laura Ildikó
1 Krstic, Sava A.
...and 75 more Authors

Citations by Year