Cesare Tinelli - researchr alias

researchr

You are not signed in
Sign in
Sign up

2011

2010

The SMT-LIB Initiative and the Rise of SMT - (HVC 2010 Award Talk)Clark Barrett, Leonardo Mendonça de Moura, Silvio Ranise, Aaron Stump, Cesare Tinelli. hvc 2011: 3 [doi]

Foundations of Satisfiability Modulo TheoriesCesare Tinelli. wollic 2010: 58 [doi]

2009

Satisfiability Modulo TheoriesClark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, Cesare Tinelli. In Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh, editors, Handbook of Satisfiability. Volume 185 of Frontiers in Artificial Intelligence and Applications, pages 825-885, IOS Press, 2009. [doi]

Computing finite models by reduction to function-free clause logicPeter Baumgartner, Alexander Fuchs, Hans de Nivelle, Cesare Tinelli. japll, 7(1):58-74, 2009. [doi]

Ground Interpolation for the Theory of EqualityAlexander Fuchs, Amit Goel, Jim Grundy, Sava Krstic, Cesare Tinelli. TACAS 2009: 413-427 [doi]

Solving quantified verification conditions using satisfiability modulo theoriesYeting Ge, Clark W. Barrett, Cesare Tinelli. AMAI, 55(1-2):101-122, 2009. [doi]

Ground Interpolation for Combined TheoriesAmit Goel, Sava Krstic, Cesare Tinelli. cade 2009: 183-198 [doi]

2008

The model evolution calculus as a first-order DPLL methodPeter Baumgartner, Cesare Tinelli. ai, 172(4-5):591-632, 2008. [doi]

(LIA) - Model Evolution with Linear Integer Arithmetic ConstraintsPeter Baumgartner, Alexander Fuchs, Cesare Tinelli. lpar 2008: 258-273 [doi]

Scaling Up the Formal Verification of Lustre Programs with SMT-Based TechniquesGeorge Hagen, Cesare Tinelli. FMCAD 2008: 1-9 [doi]

2007

2006

A new combination procedure for the word problem that generalizes fusion decidability results in modal logicsFranz Baader, Silvio Ghilardi, Cesare Tinelli. iandc, 204(10):1413-1452, 2006. [doi]

Splitting on Demand in SAT Modulo TheoriesClark Barrett, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli. lpar 2006: 512-526 [doi]

Lemma Learning in the Model Evolution CalculusPeter Baumgartner, Alexander Fuchs, Cesare Tinelli. lpar 2006: 572-586 [doi]

Implementing the Model Evolution CalculusPeter Baumgartner, Alexander Fuchs, Cesare Tinelli. ijait, 15(1):21-52, 2006. [doi]

Intelligent Systems and Formal Methods in Software EngineeringBernhard Beckert, Tony Hoare, Reiner Hähnle, Douglas R. Smith, Cordell Green, Silvio Ranise, Cesare Tinelli, Thomas Ball, Sriram K. Rajamani. expert, 21(6):71-81, 2006. [doi]

Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(::::T::::)Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli. JACM, 53(6):937-977, 2006. [doi]

2005

PrefaceWolfgang Ahrendt, Peter Baumgartner, Hans de Nivelle, Silvio Ranise, Cesare Tinelli. ENTCS, 125(3):1-2, 2005. [doi]

The Model Evolution Calculus with EqualityPeter Baumgartner, Cesare Tinelli. cade 2005: 392-408 [doi]

Combining Nonstably Infinite TheoriesCesare Tinelli, Calogero G. Zarba. JAR, 34(3):209-238, 2005. [doi]

2004

2003

The Model Evolution CalculusPeter Baumgartner, Cesare Tinelli. cade 2003: 350-364 [doi]

Combining Non-Stably Infinite TheoriesCesare Tinelli, Calogero G. Zarba. ENTCS, 86(1), 2003. [doi]

Unions of non-disjoint theories and combinations of satisfiability proceduresCesare Tinelli, Christophe Ringeissen. TCS, 290(1):291-353, 2003.

PrefaceCesare Tinelli, Teodor Rus. TCS, 291(3):219-221, 2003.

Cooperation of Background Reasoners in Theory Reasoning by Residue SharingCesare Tinelli. JAR, 30(1):1-31, 2003.

2002

Combining Decision Procedures for Positive Theories Sharing ConstructorsFranz Baader, Cesare Tinelli. RTA 2002: 352-366 [doi]

Deciding the Word Problem in the Union of Equational TheoriesFranz Baader, Cesare Tinelli. iandc, 178(2):346-390, 2002. [doi]

A DPLL-Based Calculus for Ground Satisfiability Modulo TheoriesCesare Tinelli. jelia 2002: 308-319 [doi]

2000

Combining Equational Theories Sharing Non-Collapse-Free ConstructorsFranz Baader, Cesare Tinelli. frocos 2000: 260-274

1999

Deciding the Word Problem in the Union of Equational Theories Sharing ConstructorsFranz Baader, Cesare Tinelli. RTA 1999: 175-189 [doi]

1998

Constraint Logic Programming over Unions of Constraint TheoriesCesare Tinelli, Mehdi T. Harandi. jflp, 1998(6), 1998.

1997

A New Approach for Combining Decision Procedure for the Word Problem, and Its Connection to the Nelson-Oppen Combination MethodFranz Baader, Cesare Tinelli. cade 1997: 19-33

1996

A New Correctness Proof of the {Nelson-Oppen} Combination ProcedureCesare Tinelli, Mehdi T. Harandi. frocos 1996: 103-119

Constraint Logic Programming over Unions of Constraint TheoriesCesare Tinelli, Mehdi T. Harandi. cp 1996: 436-450