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 |