Roberto Bruttomesso
Roberto Bruttomesso
Expert Researcher and Software Engineer
Email verificata su atrenta.com
TitoloCitata daAnno
The MathSAT 4 SMT Solver
R Bruttomesso, A Cimatti, A Franzén, A Griggio, R Sebastiani
International Conference on Computer Aided Verification, 299-303, 2008
2252008
The opensmt solver
R Bruttomesso, E Pek, N Sharygina, A Tsitovich
International Conference on Tools and Algorithms for the Construction and …, 2010
1302010
Efficient satisfiability modulo theories via delayed theory combination
M Bozzano, R Bruttomesso, A Cimatti, T Junttila, S Ranise, P Van Rossum, ...
International Conference on Computer Aided Verification, 335-349, 2005
972005
MathSAT: Tight Integration of SAT and Mathematical Decision Procedures
M Bozzano, R Bruttomesso, A Cimatti, T Junttila, P Van Rossum, S Schulz, ...
Journal of Automated Reasoning 35 (1-3), 265-293, 2005
922005
An incremental and layered procedure for the satisfiability of linear arithmetic logic
M Bozzano, R Bruttomesso, A Cimatti, T Junttila, P Van Rossum, S Schulz, ...
International Conference on Tools and Algorithms for the Construction and …, 2005
852005
An incremental and layered procedure for the satisfiability of linear arithmetic logic
M Bozzano, R Bruttomesso, A Cimatti, T Junttila, P Van Rossum, S Schulz, ...
International Conference on Tools and Algorithms for the Construction and …, 2005
852005
Efficient theory combination via boolean search
M Bozzano, R Bruttomesso, A Cimatti, T Junttila, S Ranise, P van Rossum, ...
Information and Computation 204 (10), 1493-1525, 2006
842006
A Lazy and Layered SMT() Solver for Hard Industrial Verification Problems
R Bruttomesso, A Cimatti, A Franzén, A Griggio, Z Hanna, A Nadel, A Palti, ...
International Conference on Computer Aided Verification, 547-560, 2007
822007
The mathsat 3 system
M Bozzano, R Bruttomesso, A Cimatti, T Junttila, P Van Rossum, S Schulz, ...
International Conference on Automated Deduction, 315-321, 2005
662005
SAFARI: SMT-based abstraction for arrays with interpolants
F Alberti, R Bruttomesso, S Ghilardi, S Ranise, N Sharygina
International Conference on Computer Aided Verification, 679-685, 2012
512012
Lazy abstraction with interpolants for arrays
F Alberti, R Bruttomesso, S Ghilardi, S Ranise, N Sharygina
International Conference on Logic for Programming Artificial Intelligence …, 2012
462012
Encoding RTL constructs for MathSAT: a preliminary report
M Bozzano, R Bruttomesso, A Cimatti, A Franzén, Z Hanna, ...
Electronic Notes in Theoretical Computer Science 144 (2), 3-14, 2006
352006
An extension of lazy abstraction with interpolation for programs with arrays
F Alberti, R Bruttomesso, S Ghilardi, S Ranise, N Sharygina
Formal Methods in System Design 45 (1), 63-109, 2014
292014
Verifying heap-manipulating programs in an SMT framework
Z Rakamarić, R Bruttomesso, AJ Hu, A Cimatti
International Symposium on Automated Technology for Verification and …, 2007
292007
Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: A comparative analysis
R Bruttomesso, A Cimatti, A Franzén, A Griggio, R Sebastiani
International Conference on Logic for Programming Artificial Intelligence …, 2006
272006
An efficient and flexible approach to resolution proof reduction
SF Rollini, R Bruttomesso, N Sharygina
Haifa verification conference, 182-196, 2010
262010
Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
R Bruttomesso, A Cimatti, A Franzen, A Griggio, R Sebastiani
Annals of Mathematics and Artificial Intelligence 55 (1-2), 63, 2009
262009
A scalable decision procedure for fixed-width bit-vectors
R Bruttomesso, N Sharygina
2009 IEEE/ACM International Conference on Computer-Aided Design-Digest of …, 2009
252009
The 2014 SMT competition
DR Cok, D Déharbe, T Weber
Journal on Satisfiability, Boolean Modeling and Computation 9, 207-242, 2016
232016
Rewriting-based Quantifier-free Interpolation for a Theory of Arrays
R Bruttomesso, S Ghilardi, S Ranise
22nd International Conference on Rewriting Techniques and Applications (RTA'11), 2011
202011
Il sistema al momento non puň eseguire l'operazione. Riprova piů tardi.
Articoli 1–20