Cesare Tinelli's Publications



Please see the following up-to-date list of publications.

You can also check BDLP and Google Scholar.

Current and Pending Work


Conferences and Workshops

[B-T19b] Haniel Barbosa, Andrew Reynolds, Daniel Larraz and Cesare Tinelli. Extending enumerative function synthesis via SMT-driven classification. In Proceedings of the 19th conferences on Formal Methods in Computer-Aided Design (FMCAD'19), San Jose, CA, USA, 2019. DOI 10.23919/FMCAD.2019.8894267.
[ Abstract | Paper | BibTeX ]
[E-T19] Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark Barrett and Cesare Tinelli. Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract). In Proceedings of the sixth Workshop on Proof eXchange for Theorem Proving (PxTP 2019), Natal, Brazil, 2019. DOI 10.4204/EPTCS.301.4.
[ Abstract | Paper | BibTeX ]
[B-B19] Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli and Clark Barrett. Extending SMT solvers to Higher-Order Logic. In Proceedings of the 27th International Conference on Automated Deduction (CADE-27), Natal, Brazil, 2019. DOI 10.1007/978-3-030-29436-6_3.
[ Abstract | Paper | BibTeX ]
[N-T19] Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark Barrett and Cesare Tinelli. Towards Bit Width Independent Proofs in SMT Solvers. In Proceedings of the 27th International Conference on Automated Deduction (CADE-27), Natal, Brazil, 2019. DOI 10.1007/978-3-030-29436-6_22.
[ Abstract | Paper | BibTeX ]
[B-T19] Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli Invertibility Conditions for Floating-Point Formulas. In Proceedings of the 31st International Conference on Computer Aided Verification (CAV 2019), New York, NY, USA, 2019. DOI 10.1007/978-3-030-25543-5_8.
[ Abstract | Paper | BibTeX ]
[R-T19a] Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark Barrett, Cesare Tinelli. cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis. In Proceedings of the 31st International Conference on Computer Aided Verification (CAV 2019), New York, NY, USA, 2019. DOI 10.1007/978-3-030-25543-5_5.
[ Abstract | Paper | BibTeX ]
[R-T19b] Andrew Reynolds, Andres Nötzli, Clark Barrett, Cesare Tinelli. High-Level Abstractions for Simplifying Extended String Constraints in SMT. In Proceedings of the 31st International Conference on Computer Aided Verification (CAV 2019), New York, NY, USA, 2019. DOI 10.1007/978-3-030-25543-5_2.
[ Abstract | Paper | BibTeX ]
[N-T19] Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark W. Barrett, Cesare Tinelli. Syntax-Guided Rewrite Rule Enumeration for SMT Solvers. In Proceedings of the 22nd International Conference on Theory and Applications of Satisfiability Testing (SAT 2019), Lisbon, Portugal, 2019. DOI 10.1007/978-3-030-24258-9_20.
[ Abstract | Paper | BibTeX ]
[R-B18] Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, Clark Barrett. Datatypes with Shared Selectors. In Proceedings of the 9th International Joint Conference on Automated Reasoning (IJCAR 2018), Oxford, UK, 2018. DOI 10.1007/978-3-319-94205-6_39.
[ Abstract | Paper | BibTeX ]
[N-T18] Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli. Solving Quantified Bit-Vectors Using Invertibility Conditions. In Proceedings of the 30th International Conference on Computer Aided Verification (CAV 2018), Oxford, UK, . DOI 10.1007/978-3-319-96142-2_16.
[ Abstract | Paper | BibTeX ]
[RTJB17] Andrew Reynolds, Cesare Tinelli, Dejan Jovanovic and Clark Barrett. Designing Theory Solvers with Extensions. In Proceedings of the 11th International Symposium on Frontiers of Combining Systems (FroCoS 2017), Brasilia, Brazil, 2017. Invited paper. DOI 10.1007/978-3-319-66167-4_2.
[ Abstract | Paper | BibTeX ]
[MRTB17] Baoluo Meng, Andrew Reynolds, Cesare Tinelli, and Clark Barrett. Relational Constraint Solving in SMT. In Proceedings of the 26th International Conference on Automated Deduction (CADE-26), Gothenburg, Sweden, 2017. DOI 10.1007/978-3-319-63046-5_10.
[ Abstract | Paper | BibTeX ]
[E-B17] Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, and Clark Barrett. SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. In Proceedings of the 29th International Conference on Computer Aided Verification (CAV 2017), Heidelberg, Germany, 2017. DOI 10.1007/978-3-319-63390-9_7.
[ Abstract | Paper | BibTeX ]
[R-T17] Andrew Reynolds, Maverick Woo, Clark Barrett, David Brumley, Tianyi Liang, and Cesare Tinelli. Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification. In Proceedings of the 29th International Conference on Computer Aided Verification (CAV 2017), Heidelberg, Germany, 2017. DOI 10.1007/978-3-319-63390-9_24.
[ Abstract | Paper | BibTeX ]
[W-S17] Lucas Wagner, Alain Mebsout, Cesare Tinelli, Darren Cofer, and Konrad Slind. Qualification of a Model Checker for Avionics Software Verification. In Proceedings of the 9th NASA Formal Methods Symposium (NFM 2017), Moffett Field, CA, USA, 2017. DOI 10.1007/978-3-319-57288-8_29.
[ Abstract | Paper | BibTeX ]
[MT16] Alain Mebsout and Cesare Tinelli. Proof Certificates for SMT-based Model Checkers for Infinite-state Systems. In Proceedings of 16th Conference on Formal Methods in Computer-Aided Design (FMCAD 2016), Mountain View, CA, USA, 2016. DOI 10.1109/FMCAD.2016.7886669.
[ Abstract | Paper | BibTeX ]
[K-T16] Guy Katz, Clark Barrett, Cesare Tinelli, Andrew Reynolds, and Liana Hadarean. Lazy Proofs for DPLL(T)-Based SMT Solvers. In Proceedings of 16th Conference on Formal Methods in Computer-Aided Design, Mountain View, CA, USA, 2016. Best paper award. DOI 10.1109/FMCAD.2016.7886666.
[ Abstract | Paper | BibTeX ]
[CMST16] Adrien Champion, Alain Mebsout, Christoph Sticksel, and Cesare Tinelli. The Kind 2 Model-Checker. In Proceedings of 28th International Conference on Computer Aided Verification (CAV'16), Toronto, Canada, 2016. ©Springer. DOI 10.1007/978-3-319-41540-6_29.
[ Abstract | Paper | BibTeX ]
[CGKT16] Adrien Champion, Arie Gurfinkel, Temesghen Kahsai, and Cesare Tinelli. CoCoSpec: A Mode-Aware Contract Language for Reactive Systems. In Proceedings of the 14th International Conference on Software Engineering and Formal Methods (SEFM 2016), Vienna, Austria, 2016. ©Springer. DOI 10.1007/978-3-319-41591-8_24.
[ Abstract | Paper | BibTeX ]
[BRBT16] Kshitij Bansal, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. In Proceedings of the 8th International Joint Conference on Automated Reasoning (IJCAR'16), Coimbra, Portugal, 2016. ©Springer. DOI 10.1007/978-3-319-40229-1_7.
[ Abstract | Paper | BibTeX ]
[RBCT16] Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, and Cesare Tinelli. Model Finding for Recursive Functions in SMT. In Proceedings of the 8th International Joint Conference on Automated Reasoning (IJCAR'16), Coimbra, Portugal, 2016. ©Springer. DOI 10.1007/978-3-319-40229-1_10.
[ Abstract | Paper | BibTeX ]
[E-T16] Burak Ekici, Guy Katz, Chantal Keller, Alain Mebsout, Andrew J. Reynolds, and Cesare Tinelli. Extending SMTCoq, a Certified Checker for SMT (Extended Abstract). In Proceedings of 1st First International Workshop on Hammers for Type Theories (HaTT'16), Coimbra, Portugal, 2016. DOI 10.4204/EPTCS.210.5.
[ Abstract | Paper | BibTeX ]
[H-D15] Liana Hadarean, Clark Barrett, Andrew Reynolds, Cesare Tinelli and Morgan Deters. Fine-grained SMT proofs for the theory of fixed-width bit-vectors. In 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 20), Suva, Fiji, 2015. ©Springer. DOI 10.1007/978-3-662-48899-7_24
[ Abstract | Paper | BibTeX ]
[L-B15] Tianyi Liang, Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli, and Clark Barrett. A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings. In Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FroCoS'15), Wroclaw, Poland, 2015. ©Springer. DOI 10.1007/978-3-319-24246-0_9.
[ Abstract | Paper | BibTeX ]
[R-B15] Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, and Clark Barrett. Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. In Proceedings of the 27th International Conference on Computer Aided Verification (CAV'15), San Francisco, CA, USA, 2015. ©Springer. DOI 10.1007/978-3-319-21668-3_12
[ Abstract | Paper | BibTeX ]
[BTRW15] Martin Brain, Cesare Tinelli, Philipp Rümmer and Thomas Wahl. An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic. In Proceedings of the 22nd IEEE Symposium on Computer Arithmetic (ARITH'15), Lyon, France, 2015. DOI 10.1109/ARITH.2015.26
[ Abstract | Paper | BibTeX ]
[KBT14] Timothy King, Clark Barrett and Cesare Tinelli. Leveraging Linear and Mixed Integer Programming for SMT. In Proceedings of the 14th International Conference on Formal Methods in Computer-Aided Design (FMCAD'14), Lausanne, Switzerland, 2014. IEEE. DOI 10.1109/FMCAD.2014.6987606.
[ Abstract | Paper | BibTeX ]
[KBT14] Andrew Reynolds, Cesare Tinelli and Leonardo De Moura. Finding Conflicting Instances of Quantified Formulas in SMT. In Proceedings of the 14th International Conference on Formal Methods in Computer-Aided Design (FMCAD'14), Lausanne, Switzerland, 2014. IEEE. DOI 10.1109/FMCAD.2014.6987613.
[ Abstract | Paper | BibTeX ]
[SST14] Aaron Stump and Geoff Sutcliffe and Cesare Tinelli. StarExec: a Cross-Community Infrastructure for Logic Solving. In Proceedings of the 7th International Joint Conference on Automated Reasoning (IJCAR'14), Vienna, Austria, 2014. ©Springer. DOI 10.1007/978-3-319-08587-6_28.
[ Abstract | Paper | BibTeX ]
[H-T14] Liana Hadarean, Kshitij Bansal, Dejan Jovanović, Clark Barrett and Cesare Tinelli. A Tale Of Two Solvers: Eager and Lazy Approaches to Bit-vectors. In Proceedings of the 26th International Conference on Computer Aided Verification (CAV'14), Vienna, Austria, 2014. ©Springer. DOI 10.1007/978-3-319-08867-9_45.
[ Abstract | Paper | BibTeX ]
[L-D14] Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark Barrett and Morgan Deters. A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions. In Proceedings of the 26th International Conference on Computer Aided Verification (CAV'14), Vienna, Austria, 2014. ©Springer. DOI 10.1007/978-3-319-08867-9_43.
[ Abstract | Paper | BibTeX ]
[R-B13] Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstić, Morgan Deters and Clark Barrett. Quantifier Instantiation Techniques for Finite Model Finding in SMT. In Proceedings of the 24th International Conference on Automated Deduction (CADE-24), Lake Placid, NY, USA, 2013. ©Springer. DOI 10.1007/978-3-642-38574-2_26.
[ Abstract | Paper | BibTeX ]
[RTGK13] Andrew Reynolds, Cesare Tinelli, Amit Goel and Sava Krstić. Finite Model Finding in SMT. In Proceedings of the 25th International Conference on Computer Aided Verification (CAV'13), St Petersburg, Russia, 2013. ©Springer. DOI 10.1007/978-3-642-39799-8_42
[ Abstract | Paper | BibTeX ]
[GKT13] Pierre-Loïc Garoche, Temesghen Kahsai and Cesare Tinelli. Incremental Invariant Generation using Logic-based Automatic Abstract Transformers. In Proceedings of the 5th NASA Formal Methods Symposium (NFM'13), Moffett Field, CA, USA, 2013. ©Springer. DOI 10.1007/978-3-642-38088-4_10.
[ Abstract | Paper | BibTeX ]
[LT12] Tianyi Liang and Cesare Tinelli. Exploiting parallelism in the ME calculus. In Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning (PAAR'12), Manchester, UK, 2012.
[ Abstract | Paper ]
[SATA12] Aaron Stump, Andrew Reynolds, Cesare Tinelli, Austin Laugesen, Harley Eades, Corey Oliver, Ruoyu Zhang. LFSC for SMT Proofs: Work in Progress. In Proceedings of the 2nd International Workshop on Proof eXchange for Theorem Proving (PxTP'12), Manchester, UK, 2012.
[ Abstract | Paper ]
[KGTW12] Temesghen Kahsai, Pierre-Loïc Garoche, Cesare Tinelli and Mike Whalen. Incremental verification with mode variable invariants in state machines. In Proceedings of the 4th NASA Formal Methods Symposium (NFM'12), Norfolk, Virginia, USA, 2012. ©Springer
DOI 10.1007/978-3-642-28891-3_35
[ Abstract | Paper | BibTeX ]
[BT11] Peter Baumgartner and Cesare Tinelli. Model Evolution with Equality Modulo Built-in Theories. In Proceedings of the 23rd International Conference on Automated Deduction (CADE-23), Wrocław, Poland, 2011. ©Springer
DOI 10.1007/978-3-642-22438-6_9
[ Abstract | Paper | BibTeX ]
[B11] Clark Barrett, Christopher Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, and Cesare Tinelli. CVC4. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV'11), Snowbird, Utah, 2011. ©Springer
DOI 10.1007/978-3-642-22110-1_14
[ Abstract | Paper | BibTeX ]
[RTH11] Andrew Reynolds, Cesare Tinelli and Liana Hadarean. Certified Interpolant Generation for EUF. In Proceedings of the 9th International Workshop on Satisfiability Modulo Theories (SMT'11), Snowbird, USA, 2011.
[ Abstract | Paper | BibTeX ]
[KGT11] Temesghen Kahsai and Cesare Tinelli. PKIND: A parallel k-induction based model checker. In Proceedings of 10th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC'11), Snowbird, USA, 2011. EPTCS.
[ Abstract | Paper | BibTeX ]
[KGT11] Temesghen Kahsai, Yeting Ge and Cesare Tinelli. Instantiation-Based Invariant Discovery. In Proceedings of the 3rd NASA Formal Methods Symposium (NFM'11), Pasadena, CA, 2011. ©Springer
DOI 10.1007/978-3-642-20398-5_15
[ Abstract | Paper | BibTeX ]
[BST10] Clark Barrett, Aaron Stump and Cesare Tinelli. The SMT-LIB Standard: Version 2.0. In Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (SMT'10), Edinburgh, UK, 2010.
[ Abstract | Paper | BibTeX ]
[RHT10] Andrew Reynolds, Liana Hadarean, Cesare Tinelli, Yeting Ge, Aaron Stump and Clark Barrett. Comparing Proof Systems for Linear Real Arithmetic with LFSC. In Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (SMT'10), Edinburgh, UK, 2010.
[ Abstract | Paper | BibTeX ]
[GKT09] Amit Goel, Sava Krstić and Cesare Tinelli. Ground Interpolation for Combined Theories. In Proceedings of the 22nd International Conference on Automated Deduction (CADE-22), Montreal, Canada, 2009. ©Springer
[ Abstract | Paper | BibTeX ]
[FGG09] Alexander Fuchs, Amit Goel, Jim Grundy, Sava Krstić, and Cesare Tinelli. Ground Interpolation for the Theory of Equality. In Proceedings of the 15th Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'09), York, UK, 2009. ©Springer
[ Abstract | Paper | BibTeX ]
[BFT08] Peter Baumgartner Alexander Fuchs and Cesare Tinelli. ME(LIA) - Model Evolution With Linear Integer Arithmetic Constraints. In Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'08), Doha, Qatar, 2008. ©Springer
[ Abstract | Paper | BibTeX ]
[HT08] 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. IEEE, 2008.
[ Abstract | Preprint | BibTeX ]
[GBT07] 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 13th Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07), Braga, Portugal, 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

[BBRT18] Kshitij Bansal, Clark Barrett, Andrew Reynolds, Cesare Tinelli. Reasoning with Finite Sets and Cardinality Constraints in SMT. Logical Methods in Computer Science 14(4), 2018. DOI 10.23638/LMCS-14(4:12)2018.
[ Abstract | Paper | BibTeX ]
[RTB17] Andrew Reynolds, Cesare Tinelli, Clark Barrett. Constraint solving for finite model finding in SMT solvers. Theory and Practice of Logic Programming 17(4): 516-558, 2017.
DOI 10.1017/S1471068417000175. [ Abstract | Preprint | BibTeX ]
[T-T16] Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze, Cesare Tinelli, Clark Barrett, and Morgan Deters. An efficient SMT solver for string constraints. Formal Methods in System Design 48(3): 206–234, 2016.
DOI 10.1007/s10703-016-0247-6.
(Extended and improved version of [L-D14].)
[ Abstract | Preprint | BibTeX ]
[S-T13] Aaron Stump, Duckki Oe, Andrew Reynolds, Liana Hadarean, and Cesare Tinelli. SMT Proof Checking Using a Logical Framework. Formal Methods in System Design. 42(1):91-118, February 2013.
DOI 10.1007/s10703-012-0163-3.
[ Abstract | Preprint | BibTeX ]
[BPT12] Peter Baumgartner, Bjoern Pelzer, and Cesare Tinelli. Model Evolution with Equality -- Revised and Implemented. Journal of Symbolic Computation, 47:1011-1045, 2012. Special Issue on First Order Theorem Proving.
DOI 10.1016/j.jsc.2011.12.031.
(Substantial reworking of [BT05].)
[ Abstract | Preprint | BibTeX ]
[FGG12] Alexander Fuchs, Amit Goel, Jim Grundy, Sava Krstić, and Cesare Tinelli. Ground interpolation for the theory of equality. Logical Methods in Computer Science, 8 (1:06) 2012, pp. 1–23. Special issue with selected papers from TACAS 2009.
DOI 10.2168/LMCS-8(1:6)2012.
(Extended and improved version of [FGG09].)
[ Abstract | Preprint | BibTeX ]
[GBT09] Yeting Ge, Clark Barrett, and Cesare Tinelli. Solving Quantified Verification Conditions using Satisfiability Modulo Theories Annals of Mathematics and Artificial Intelligence, 55:101-122, 2009.
DOI 10.1007/s10472-009-9153-6. (Extended and improved version of [GBT07].)
[ Abstract | Preprint | BibTeX ]
[BFNT09] Peter Baumgartner Alexander Fuchs, Hans de Nivelle, and Cesare Tinelli. Computing Finite Models by Reduction to Function-Free Clause Logic. Journal of Applied Logic, 7:58-74, 2009.
(Extended and improved version of [BFNT06].)
[ Abstract | Preprint | BibTeX ]
[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 ]

Books

[BT18] Clark Barrett and Cesare Tinelli. Satisfiability Modulo Theories. Chapter on Satisfiability Modulo Theories. In E. Clarke and T. Henzinger, H. Veith, and H., Bloem editors, Handbook of Model Checking. Springer, 2018. DOI 10.1007/978-3-319-10575-8_11
[ Abstract | Preprint | BibTeX ]
[BSST09] Clark Barrett, Roberto Sebastiani, Sanjit Seshia and Cesare Tinelli. Chapter on Satisfiability Modulo Theories. In A. Biere, H. van Maaren and T. Walsh editors, Handbook on Satisfiability. IOS Press, February 2009. DOI 10.3233/978-1-58603-929-5-825
[ Abstract | Preprint | BibTeX ]

Technical Reports

[R15] Tianyi Liang, Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli, and Clark Barrett. A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings. Technical report. Department of Computer Science, The University of Iowa, 2015.
[ Paper | BibTeX ]
[R11] Peter Baumgartner and Cesare Tinelli. Model Evolution with Equality Modulo Built-in Theories. Technical Report. NICTA, 2011.
[ Abstract | Paper | BibTeX ]
[R08] Peter Baumgartner Alexander Fuchs and Cesare Tinelli. ME(LIA) - Model Evolution With Linear Integer Arithmetic Constraints. Technical report no. 08-06. Department of Computer Science, The University of Iowa, 2008.
[ Abstract | Paper | BibTeX ]
[R06c] Sava Krstić, Amit Goel, Jim Grundy and Cesare Tinelli. Combined Satisfiability Modulo Parametric Theories. Technical report, October 2006 (revised January 2007).
[ Abstract | Paper | BibTeX ]
[R06b] 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 ]
[R06a] 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 | Paper | BibTeX ]
[R05b] Peter Baumgartner and Cesare Tinelli. The Model Evolution Calculus with Equality. Technical report, 2005.
[ Abstract | Paper | BibTeX ]
[R05a] 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.













Main Page
Publications

  Current Work

  Conferences &
  Workshops

  Journals

  Books

  Tech Reports

  Other