Cesare Tinelli
#163,276
Most Influential Person Now
Italian computer scientist
Cesare Tinelli's AcademicInfluence.com Rankings
Cesare Tinellicomputer-science Degrees
Computer Science
#9572
World Rank
#10047
Historical Rank
Automated Reasoning
#19
World Rank
#19
Historical Rank
Software Engineering
#257
World Rank
#262
Historical Rank
Database
#6542
World Rank
#6777
Historical Rank
Download Badge
Computer Science
Cesare Tinelli's Degrees
- PhD Computer Science University of Iowa
- Masters Computer Science University of Iowa
- Bachelors Computer Science Consorzio ICoN
Similar Degrees You Can Earn
Why Is Cesare Tinelli Influential?
(Suggest an Edit or Addition)Cesare Tinelli's Published Works
Number of citations in a given year to any of this author's works
Total number of citations to an author for the works they published in a given year. This highlights publication of the most important work(s) by the author
Published Works
- Satisfiability Modulo Theories (2021) (1342)
- The SMT-LIB Standard Version 2.0 (2010) (976)
- Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T) (2006) (917)
- Handbook of Satisfiability (2021) (533)
- DPLL( T): Fast Decision Procedures (2004) (357)
- Cvc4 (2011) (285)
- The SMT-LIB Standard: Version 1.2 (2005) (213)
- Introducing StarExec: a Cross-Community Infrastructure for Logic Solving (2014) (194)
- A New Correctness Proof of the {Nelson-Oppen} Combination Procedure (1996) (181)
- A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions (2014) (137)
- Solving quantified verification conditions using satisfiability modulo theories (2007) (130)
- Counterexample-Guided Quantifier Instantiation for Synthesis in SMT (2015) (127)
- The Model Evolution Calculus (2003) (127)
- Splitting on Demand in SAT Modulo Theories (2006) (122)
- Abstract DPLL and Abstract DPLL Modulo Theories (2005) (109)
- Scaling Up the Formal Verification of Lustre Programs with SMT-Based Techniques (2008) (105)
- PKind: A parallel k-induction based model checker (2011) (91)
- Unions of non-disjoint theories and combinations of satisfiability procedures (2003) (86)
- A DPLL-Based Calculus for Ground Satisfiability Modulo Theories (2002) (83)
- The Kind 2 Model Checker (2016) (80)
- Computing finite models by reduction to function-free clause logic (2009) (80)
- Implementing the Model Evolution Calculus (2006) (73)
- Quantifier Instantiation Techniques for Finite Model Finding in SMT (2013) (72)
- Combining Nonstably Infinite Theories (2005) (69)
- Finding conflicting instances of quantified formulas in SMT (2014) (67)
- Finite Model Finding in SMT (2013) (62)
- An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic (2015) (61)
- SMT proof checking using a logical framework (2013) (59)
- SMTCoq: A Plug-In for Integrating SMT Solvers into Coq (2017) (57)
- cvc5: A Versatile and Industrial-Strength SMT Solver (2022) (57)
- Darwin: A Theorem Prover for the Model Evolution Calculus (2004) (54)
- A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors (2014) (54)
- An Abstract Decision Procedure for a Theory of Inductive Data Types (2007) (51)
- Combining Decision Procedures for Sorted Theories (2004) (49)
- cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis (2019) (47)
- Combining Non-Stably Infinite Theories (2003) (47)
- The SMT-LIB Format: An Initial Proposal (2003) (47)
- An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types (2007) (46)
- Ground Interpolation for the Theory of Equality (2009) (46)
- The Model Evolution Calculus with Equality (2005) (44)
- A New Combination Procedure for the Word Problem That Generalizes Fusion Decidability Results in Modal Logics (2004) (43)
- The model evolution calculus as a first-order DPLL method (2008) (43)
- Lemma Learning in the Model Evolution Calculus (2006) (42)
- An efficient SMT solver for string constraints (2016) (42)
- Ground Interpolation for Combined Theories (2009) (40)
- Deciding the Word Problem in the Union of Equational Theories (1998) (40)
- Cooperation of Background Reasoners in Theory Reasoning by Residue Sharing (2003) (40)
- Intelligent Systems and Formal Methods in Software Engineering (2006) (39)
- Some advances in tools and algorithms for the construction and analysis of systems (2017) (39)
- A tour of CVC4: How it works, and how to use it (2014) (38)
- A New Approach for Combining Decision Procedure for the Word Problem, and Its Connection to the Nelson-Oppen Combination Method (1997) (37)
- Instantiation-Based Invariant Discovery (2011) (37)
- Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification (2017) (33)
- Description Logic, Theory Combination, and All That (2019) (33)
- (LIA) - Model Evolution with Linear Integer Arithmetic Constraints (2008) (33)
- CoCoSpec: A Mode-Aware Contract Language for Reactive Systems (2016) (32)
- The SMT-LIB Initiative and the Rise of SMT - (HVC 2010 Award Talk) (2010) (30)
- A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT (2016) (29)
- On Solving Quantified Bit-Vectors using Invertibility Conditions (2018) (29)
- Combined Satisfiability Modulo Parametric Theories (2007) (29)
- A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings (2015) (27)
- Extending SMT Solvers to Higher-Order Logic (2019) (27)
- Lazy proofs for DPLL(T)-based SMT solvers (2016) (26)
- Relational Constraint Solving in SMT (2017) (25)
- Model Evolution with Equality Modulo Built-in Theories (2011) (24)
- Model Finding for Recursive Functions in SMT (2016) (24)
- Model Evolution with equality - Revised and implemented (2012) (23)
- Syntax-Guided Rewrite Rule Enumeration for SMT Solvers (2019) (22)
- Incremental Invariant Generation Using Logic-Based Automatic Abstract Transformers (2013) (22)
- Refutation-based synthesis in SMT (2019) (21)
- The SMT-LIB Standard : Version 1 . 0 Working Draft (2004) (20)
- Proof certificates for SMT-based model checkers for infinite-state systems (2016) (19)
- On Counterexample Guided Quantifier Instantiation for Synthesis in CVC4 (2015) (18)
- Designing Theory Solvers with Extensions (2017) (17)
- Constraint Logic Programming over Unions of Constraint Theories (1996) (17)
- Leveraging linear and mixed integer programming for SMT (2014) (17)
- Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors (2015) (15)
- SMT-Based Model Checking (2012) (15)
- Finite model finding in satisfiability modulo theories (2013) (14)
- Deciding the Word Problem in the Union of Equational Theories Sharing Constructors (1999) (14)
- Comparing proof systems for linear real arithmetic LFSC (2010) (13)
- SyGuS Techniques in the Core of an SMT Solver (2017) (13)
- Combining Decision Procedures for Positive Theories Sharing Constructors (2002) (13)
- Extending SMTCoq, a Certified Checker for SMT (Extended Abstract) (2016) (13)
- Incremental Verification with Mode Variable Invariants in State Machines (2012) (13)
- Certified Interpolant Generation for EUF (2011) (12)
- Combining Equational Theories Sharing Non-Collapse-Free Constructors (2000) (12)
- Non-Disjoint Unions of Theories and Combinations of Satisfiability Procedures: First Results (1998) (12)
- Extending enumerative function synthesis via SMT-driven classification (2019) (12)
- Towards Bit-Width-Independent Proofs in SMT Solvers (2019) (11)
- Datatypes with Shared Selectors (2018) (11)
- High-Level Abstractions for Simplifying Extended String Constraints in SMT (2019) (11)
- Qualification of a Model Checker for Avionics Software Verification (2017) (10)
- Architectural and Behavioral Analysis for Cyber Security (2019) (10)
- An analysis of incremental assistant capabilities of a software evolution expert system (1991) (10)
- Theory Combination: Beyond Equality Sharing (2019) (9)
- SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces (2020) (9)
- Verification of quasi-synchronous systems with Uppaal (2014) (9)
- Foundations of Satisfiability Modulo Theories (2010) (9)
- Smt-Switch: A Solver-agnostic C++ API for SMT Solving (2020) (8)
- Combining Decision Procedures for Theories in Sorted Logics (2004) (8)
- LFSC for SMT Proofs: Work in Progress (2012) (7)
- Symbolic computation and satisfiability checking (2020) (7)
- CVC4 at the SMT Competition 2018 (2018) (7)
- VERDICT: A Language and Framework for Engineering Cyber Resilient and Safe System (2021) (6)
- Formal Verification of Quasi-Synchronous Systems (2015) (6)
- Invertibility Conditions for Floating-Point Formulas (2019) (6)
- Reasoning with Finite Sets and Cardinality Constraints in SMT (2017) (5)
- Reductions for Strings and Regular Expressions Revisited (2020) (5)
- Invariant stream generators using automatic abstract transformers based on a decidable logic (2012) (4)
- A Decision Procedure for String to Code Point Conversion (2020) (4)
- Combining satisfiability procedures for automated deduction and constraint-based reasoning (1999) (4)
- Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 9035 (2015) (4)
- Trusting Outsourced Components In Flight Critical Systems (2015) (4)
- Bit-Precise Reasoning via Int-Blasting (2022) (3)
- Formal Methods Tool Qualification (2017) (3)
- Higher-Order SMT Solving (Work in Progress) (2018) (3)
- An Abstract Framework for Satisfiability Modulo Theories (2007) (3)
- Towards Satisfiability Modulo Parametric Bit-vectors (2021) (3)
- Syntax-Guided Quantifier Instantiation (2021) (3)
- Even Faster Conflicts and Lazier Reductions for String Solvers (2022) (3)
- On solving quantified bit-vector constraints using invertibility conditions (2021) (3)
- Politeness and Stable Infiniteness: Stronger Together (2021) (3)
- Constraint solving for finite model finding in SMT solvers* (2017) (3)
- Rewrites for SMT Solvers using Syntax-Guided Enumeration ( Work in Progress ) (2018) (2)
- De iding the Word Problem in the Union ofEquational Theories Sharing Constru tors (1999) (2)
- Chapter 33. Satisfiability Modulo Theories (2021) (2)
- Efficient solving of string constraints for security analysis (2016) (2)
- Merit and Blame Assignment with Kind 2 (2021) (2)
- Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description) (2022) (2)
- Flexible Proof Production in an Industrial-Strength SMT Solver (2022) (2)
- Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis (2020) (2)
- Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract) (2019) (2)
- An efficient SMT solver for string constraints (2016) (1)
- Verifying Bit-vector Invertibility Conditions in Coq (2019) (1)
- Extending SMT solvers to Higher-Order Logic ( Technical Report ) (2019) (1)
- Reasoning About Vectors using an SMT Theory of Sequences (2022) (1)
- Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language (2022) (1)
- Symbolic Computation and Satisfiability Checking Editorial (2019) (1)
- CVC 3 Proof Conversion to LFSC (2010) (1)
- Exploiting parallelism in the ME calculus (2013) (1)
- CVC4SY for SyGuS-COMP 2019 (2019) (1)
- Special issue of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015) (2017) (1)
- An efficient DPLL(T) solver for a theory of strings and regular expressions (2015) (1)
- CVC4 at the SMT Competition 2020 (2020) (1)
- Frontiers of Combining Systems, 8th International Symposium, FroCoS 2011, Saarbrücken, Germany, October 5-7, 2011. Proceedings (2011) (1)
- Realizability Checking of Contracts with Kind 2 (2022) (1)
- Combination Results for Many SortedTheories with Overlapping (2004) (1)
- Some advances in tools and algorithms for the construction and analysis of systems (2017) (1)
- Preface to the Special Issue on Automated Reasoning Systems (2019) (0)
- Certified Satisfiability Modulo Theories (SMT) Solving for System Verification (2017) (0)
- A New Combination Pro edure for the Word Problem that Generalizes Fusion De idability Results in Modal Logi s (2019) (0)
- L O ] 2 0 Ju n 20 18 CVC 4 at the SMT Competition 2018 (2018) (0)
- Scalable and Accurate SMT-based Model Checking of Data Flow Systems (2013) (0)
- CVC 3 ( Tool Paper ) (2007) (0)
- Trends and Challenges in Satisfiability Modulo Theories (2007) (0)
- Preface to the Special Issue on Automated Reasoning Systems (2019) (0)
- Datatypes with Shared Selectors (Technical Report) (2018) (0)
- Selected Papers from the Workshop on Disproving and the Second International Workshop on Pragmatics of Decision Procedures 2004 (2005) (0)
- Finding Locally Smallest Cut Sets using Max-SMT (2023) (0)
- SMT proof checking using a logical framework (2012) (0)
- Increasing Automation in Coq via Trustworthy Cooperation with External Automated Reasoners: Invited Speaker at the Fifth Workshop on Proof eXchange for Theorem Proving (2017) (0)
- Refutation-based synthesis in SMT (2017) (0)
- Preface (2004) (0)
- NASA / CR – 2017-219371 Formal Methods Tool Qualification (2017) (0)
- CVC 4 SY for SyGuS-COMP 2019 (2019) (0)
- Special issue of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015) (2017) (0)
- Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371) (2017) (0)
- Satisfiability Modulo Finite Fields (2023) (0)
- LO ] 26 M ay 2 01 5 On Counterexample Guided Quantifier Instantiation for Synthesis in CVC 4 ⋆ ⋆ ⋆ (2015) (0)
- Beyond model checking of idealized Lustre in Kind 2 (2023) (0)
- A Tour of Franz Baader's Contributions to Knowledge Representation and Automated Deduction (2019) (0)
- On solving quantified bit-vector constraints using invertibility conditions (2021) (0)
- First Results on How to Certify Subsumptions Computed by the EL Reasoner ELK Using the Logical Framework with Side Conditions (2020) (0)
- Proceedings of the 8th international conference on Frontiers of combining systems (2011) (0)
- Publications of Viktor Kuncak in the Period 2013-today (2018) (0)
- SMTCoq Proof witness Certi fi cate Formula Coq goal Legend : Coq checker + Soundess Preprocessor SMT solver (2018) (0)
- An Abstra t De ision Pro edure for Satis ability in the Theory ofRe ursive Data (2013) (0)
- J un 2 01 5 On Counterexample Guided Quantifier Instantiation for Synthesis in CVC 4 ⋆ ⋆ ⋆ (2018) (0)
- From Declarative to Computational Proof Checking for LRA (2012) (0)
- Deduction Beyond Satisfiability (Dagstuhl Seminar 19371) (2019) (0)
This paper list is powered by the following services:
What Schools Are Affiliated With Cesare Tinelli?
Cesare Tinelli is affiliated with the following schools:
