| 2009 |
| 37 | EE | Alexander Fuchs,
Amit Goel,
Jim Grundy,
Sava Krstic,
Cesare Tinelli:
Ground Interpolation for the Theory of Equality.
TACAS 2009: 413-427 |
| 36 | EE | Peter Baumgartner,
Alexander Fuchs,
Hans de Nivelle,
Cesare Tinelli:
Computing finite models by reduction to function-free clause logic.
J. Applied Logic 7(1): 58-74 (2009) |
| 2008 |
| 35 | EE | Peter Baumgartner,
Alexander Fuchs,
Cesare Tinelli:
(LIA) - Model Evolution with Linear Integer Arithmetic Constraints.
LPAR 2008: 258-273 |
| 34 | EE | Peter Baumgartner,
Cesare Tinelli:
The model evolution calculus as a first-order DPLL method.
Artif. Intell. 172(4-5): 591-632 (2008) |
| 2007 |
| 33 | EE | Yeting Ge,
Clark Barrett,
Cesare Tinelli:
Solving Quantified Verification Conditions Using Satisfiability Modulo Theories.
CADE 2007: 167-182 |
| 32 | EE | Clark Barrett,
Cesare Tinelli:
CVC3.
CAV 2007: 298-302 |
| 31 | EE | Cesare Tinelli:
An Abstract Framework for Satisfiability Modulo Theories.
TABLEAUX 2007: 10 |
| 30 | EE | Sava Krstic,
Amit Goel,
Jim Grundy,
Cesare Tinelli:
Combined Satisfiability Modulo Parametric Theories.
TACAS 2007: 602-617 |
| 29 | EE | Cesare Tinelli:
Trends and Challenges in Satisfiability Modulo Theories.
VERIFY 2007 |
| 28 | EE | Clark Barrett,
Igor Shikanian,
Cesare Tinelli:
An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types.
Electr. Notes Theor. Comput. Sci. 174(8): 23-37 (2007) |
| 27 | EE | Clark Barrett,
Igor Shikanian,
Cesare Tinelli:
An Abstract Decision Procedure for a Theory of Inductive Data Types.
JSAT 3(1-2): 21-46 (2007) |
| 2006 |
| 26 | EE | Clark Barrett,
Robert Nieuwenhuis,
Albert Oliveras,
Cesare Tinelli:
Splitting on Demand in SAT Modulo Theories.
LPAR 2006: 512-526 |
| 25 | EE | Peter Baumgartner,
Alexander Fuchs,
Cesare Tinelli:
Lemma Learning in the Model Evolution Calculus.
LPAR 2006: 572-586 |
| 24 | EE | Bernhard Beckert,
Tony Hoare,
Reiner Hähnle,
Douglas R. Smith,
Cordell Green,
Silvio Ranise,
Cesare Tinelli,
Thomas Ball,
Sriram K. Rajamani:
Intelligent Systems and Formal Methods in Software Engineering.
IEEE Intelligent Systems 21(6): 71-81 (2006) |
| 23 | EE | Franz Baader,
Silvio Ghilardi,
Cesare Tinelli:
A new combination procedure for the word problem that generalizes fusion decidability results in modal logics.
Inf. Comput. 204(10): 1413-1452 (2006) |
| 22 | EE | Peter Baumgartner,
Alexander Fuchs,
Cesare Tinelli:
Implementing the Model Evolution Calculus.
International Journal on Artificial Intelligence Tools 15(1): 21-52 (2006) |
| 21 | EE | Robert Nieuwenhuis,
Albert Oliveras,
Cesare Tinelli:
Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T).
J. ACM 53(6): 937-977 (2006) |
| 2005 |
| 20 | EE | Peter Baumgartner,
Cesare Tinelli:
The Model Evolution Calculus with Equality.
CADE 2005: 392-408 |
| 19 | EE | Cesare Tinelli,
Calogero G. Zarba:
Combining Nonstably Infinite Theories.
J. Autom. Reasoning 34(3): 209-238 (2005) |
| 2004 |
| 18 | EE | Harald Ganzinger,
George Hagen,
Robert Nieuwenhuis,
Albert Oliveras,
Cesare Tinelli:
DPLL( T): Fast Decision Procedures.
CAV 2004: 175-188 |
| 17 | EE | Franz Baader,
Silvio Ghilardi,
Cesare Tinelli:
A New Combination Procedure for the Word Problem That Generalizes Fusion Decidability Results in Modal Logics.
IJCAR 2004: 183-197 |
| 16 | EE | Cesare Tinelli,
Calogero G. Zarba:
Combining Decision Procedures for Sorted Theories.
JELIA 2004: 641-653 |
| 15 | EE | Robert Nieuwenhuis,
Albert Oliveras,
Cesare Tinelli:
Abstract DPLL and Abstract DPLL Modulo Theories.
LPAR 2004: 36-50 |
| 2003 |
| 14 | EE | Peter Baumgartner,
Cesare Tinelli:
The Model Evolution Calculus.
CADE 2003: 350-364 |
| 13 | EE | Cesare Tinelli,
Calogero G. Zarba:
Combining Non-Stably Infinite Theories.
Electr. Notes Theor. Comput. Sci. 86(1): (2003) |
| 12 | | Cesare Tinelli:
Cooperation of Background Reasoners in Theory Reasoning by Residue Sharing.
J. Autom. Reasoning 30(1): 1-31 (2003) |
| 11 | | Cesare Tinelli,
Christophe Ringeissen:
Unions of non-disjoint theories and combinations of satisfiability procedures.
Theor. Comput. Sci. 290(1): 291-353 (2003) |
| 10 | | Cesare Tinelli,
Teodor Rus:
Preface.
Theor. Comput. Sci. 291(3): 219-221 (2003) |
| 2002 |
| 9 | EE | Cesare Tinelli:
A DPLL-Based Calculus for Ground Satisfiability Modulo Theories.
JELIA 2002: 308-319 |
| 8 | EE | Franz Baader,
Cesare Tinelli:
Combining Decision Procedures for Positive Theories Sharing Constructors.
RTA 2002: 352-366 |
| 7 | EE | Franz Baader,
Cesare Tinelli:
Deciding the Word Problem in the Union of Equational Theories.
Inf. Comput. 178(2): 346-390 (2002) |
| 2000 |
| 6 | | Franz Baader,
Cesare Tinelli:
Combining Equational Theories Sharing Non-Collapse-Free Constructors.
FroCos 2000: 260-274 |
| 1999 |
| 5 | EE | Franz Baader,
Cesare Tinelli:
Deciding the Word Problem in the Union of Equational Theories Sharing Constructors.
RTA 1999: 175-189 |
| 1998 |
| 4 | | Cesare Tinelli,
Mehdi T. Harandi:
Constraint Logic Programming over Unions of Constraint Theories.
Journal of Functional and Logic Programming 1998(6): (1998) |
| 1997 |
| 3 | | Franz Baader,
Cesare Tinelli:
A New Approach for Combining Decision Procedure for the Word Problem, and Its Connection to the Nelson-Oppen Combination Method.
CADE 1997: 19-33 |
| 1996 |
| 2 | | Cesare Tinelli,
Mehdi T. Harandi:
Constraint Logic Programming over Unions of Constraint Theories.
CP 1996: 436-450 |
| 1 | | Cesare Tinelli,
Mehdi T. Harandi:
A New Correctness Proof of the {Nelson-Oppen} Combination Procedure.
Frontiers of Combining Systems (FroCos) 1996: 103-119 |