Roberto Bruttomesso - Publications List

Journal articles

2009

R Bruttomesso, A Cimatti, A Franzen, A Griggio, R Sebastiani (2009) Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories : a comparative analysis Annals of Mathematics and Artificial Intelligence

Abstract:

Notes:

2006

M Bozzano, R Bruttomesso, A Cimatti, T Junttila, S Ranise, P van Rossum, R Sebastiani (2006) Efficient Theory Combination via Boolean Search Information Computation 204: 10. 1493-1525

Abstract:

Notes:

2005

M Bozzano, R Bruttomesso, A Cimatti, T Junttila, P van Rossum, S Schulz, R Sebastiani (2005) MathSAT : Tight Integration of SAT and Mathematical Decision Procedures JAR 35: 1-3. 265-293

Abstract:

Notes:

Conference papers

2011

2010

R Bruttomesso, E Pek, N Sharygina, A Tsitovich (2010) The OpenSMT Solver In: TACAS

Abstract:

Notes:

R Bruttomesso, E Pek, N Sharygina (2010) A Flexible Schema for Generating Explanations in Lazy Theory Propagation In: MEMOCODE

Abstract:

Notes:

S Rollini, R Bruttomesso, N Sharygina (2010) An Efficient and Flexible Approach to Resolution Proof Reduction In: HVC

Abstract:

Notes:

R Bruttomesso, S Rollini, N Sharygina, A Tsitovich (2010) Flexible Interpolation with Local Proof Transformation In: ICCAD

Abstract:

Notes:

2009

R Bruttomesso (2009) An Extension of the Davis-Putnam Procedure and its Application to Preprocessing in SMT In: SMT

Abstract:

Notes:

2008

R Bruttomesso, A Cimatti, A Franzén, A Griggio, R Sebastiani (2008) The MathSAT 4 SMT Solver In: CAV 299-303

Abstract:

Notes:

2007

R Bruttomesso, A Cimatti, A Franzen, A Griggio, Z Hanna, A Nadel, A Palti, R Sebastiani (2007) A Lazy and Layered SMT(BV) Solver for Hard Industrial Verification Problems In: CAV 247-260

Abstract:

Notes:

Z Rakamarić, R Bruttomesso, A J Hu, A Cimatti (2007) Verifying Heap Manipulating Programs in an SMT Framework In: ATVA’07 237-252

Abstract:

Notes:

2006

2005

M Bozzano, R Bruttomesso, A Cimatti, T Junttila, P Van Rossum, S Ranise, R Sebastiani (2005) Efficient Satisfiability Modulo Theories via Delayed Theory Combination In: CAV’05 335-349

Abstract:

Notes:

M Bozzano, R Bruttomesso, A Cimatti, T Junttila, P Van Rossum, S Schulz, R Sebastiani (2005) The MathSAT 3 System In: CADE-20 315-321

Abstract:

Notes:

M Bozzano, R Bruttomesso, A Cimatti, T Junttila, P Van Rossum, S Schulz, R Sebastiani (2005) An Incremental and Layered Procedure for Satisfiability of Linear Arithmetic Logic In: TACAS 317-333

Abstract:

Notes:

M Bozzano, R Bruttomesso, A Cimatti, A Franzén, Z Hanna, Z Kasidashvili, A Palti, R Sebastiani (2005) Encoding RTL constructs for MathSAT : a preliminary report In: PDPAR’05 3-14

Abstract:

Notes:

PhD theses

2008

Roberto Bruttomesso (2008) RTL Verification : from SAT to SMT(BV) University of Trento

Abstract:

Notes: Available at \urlhttp://www.inf.unisi.ch/postdoc/bruttomesso/files/phdthesis.pdf