Roberto Bruttomesso

	2012
23		Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina: Lazy Abstraction with Interpolants for Arrays. LPAR 2012: 46-61
22		Roberto Bruttomesso, Alessandro Carioni, Silvio Ghilardi, Silvio Ranise: Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms. NASA Formal Methods 2012: 279-294
21		Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise: From Strong Amalgamability to Modularity of Quantifier-Free Interpolation CoRR abs/1203.3730: (2012)
20		Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise: Quantifier-Free Interpolation of a Theory of Arrays Logical Methods in Computer Science 8(2): (2012)
	2011
19		Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise: A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints. FroCos 2011: 103-118
18		Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise: Rewriting-based Quantifier-free Interpolation for a Theory of Arrays. RTA 2011: 171-186
	2010
17		Simone Rollini, Roberto Bruttomesso, Natasha Sharygina: An Efficient and Flexible Approach to Resolution Proof Reduction. Haifa Verification Conference 2010: 182-196
16		Roberto Bruttomesso, Simone Rollini, Natasha Sharygina, Aliaksei Tsitovich: Flexible interpolation with local proof transformations. ICCAD 2010: 770-777
15		Roberto Bruttomesso, Edgar Pek, Natasha Sharygina: A flexible schema for generating explanations in lazy theory propagation. MEMOCODE 2010: 41-48
14		Roberto Bruttomesso, Edgar Pek, Natasha Sharygina, Aliaksei Tsitovich: The OpenSMT Solver. TACAS 2010: 150-153
	2009
13		Roberto Bruttomesso, Natasha Sharygina: A scalable decision procedure for fixed-width bit-vectors. ICCAD 2009: 13-20
12		Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani: Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis. Ann. Math. Artif. Intell. 55(1-2): 63-99 (2009)
	2008
11		Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani: The MathSAT 4SMT Solver. CAV 2008: 299-303
	2007
10		Zvonimir Rakamaric, Roberto Bruttomesso, Alan J. Hu, Alessandro Cimatti: Verifying Heap-Manipulating Programs in an SMT Framework. ATVA 2007: 237-252
9		Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Ziyad Hanna, Alexander Nadel, Amit Palti, Roberto Sebastiani: A Lazy and Layered SMT($\mathcal{BV}$) Solver for Hard Industrial Verification Problems. CAV 2007: 547-560
	2006
8		Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani: Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis. LPAR 2006: 527-541
7		Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Alessandro Santuari, Roberto Sebastiani: To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in SMT(EUF ÈT). LPAR 2006: 557-571
6		Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Ziyad Hanna, Zurab Khasidashvili, Amit Palti, Roberto Sebastiani: Encoding RTL Constructs for MathSAT: a Preliminary Report. Electr. Notes Theor. Comput. Sci. 144(2): 3-14 (2006)
5		Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani: Efficient theory combination via boolean search. Inf. Comput. 204(10): 1493-1525 (2006)
	2005
4		Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani: The MathSAT 3 System. CADE 2005: 315-321
3		Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani: Efficient Satisfiability Modulo Theories via Delayed Theory Combination. CAV 2005: 335-349
2		Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani: An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic. TACAS 2005: 317-333
1		Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani: MathSAT: Tight Integration of SAT and Mathematical Decision Procedures. J. Autom. Reasoning 35(1-3): 265-293 (2005)

Coauthor Index

1	Francesco Alberti	[23]
2	Marco Bozzano	[1] [2] [3] [4] [5] [6]
3	Alessandro Carioni	[22]
4	Alessandro Cimatti	[1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11] [12]
5	Anders Franzén	[6] [7] [8] [9] [11] [12]
6	Silvio Ghilardi	[18] [19] [20] [21] [22] [23]
7	Alberto Griggio	[7] [8] [9] [11] [12]
8	Ziyad Hanna	[6] [9]
9	Alan J. Hu	[10]
10	Tommi A. Junttila	[1] [2] [3] [4] [5]
11	Zurab Khasidashvili	[6]
12	Alexander Nadel	[9]
13	Amit Palti	[6] [9]
14	Edgar Pek	[14] [15]
15	Zvonimir Rakamaric	[10]
16	Silvio Ranise	[3] [5] [18] [19] [20] [21] [22] [23]
17	Simone Rollini	[16] [17]
18	Peter van Rossum	[1] [2] [3] [4] [5]
19	Alessandro Santuari	[7]
20	Stephan Schulz	[1] [2] [4]
21	Roberto Sebastiani	[1] [2] [3] [4] [5] [6] [7] [8] [9] [11] [12]
22	Natasha Sharygina	[13] [14] [15] [16] [17] [23]
23	Aliaksei Tsitovich	[14] [16]

Last update Sun May 27 04:04:01 2012 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page