Cesare Tinelli

Aaron Stump, Duckki Oe, Andrew Reynolds, Liana Hadarean, Cesare Tinelli: SMT proof checking using a logical framework. Formal Methods in System Design 42(1): 91-118 (2013)

Alexander Fuchs, Amit Goel, Jim Grundy, Sava Krstic, Cesare Tinelli: Ground interpolation for the theory of equality. Logical Methods in Computer Science 8(1) (2012)

Peter Baumgartner, Björn Pelzer, Cesare Tinelli: Model Evolution with equality - Revised and implemented. J. Symb. Comput. 47(9): 1011-1045 (2012)

Aaron Stump, Geoff Sutcliffe, Cesare Tinelli: Introducing StarExec: a Cross-Community Infrastructure for Logic Solving. COMPARE 2012: 2

Cesare Tinelli: SMT-Based Model Checking. NASA Formal Methods 2012: 1

Temesghen Kahsai, Pierre-Loïc Garoche, Cesare Tinelli, Mike Whalen: Incremental Verification with Mode Variable Invariants in State Machines. NASA Formal Methods 2012: 388-402

Pierre-Loïc Garoche, Temesghen Kahsai, Cesare Tinelli: Invariant stream generators using automatic abstract transformers based on a decidable logic. CoRR abs/1205.3758 (2012)

Peter Baumgartner, Cesare Tinelli: Model Evolution with Equality Modulo Built-in Theories. CADE 2011: 85-100

Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, Cesare Tinelli: CVC4. CAV 2011: 171-177

Temesghen Kahsai, Yeting Ge, Cesare Tinelli: Instantiation-Based Invariant Discovery. NASA Formal Methods 2011: 192-206

Temesghen Kahsai, Cesare Tinelli: PKind: A parallel k-induction based model checker. PDMC 2011: 55-62

Cesare Tinelli, Viorica Sofronie-Stokkermans (Eds.): Frontiers of Combining Systems, 8th International Symposium, FroCoS 2011, Saarbrücken, Germany, October 5-7, 2011. Proceedings. Lecture Notes in Computer Science 6989, Springer 2011, isbn 978-3-642-24363-9

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

Cesare Tinelli: Foundations of Satisfiability Modulo Theories. WoLLIC 2010: 58

Yeting Ge, Clark W. Barrett, Cesare Tinelli: Solving quantified verification conditions using satisfiability modulo theories. Ann. Math. Artif. Intell. 55(1-2): 101-122 (2009)

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)

Amit Goel, Sava Krstic, Cesare Tinelli: Ground Interpolation for Combined Theories. CADE 2009: 183-198

Alexander Fuchs, Amit Goel, Jim Grundy, Sava Krstic, Cesare Tinelli: Ground Interpolation for the Theory of Equality. TACAS 2009: 413-427

Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, Cesare Tinelli: Satisfiability Modulo Theories. Handbook of Satisfiability 2009: 825-885

Peter Baumgartner, Cesare Tinelli: The model evolution calculus as a first-order DPLL method. Artif. Intell. 172(4-5): 591-632 (2008)

George Hagen, Cesare Tinelli: Scaling Up the Formal Verification of Lustre Programs with SMT-Based Techniques. FMCAD 2008: 1-9

Peter Baumgartner, Alexander Fuchs, Cesare Tinelli: (LIA) - Model Evolution with Linear Integer Arithmetic Constraints. LPAR 2008: 258-273

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)

Clark Barrett, Igor Shikanian, Cesare Tinelli: An Abstract Decision Procedure for a Theory of Inductive Data Types. JSAT 3(1-2): 21-46 (2007)

Yeting Ge, Clark Barrett, Cesare Tinelli: Solving Quantified Verification Conditions Using Satisfiability Modulo Theories. CADE 2007: 167-182

Cesare Tinelli: Trends and Challenges in Satisfiability Modulo Theories. VERIFY 2007

Clark Barrett, Cesare Tinelli: CVC3. CAV 2007: 298-302

Cesare Tinelli: An Abstract Framework for Satisfiability Modulo Theories. TABLEAUX 2007: 10

Sava Krstic, Amit Goel, Jim Grundy, Cesare Tinelli: Combined Satisfiability Modulo Parametric Theories. TACAS 2007: 602-617

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)

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)

Peter Baumgartner, Alexander Fuchs, Cesare Tinelli: Implementing the Model Evolution Calculus. International Journal on Artificial Intelligence Tools 15(1): 21-52 (2006)

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)

Clark Barrett, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli: Splitting on Demand in SAT Modulo Theories. LPAR 2006: 512-526

Peter Baumgartner, Alexander Fuchs, Cesare Tinelli: Lemma Learning in the Model Evolution Calculus. LPAR 2006: 572-586

Wolfgang Ahrendt, Peter Baumgartner, Hans de Nivelle, Silvio Ranise, Cesare Tinelli: Preface. Electr. Notes Theor. Comput. Sci. 125(3): 1-2 (2005)

Cesare Tinelli, Calogero G. Zarba: Combining Nonstably Infinite Theories. J. Autom. Reasoning 34(3): 209-238 (2005)

Peter Baumgartner, Cesare Tinelli: The Model Evolution Calculus with Equality. CADE 2005: 392-408

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

Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli: DPLL( T): Fast Decision Procedures. CAV 2004: 175-188

Cesare Tinelli, Calogero G. Zarba: Combining Decision Procedures for Sorted Theories. JELIA 2004: 641-653

Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli: Abstract DPLL and Abstract DPLL Modulo Theories. LPAR 2004: 36-50

Cesare Tinelli, Calogero G. Zarba: Combining Non-Stably Infinite Theories. Electr. Notes Theor. Comput. Sci. 86(1): 35-48 (2003)

Cesare Tinelli: Cooperation of Background Reasoners in Theory Reasoning by Residue Sharing. J. Autom. Reasoning 30(1): 1-31 (2003)

Cesare Tinelli, Christophe Ringeissen: Unions of non-disjoint theories and combinations of satisfiability procedures. Theor. Comput. Sci. 290(1): 291-353 (2003)

Cesare Tinelli, Teodor Rus: Preface. Theor. Comput. Sci. 291(3): 219-221 (2003)

Peter Baumgartner, Cesare Tinelli: The Model Evolution Calculus. CADE 2003: 350-364

Franz Baader, Cesare Tinelli: Deciding the Word Problem in the Union of Equational Theories. Inf. Comput. 178(2): 346-390 (2002)

Cesare Tinelli: A DPLL-Based Calculus for Ground Satisfiability Modulo Theories. JELIA 2002: 308-319

Franz Baader, Cesare Tinelli: Combining Decision Procedures for Positive Theories Sharing Constructors. RTA 2002: 352-366

Franz Baader, Cesare Tinelli: Combining Equational Theories Sharing Non-Collapse-Free Constructors. FroCoS 2000: 260-274

Franz Baader, Cesare Tinelli: Deciding the Word Problem in the Union of Equational Theories Sharing Constructors. RTA 1999: 175-189

Cesare Tinelli, Mehdi T. Harandi: Constraint Logic Programming over Unions of Constraint Theories. Journal of Functional and Logic Programming 1998(6) (1998)

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

Cesare Tinelli, Mehdi T. Harandi: Constraint Logic Programming over Unions of Constraint Theories. CP 1996: 436-450

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