Cesare Tinelli's Publications
Current and Pending Work
| o |
George Hagen
and Cesare Tinelli.
Scaling up the formal verification of Lustre programs with SMT-based techniques.
In
Proceedings of the 8th International Conference on Formal Methods in Computer-Aided Design (FMCAD'08), Portland, Oregon,
2008.
©Springer.
(To appear.)
[ Abstract | Preliminary version | BibTeX ] |
| o |
Peter Baumgartner,
Alexander Fuchs,
Hans de Nivelle,
and
Cesare Tinelli.
Computing Finite Models by Reduction to Function-Free Clause Logic.
Journal of Applied Logic, 2007.
(Accepted for publication.)
(Extended and improved version of [BFNT06].) [ Abstract | Preprint ] |
| o |
Peter Baumgartner,
Alexander Fuchs
and Cesare Tinelli.
Lemma Learning in the Model Evolution Calculus.
Technical report no. 06-04.
Department of Computer Science,
The University of Iowa, 2006.
[ Abstract | Draft ] |
| o |
Silvio Ranise
and Cesare Tinelli.
The SMT-LIB Standard: Version 1.2.
Technical Report.
Department of Computer Science,
The University of Iowa, 2006.
[ Abstract | Paper | BibTeX ] |
Refereed Conferences and Workshops
| [BGT07] |
Yeting Ge,
Clark Barrett,
and Cesare Tinelli.
Solving Quantified Verification Conditions using Satisfiability Modulo Theories
In
Proceedings of the 21st International Conference on Automated Deduction (CADE-21), Bremen, Germany,
2007.
©Springer
[ Abstract | Paper | BibTeX ] |
| [BT07] |
Clark Barrett,
and Cesare Tinelli.
CVC3
In
Proceedings of the 19th International Conference on Computer Aided Verification (CAV'07), Berlin, Germany,
2007.
©Springer
[ Abstract | Paper | BibTeX ] |
| [KGGT07] |
Sava Krstić,
Amit Goel,
Jim Grundy,
and Cesare Tinelli.
Combined Satisfiability Modulo Parametric Theories.
In
Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07),
2007.
©Springer
[ Abstract | Paper | BibTeX ] |
| [BNOT06] |
Clark Barrett,
Robert Nieuwenhuis,
Albert Oliveras, and
Cesare Tinelli.
Splitting on Demand in SAT Modulo Theories.
In
Proceedings of the 13th International Conference on
Logic for Programming, Artificial Intelligence and Reasoning (LPAR'06),
Phnom Penh, Cambodia, 2006.
©Springer
[ Abstract | Paper | BibTeX ] |
| [BFT06] |
Peter Baumgartner,
Alexander Fuchs,
and Cesare Tinelli.
Lemma Learning in the Model Evolution Calculus.
In
Proceedings of the 13th International Conference on
Logic for Programming, Artificial Intelligence and Reasoning (LPAR'06),
Phnom Penh, Cambodia, 2006.
©Springer
[ Abstract | Paper | BibTeX ] |
| [BST06] |
Clark Barrett,
Igor Shikanian,
and Cesare Tinelli.
An Abstract Decision Procedure for Satisfiability in
the Theory of Recursive Data Types.
In
Proceedings of the of the 4th International Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR'06), 2006.
[ Abstract | Paper | BibTeX ] |
| [BFNT06] |
Peter Baumgartner,
Alexander Fuchs,
Hans de Nivelle,
and
Cesare Tinelli.
Computing Finite Models by Reduction to Function-Free Clause Logic.
In
Proceedings of the International Workshop on Disproving (DISPROVING'06), 2006.
[ Abstract | Paper | BibTeX ] |
| [BT05] |
Peter Baumgartner
and Cesare Tinelli.
The Model Evolution Calculus with Equality.
In
Proceedings of the 20th International Conference on Automated Deduction (CADE-20), Tallinn, Estonia,
2005.
©Springer
[ Abstract | Paper | BibTeX ] |
| [NOT05] |
Robert Nieuwenhuis,
Albert Oliveras, and
Cesare Tinelli.
Abstract DPLL and Abstract DPLL Modulo Theories.
In
Proceedings of the 11th International Conference on
Logic for Programming, Artificial Intelligence and Reasoning (LPAR'04),
Montevideo, Uruguay, 2005.
©Springer
[ Abstract | Paper | Extended Version | BibTeX ] |
| [TZ04] |
Cesare Tinelli
and
Calogero Zarba.
Combining decision procedures for sorted theories.
In
Proceedings of the 9th European Conference on
Logic in Artificial Intelligence (JELIA'04),
Lisbon, Portugal, 2004.
©Springer
[ Abstract | Paper | BibTeX ] |
| [BFT04] |
Peter Baumgartner,
Alexander Fuchs
and
Cesare Tinelli.
Darwin: A Theorem Prover for the Model Evolution Calculus.
in
Proceedings of the first Workshop on Empirically Successful First Order Reasoning (ESFOR'04), Cork, Ireland,
2004.
[ Abstract | Paper | BibTeX ] |
| [GHN04] |
Harald Ganzinger,
George Hagen,
Robert Nieuwenhuis,
Albert Oliveras, and
Cesare Tinelli.
DPLL(T): Fast Decision Procedures.
In
Proceedings of the 16th International Conference on Computer Aided Verification (CAV'04), Boston, USA,
2004.
©Springer
[ Abstract | Paper | BibTeX ] |
| [BGT04] |
Franz Baader,
Silvio Ghilardi
and
Cesare Tinelli.
A New Combination procedure for the Word Problem
that Generalizes Fusion Results in Modal Logics.
In
Proceedings of the 2nd International Joint Conference on Automated Reasoning (IJCAR'04), Cork, Ireland,
2004.
©Springer
[ Abstract | Paper | BibTeX ] |
| [BT03] |
Peter Baumgartner
and Cesare Tinelli.
The Model Evolution Calculus.
In
Proceedings of the 19th International Conference on Automated Deduction (CADE-19), Miami, Florida, USA,
2003.
©Springer
[ Abstract | Paper | BibTeX ] |
| [TZ03] |
Cesare Tinelli
and
Calogero Zarba.
Combining non-stably infinite theories.
In
Proceedings of the 4th International Workshop on
First Order Theorem Proving (FTP'03), Valencia, Spain,
2003.
Elsevier Science Publishers.
[ Abstract | Paper | BibTeX | Errata ] |
| [T02] |
Cesare Tinelli.
A DPLL-based Calculus for Ground Satisfiability Modulo Theories.
In
Proceedings of the 8th European Conference on
Logic in Artificial Intelligence
(JELIA'02),
Cosenza, Italy, 2002.
©Springer
[ Abstract | Paper | BibTeX ] |
| [BT02a] |
Franz Baader
and
Cesare Tinelli.
Combining Decision Procedures for Positive Theories Sharing Constructors.
In
Proceedings of the 13th International Conference on
Rewriting Techniques and Applications
(RTA'02),
Copenhagen, Denmark, 2002.
©Springer-Verlag
[ Abstract | Paper | BibTeX ] |
| [T00] |
Cesare Tinelli.
Cooperation of Background Reasoners in Theory Reasoning by Residue Sharing.
In
Proceedings of the International Workshop on First order Theorem Proving (FTP'2000).
[ Abstract | Paper | BibTeX | Errata ] |
| [BT00] |
Franz Baader
and
Cesare Tinelli.
Combining Equational Theories Sharing Non-Collapse-Free Constructors.
Frontiers of Combining Systems (FroCoS'2000).
©Springer-Verlag
(Longer version available in [R99]) [ Abstract | Paper | BibTeX | Errata ] |
| [BT99] |
Franz Baader
and
Cesare Tinelli.
Deciding the Word Problem in the Union of
Equational Theories Sharing Constructors.
In
Proceedings of the 10th International Conference on
Rewriting Techniques and Applications
(RTA-99),
Trento, Italy, 1999.
©Springer-Verlag
(Longer version available in [R98b]) [ Abstract | Paper | BibTeX | Errata ] |
| [BT97] |
Franz Baader
and
Cesare Tinelli.
A New Approach for Combining Decision Procedures for the Word Problem,
and Its Connection to the Nelson-Oppen Combination Method.
Proceedings of the 14th International Conference on Automated Deduction
(CADE-14)
,
Townsville, North Queensland, Australia, 1997.
(Longer version available in [R96]) [ Abstract | Paper | BibTeX ] |
| [TH96b] |
Cesare Tinelli
and
Mehdi Harandi.
Constraint Logic Programming over Unions of Constraint Theories.
Proceedings of the 2nd International Conference on Principles and Practice of
Constraint Programming
(CP'96),
Cambridge, Massachusetts, USA, Aug 19-22, 1996.
[ Abstract | Paper | BibTeX ] |
| [TH96a] |
Cesare Tinelli
and
Mehdi Harandi
A New Correctness Proof of the Nelson-Oppen Combination Procedure.
Proceedings of the 1st International Workshop
``Frontiers of Combining Systems''
(FroCoS'96),
Munich, Germany, March 26-29, 1996.
[ Abstract | Preprint | BibTeX ] |
Journals and Technical Magazines
| [BT08] |
Peter Baumgartner
and Cesare Tinelli.
The Model Evolution Calculus as a
First-Order DPLL Method.
Artificial Intelligence, 172:591-632, 2008.
(Extended and improved version of [BT03].) [ Abstract | Preprint | BibTeX ] |
| [BST07] |
Clark Barrett,
Igor Shikanian,
and Cesare Tinelli.
An Abstract Decision Procedure for Satisfiability in
the Theory of Inductive Data Types.
Journal on Satisfiability, Boolean Modeling and Computation, 3:1-17, 2007.
(Extended and improved version of [BST06].) [ Abstract | Paper | BibTeX ] |
| [NOT06] |
Robert Nieuwenhuis,
Albert Oliveras, and
Cesare Tinelli.
Solving SAT and SAT Modulo Theories: from an Abstract
Davis-Putnam-Logemann-Loveland Procedure to DPLL(T).
Journal of the ACM, 53(6):937-977, November 2006.
(Extended and improved version of [NOT05].) [ Abstract | Preprint | BibTeX ] |
| [RT06] |
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.
In
Trends and Controversies - IEEE Intelligent Systems Magazine,
21(6):71-81, November/December 2006. [ Preprint of section on SMT ] |
| [BGT06] |
Franz Baader,
Silvio Ghilardi
and
Cesare Tinelli.
A New Combination procedure for the Word Problem
that Generalizes Fusion Results in Modal Logics.
Information and Computation.
Special Issue on Combining Logical Systems,
240(10):1413-1452,
October 2006.
(Extended version of [BGT04].) [ Abstract | Preprint | BibTeX ] |
| [BFT06] |
Peter Baumgartner,
Alexander Fuchs
and
Cesare Tinelli.
Implementing the Model Evolution Calculus.
International Journal of Artificial Intelligence Tools,
15(1):21-52, February 2006.
(Extended version of [BFT04].) [ Abstract | Preprint | BibTeX ] |
| [TZ05] |
Cesare Tinelli
and
Calogero Zarba.
Combining nonstably infinite theories.
Journal of Automated Reasoning,
34(3):209-238, April 2005.
(Extended and amended version of [TZ03].) [ Abstract | Preprint | BibTeX ] |
| [T03] |
Cesare Tinelli.
Cooperation of Background Reasoners in Theory Reasoning by Residue Sharing.
Journal of Automated Reasoning
30(1):1-31, January 2003.
(Revised version of [R02b].) [ Abstract | Preprint | BibTeX ] |
| [TR03] |
Cesare Tinelli
and
Christophe Ringeissen.
Unions of Non-Disjoint Theories and Combinations of Satisfiability Procedures.
Theoretical Computer Science,
290(1), 2003.
(Journal version of [R01]) [ Abstract | Preprint | BibTeX ] |
| [BT02] |
Franz Baader
and
Cesare Tinelli.
Deciding the Word Problem in the Union of
Equational Theories Sharing Constructors.
Information and Computation,
178(2), 2002.
(Revised and extended version of [BT97], [BT99] and [BT2000].) [ Abstract | Preprint | BibTeX ] |
| [TH98] |
Cesare Tinelli
and
Mehdi Harandi.
Constraint Logic Programming over Unions of Constraint Theories.
The
Journal of Functional and Logic Programming (6), 1998.
(Revised and extended version of [TH96b]) [ Abstract | Paper | BibTeX ] |
Technical Reports
| [R06] |
Sava Krstić,
Amit Goel,
Jim Grundy
and Cesare Tinelli.
Combined Satisfiability Modulo Parametric Theories.
Technical report, October 2006
(revised January 2007).
[ Abstract | Paper | BibTeX ] |
| [R06a] |
Clark Barrett,
Robert Nieuwenhuis,
Albert Oliveras, and
Cesare Tinelli.
Splitting on Demand in SAT Modulo Theories.
Technical report no. 06-05.
Department of Computer Science,
The University of Iowa, 2006.
[ Abstract | Paper | BibTeX ] |
| [R05] |
Clark Barrett,
Igor Shikanian
and Cesare Tinelli.
An Abstract Decision Procedure for Satisfiability in
the Theory of Recursive Data Types.
Technical Report no. TR2005-878,
Department of Computer Science, New York University,
Nov 2005.
[ Abstract | Paper | BibTeX ] |
| [R04b] |
Vijay Ganesh,
Sergey Berezin,
Cesare Tinelli,
David L. Dill.
Combination Results for Many-Sorted Theories with Overlapping Signatures.
Technical Report.
Department of Computer Science, Stanford University,
2004.
[ Abstract | Draft | BibTeX ] |
| [R04a] |
Cesare Tinelli
and
Calogero Zarba.
Combining decision procedures for theories in sorted logics.
Technical Report no. 04-01, Department of Computer Science,
The University of Iowa,
2004.
[ Abstract | Paper | BibTeX ] |
| [R03c] |
Franz Baader,
Silvio Ghilardi
and
Cesare Tinelli.
A New Combination procedure for the Word Problem
that Generalizes Fusion Results in Modal Logics.
Technical Report no. 03-03,
Department of Computer Science,
The University of Iowa,
2003.
(Extended version of [BGT04]) [ Abstract | Paper | BibTeX ] |
| [R03b] |
Peter Baumgartner
and Cesare Tinelli.
The Model Evolution Calculus.
Technical Report no. 1/2003,
Institut für Informatik,
Universität Koblenz-Landau,
2003.
[ Abstract | Paper | BibTeX ] |
| [R03a] |
Cesare Tinelli
and
Calogero Zarba.
Combining non-stably infinite theories.
Technical Report no. 03-01,
Department of Computer Science,
The University of Iowa,
2003.
(Extended version of [TZ03])
[ Abstract | Paper | BibTeX ] |
| [R02c] |
Cesare Tinelli.
A DPLL-based calculus for ground satisfiability modulo theories.
Technical Report,
Department of Computer Science,
University of Iowa,
2002.
(Extended version of [T02].) [ Note ] |
| [R02b] |
Cesare Tinelli.
Cooperation of Background Reasoners in Theory Reasoning by Residue Sharing.
Technical Report no. 02-03,
Department of Computer Science,
University of Iowa,
2002.
(Extended version of [T00].) [ Abstract | Paper | BibTeX ] |
| [R02a] |
Franz Baader
and
Cesare Tinelli.
Combining Decision Procedures for
Positive Theories Sharing Constructors.
Technical Report no. 02-02,
Department of Computer Science,
University of Iowa,
2002.
[ Abstract | Paper | BibTeX ] |
| [R01] |
Cesare Tinelli
and
Christophe Ringeissen.
Unions of Non-Disjoint Theories and Combinations of Satisfiability Procedures.
Technical Report no. 01-02,
Department of Computer Science,
University of Iowa,
April 2001.
(Revised and extended version of [R98a]) [ Abstract | Paper | BibTeX ] |
| [R99] |
Franz Baader
and
Cesare Tinelli.
Combining Equational Theories
Sharing Non-Collapse-Free Constructors.
Technical Report no. 99-13,
Department of Computer Science,
University of Iowa, October 1999.
[ Abstract | Paper | BibTeX ] |
| [R98b] |
Franz Baader
and
Cesare Tinelli.
Deciding the Word Problem in the Union of Equational Theories
Technical Report no. UIUCDCS-R-98-2073, Department of Computer Science, University of Illinois at Urbana-Champaign, October 1998.
[ Abstract | Paper | BibTeX ] |
| [R98a] |
Cesare Tinelli
and
Christophe Ringeissen.
Non-Disjoint Unions of Theories and Combinations of Satisfiability Procedures:
First results.
Technical Report no. UIUCDCS-R-98-2044,
Department of Computer Science,
University of Illinois at Urbana-Champaign,
April 1998
(also available as INRIA Research Report no.
RR-3402).
(Superseded by [R01]) [ Abstract | Paper | BibTeX ] |
| [R96] |
Franz Baader
and
Cesare Tinelli.
A New Approach for Combining Decision Procedures for the Word Problem,
and Its Connection to the Nelson-Oppen Combination Method.
Technical Report no. 96-01,
LuFG Theoretical Computer Science, RWTH-Aachen, Germany,
[ Abstract | Paper | BibTeX ] |
Other
| [BT02b] | Franz Baader and Cesare Tinelli, ACU-unification with a successor symbol, In Proceedings of the 16th International Workshop on Unification (UNIF 2002), 2002. |
| [Tin01a] | Cesare Tinelli, Combining Decision Procedures for Positive Theories, In Proceedings of the 15th International Workshop on Unification (UNIF 2001), 2001. |
| [BT00a] | Franz Baader and Cesare Tinelli, Combining Decision Procedures for the Word Problem, In Proceedings of the 14th International Workshop on Unification (UNIF 2000), 2000. |
| [Tin99] | Cesare Tinelli, Combining Satisfiability Procedures for Automated Deduction and Constraint-based Reasoning, PhD Dissertation, Department of Computer Science, University of Illinois at Urbana-Champaign, May 1999. |
| [Tin95] | Cesare Tinelli, Extending the CLP Scheme to Unions of Constraint Theories, Master's Thesis, Department of Computer Science, University of Illinois at Urbana-Champaign, October 1995. |