BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Cyprus
1 × Estonia
1 × Germany
1 × Serbia
2 × USA
4 × United Kingdom
Collaborated with:
S.Ranise S.Ghilardi A.Cimatti R.Sebastiani N.Sharygina A.Griggio M.Bozzano T.A.Junttila P.v.Rossum F.Alberti A.Franzén S.Schulz D.R.Cok M.Deters E.Pek A.Tsitovich Z.Hanna A.Nadel A.Palti
Talks about:
smt (5) theori (4) interpol (3) solver (3) quantifi (2) satisfi (2) modulo (2) layer (2) array (2) math (2)

Person: Roberto Bruttomesso

DBLP DBLP: Bruttomesso:Roberto

Contributed to:

CAV 20122012
IJCAR 20122012
SMT 20122012
RTA 20112011
TACAS 20102010
CAV 20082008
CAV 20072007
CADE 20052005
CAV 20052005
TACAS 20052005

Wrote 11 papers:

CAV-2012-AlbertiBGRS #abstraction #array #named #smt
SAFARI: SMT-Based Abstraction for Arrays with Interpolants (FA, RB, SG, SR, NS), pp. 679–685.
IJCAR-2012-BruttomessoGR #composition #quantifier
From Strong Amalgamability to Modularity of Quantifier-Free Interpolation (RB, SG, SR), pp. 118–133.
SMT-2012-AlbertiBGRS #library #modulo theories #reachability
Reachability Modulo Theory Library (FA, RB, SG, SR, NS), pp. 67–76.
SMT-2012-CokGBD #contest #smt
The 2012 SMT Competition (DRC, AG, RB, MD), pp. 131–142.
RTA-2011-BruttomessoGR #array #formal method #quantifier
Rewriting-based Quantifier-free Interpolation for a Theory of Arrays (RB, SG, SR), pp. 171–186.
TACAS-2010-BruttomessoPST
The OpenSMT Solver (RB, EP, NS, AT), pp. 150–153.
CAV-2008-BruttomessoCFGS #smt
The MathSAT 4SMT Solver (RB, AC, AF, AG, RS), pp. 299–303.
CAV-2007-BruttomessoCFGHNPS #industrial #lazy evaluation #problem #smt #verification
A Lazy and Layered SMT(BV) Solver for Hard Industrial Verification Problems (RB, AC, AF, AG, ZH, AN, AP, RS), pp. 547–560.
CADE-2005-BozzanoBCJRSS
The MathSAT 3 System (MB, RB, AC, TAJ, PvR, SS, RS), pp. 315–321.
CAV-2005-BozzanoBCJRRS #modulo theories #performance #satisfiability
Efficient Satisfiability Modulo Theories via Delayed Theory Combination (MB, RB, AC, TAJ, SR, PvR, RS), pp. 335–349.
TACAS-2005-BozzanoBCJRSS #incremental #linear #logic #satisfiability
An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic (MB, RB, AC, TAJ, PvR, SS, RS), pp. 317–333.
Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.