BibSLEIGH — Cesare

Travelled to:

1 × Australia
1 × Canada
1 × Denmark
1 × Estonia
1 × Ireland
1 × Italy
1 × Poland
1 × Portugal
1 × Russia
1 × United Kingdom
2 × Germany
3 × Austria
5 × USA

Collaborated with:

A.Reynolds C.W.Barrett C.Barrett F.Baader P.Baumgartner A.Goel S.Krstic M.Deters H.Barbosa A.Niemetz M.Preiner T.King K.Bansal J.Grundy A.Nötzli A.Mebsout T.Liang A.Stump G.Sutcliffe Y.Ge S.Ghilardi I.Shikanian L.Hadarean D.Jovanovic A.Champion C.Sticksel J.C.Blanchette S.Cruanes B.Meng V.Kuncak A.Fuchs H.Ganzinger G.Hagen R.Nieuwenhuis A.Oliveras A.Viswanathan D.E.Ouraoui M.Woo D.Brumley Y.Zohar M.Brain B.Ekici C.Keller G.Katz C.L.Conway

Talks about:

smt (12) theori (10) model (7) procedur (6) solver (6) combin (6) decis (5) quantifi (4) solv (4) constraint (3)

Person: Cesare Tinelli

DBLP: Tinelli:Cesare

Facilitated 1 volumes:

Contributed to:

2015

2014

2013

2011

2009

2007

2005

2004

2003

2002

1999

1997

2016

2017

2018

2019

2007

Wrote 36 papers:

CAV-2015-ReynoldsDKTB #quantifier #smt #synthesis: Counterexample-Guided Quantifier Instantiation for Synthesis in SMT (AR, MD, VK, CT, CWB), pp. 198–216.
CAV-2014-HadareanBJBT #lazy evaluation: A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors (LH, KB, DJ, CB, CT), pp. 680–695.
CAV-2014-LiangRTBD #formal method #regular expression #string: A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions (TL, AR, CT, CB, MD), pp. 646–662.
IJCAR-2014-StumpST #framework #logic #named: StarExec: A Cross-Community Infrastructure for Logic Solving (AS, GS, CT), pp. 367–373.
SMT-2014-KingBT #integer #linear #programming #smt: Leveraging Linear and Mixed Integer Programming for SMT (TK, CB, CT), p. 65.
CADE-2013-ReynoldsTGKDB #finite #quantifier #smt: Quantifier Instantiation Techniques for Finite Model Finding in SMT (AR, CT, AG, SK, MD, CB), pp. 377–391.
CAV-2013-ReynoldsTGK #finite #smt: Finite Model Finding in SMT (AR, CT, AG, SK), pp. 640–655.
CADE-2011-BaumgartnerT #evolution #similarity: Model Evolution with Equality Modulo Built-in Theories (PB, CT), pp. 85–100.
CAV-2011-BarrettCDHJKRT: CVC4 (CB, CLC, MD, LH, DJ, TK, AR, CT), pp. 171–177.
CADE-2009-GoelKT: Ground Interpolation for Combined Theories (AG, SK, CT), pp. 183–198.
TACAS-2009-FuchsGGKT #formal method #similarity: Ground Interpolation for the Theory of Equality (AF, AG, JG, SK, CT), pp. 413–427.
CADE-2007-GeBT #modulo theories #quantifier #satisfiability #using #verification: Solving Quantified Verification Conditions Using Satisfiability Modulo Theories (YG, CB, CT), pp. 167–182.
CAV-2007-BarrettT: CVC3 (CB, CT), pp. 298–302.
TACAS-2007-KrsticGGT #parametricity #satisfiability: Combined Satisfiability Modulo Parametric Theories (SK, AG, JG, CT), pp. 602–617.
CADE-2005-BaumgartnerT #calculus #evolution #similarity: The Model Evolution Calculus with Equality (PB, CT), pp. 392–408.
CAV-2004-GanzingerHNOT #performance: DPLL( T): Fast Decision Procedures (HG, GH, RN, AO, CT), pp. 175–188.
IJCAR-2004-BaaderGT #decidability #logic #problem #word: A New Combination Procedure for the Word Problem That Generalizes Fusion Decidability Results in Modal Logics (FB, SG, CT), pp. 183–197.
CADE-2003-BaumgartnerT #calculus #evolution: The Model Evolution Calculus (PB, CT), pp. 350–364.
RTA-2002-BaaderT: Combining Decision Procedures for Positive Theories Sharing Constructors (FB, CT), pp. 352–366.
RTA-1999-BaaderT #equation #problem #word: Deciding the Word Problem in the Union of Equational Theories Sharing Constructors (FB, CT), pp. 175–189.
CADE-1997-BaaderT #approach #problem #word: A New Approach for Combining Decision Procedure for the Word Problem, and Its Connection to the Nelson-Oppen Combination Method (FB, CT), pp. 19–33.
CAV-2016-ChampionMST #model checking: The Kind 2 Model Checker (AC, AM, CS, CT), pp. 510–517.
IJCAR-2016-BansalRBT #constraints #finite #set #smt: A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT (KB, AR, CWB, CT), pp. 82–98.
IJCAR-2016-ReynoldsBCT #recursion #smt: Model Finding for Recursive Functions in SMT (AR, JCB, SC, CT), pp. 133–151.
CADE-2017-MengRTB #constraints #relational #smt #theorem proving: Relational Constraint Solving in SMT (BM, AR, CT, CWB), pp. 148–165.
CAV-2017-EkiciMTKKRB #coq #named #plugin #smt: SMTCoq: A Plug-In for Integrating SMT Solvers into Coq (BE, AM, CT, CK, GK, AR, CWB), pp. 126–133.
CAV-2017-ReynoldsWBBLT #scalability #string #using: Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification (AR, MW, CWB, DB, TL, CT), pp. 453–474.
CAV-2018-NiemetzPRBT #quantifier #using: Solving Quantified Bit-Vectors Using Invertibility Conditions (AN, MP, AR, CWB, CT), pp. 236–255.
IJCAR-2018-ReynoldsVBTB #data type: Datatypes with Shared Selectors (AR, AV, HB, CT, CWB), pp. 591–608.
CADE-2019-BarbosaROTB #higher-order #logic #smt: Extending SMT Solvers to Higher-Order Logic (HB, AR, DEO, CT, CWB), pp. 35–54.
CADE-2019-NiemetzPRZBT #independence #proving #smt #towards: Towards Bit-Width-Independent Proofs in SMT Solvers (AN, MP, AR, YZ, CWB, CT), pp. 366–384.
CAV-2019-BrainNPRBT #float: Invertibility Conditions for Floating-Point Formulas (MB, AN, MP, AR, CWB, CT), pp. 116–136.
CAV-2019-ReynoldsBNBT #named #performance #synthesis: cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis (AR, HB, AN, CWB, CT), pp. 74–83.
CAV-2019-ReynoldsNBT #abstraction #constraints #smt #string: High-Level Abstractions for Simplifying Extended String Constraints in SMT (AR, AN, CWB, CT), pp. 23–42.
SMT-J-2006-BarrettST #data type #formal method #induction: An Abstract Decision Procedure for a Theory of Inductive Data Types (CB, IS, CT), pp. 21–46.