Cesare Tinelli

According to our database1, Cesare Tinelli
  • authored at least 90 papers between 1996 and 2017.
  • has a "Dijkstra number"2 of three.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepage:

On csauthors.net:

Bibliography

2017
Constraint solving for finite model finding in SMT solvers.
TPLP, 2017

Some advances in tools and algorithms for the construction and analysis of systems.
STTT, 2017

Constraint Solving for Finite Model Finding in SMT Solvers.
CoRR, 2017

A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT.
CoRR, 2017

Special issue of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015).
Acta Inf., 2017

Qualification of a Model Checker for Avionics Software Verification.
Proceedings of the NASA Formal Methods - 9th International Symposium, 2017

Designing Theory Solvers with Extensions.
Proceedings of the Frontiers of Combining Systems - 11th International Symposium, 2017

Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017

SMTCoq: A Plug-In for Integrating SMT Solvers into Coq.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017

Relational Constraint Solving in SMT.
Proceedings of the Automated Deduction - CADE 26, 2017

2016
An efficient SMT solver for string constraints.
Formal Methods in System Design, 2016

Extending SMTCoq, a Certified Checker for SMT (Extended Abstract).
Proceedings of the Proceedings First International Workshop on Hammers for Type Theories, 2016

CoCoSpec: A Mode-Aware Contract Language for Reactive Systems.
Proceedings of the Software Engineering and Formal Methods - 14th International Conference, 2016

Efficient solving of string constraints for security analysis.
Proceedings of the Symposium and Bootcamp on the Science of Security, 2016

Proof certificates for SMT-based model checkers for infinite-state systems.
Proceedings of the 2016 Formal Methods in Computer-Aided Design, 2016

Lazy proofs for DPLL(T)-based SMT solvers.
Proceedings of the 2016 Formal Methods in Computer-Aided Design, 2016

The Kind 2 Model Checker.
Proceedings of the Computer Aided Verification - 28th International Conference, 2016

Model Finding for Recursive Functions in SMT.
Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT.
Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

2015
On Counterexample Guided Quantifier Instantiation for Synthesis in CVC4.
CoRR, 2015

Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings.
Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

Counterexample-Guided Quantifier Instantiation for Synthesis in SMT.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic.
Proceedings of the 22nd IEEE Symposium on Computer Arithmetic, 2015

2014
Leveraging Linear and Mixed Integer Programming for SMT.
Proceedings of the 12th International Workshop on Satisfiability Modulo Theories, 2014

Finding conflicting instances of quantified formulas in SMT.
Proceedings of the Formal Methods in Computer-Aided Design, 2014

A tour of CVC4: How it works, and how to use it.
Proceedings of the Formal Methods in Computer-Aided Design, 2014

Leveraging linear and mixed integer programming for SMT.
Proceedings of the Formal Methods in Computer-Aided Design, 2014

A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014

A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014

StarExec: A Cross-Community Infrastructure for Logic Solving.
Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

2013
SMT proof checking using a logical framework.
Formal Methods in System Design, 2013

Incremental Invariant Generation Using Logic-Based Automatic Abstract Transformers.
Proceedings of the NASA Formal Methods, 2013

Finite Model Finding in SMT.
Proceedings of the Computer Aided Verification - 25th International Conference, 2013

Quantifier Instantiation Techniques for Finite Model Finding in SMT.
Proceedings of the Automated Deduction - CADE-24, 2013

2012
Model Evolution with equality - Revised and implemented.
J. Symb. Comput., 2012

Invariant stream generators using automatic abstract transformers based on a decidable logic
CoRR, 2012

Ground interpolation for the theory of equality
Logical Methods in Computer Science, 2012

SMT-Based Model Checking.
Proceedings of the NASA Formal Methods, 2012

Incremental Verification with Mode Variable Invariants in State Machines.
Proceedings of the NASA Formal Methods, 2012

Introducing StarExec: a Cross-Community Infrastructure for Logic Solving.
Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, 2012

Exploiting parallelism in the ME calculus.
Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning, 2012

2011
PKind: A parallel k-induction based model checker
Proceedings of the Proceedings 10th International Workshop on Parallel and Distributed Methods in verifiCation, 2011

Instantiation-Based Invariant Discovery.
Proceedings of the NASA Formal Methods, 2011

CVC4.
Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

Model Evolution with Equality Modulo Built-in Theories.
Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

2010
Foundations of Satisfiability Modulo Theories.
Proceedings of the Logic, 2010

The SMT-LIB Initiative and the Rise of SMT - (HVC 2010 Award Talk).
Proceedings of the Hardware and Software: Verification and Testing, 2010

2009
Satisfiability Modulo Theories.
Proceedings of the Handbook of Satisfiability, 2009

Computing finite models by reduction to function-free clause logic.
J. Applied Logic, 2009

Solving quantified verification conditions using satisfiability modulo theories.
Ann. Math. Artif. Intell., 2009

Ground Interpolation for the Theory of Equality.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2009

Ground Interpolation for Combined Theories.
Proceedings of the Automated Deduction, 2009

2008
The model evolution calculus as a first-order DPLL method.
Artif. Intell., 2008

(LIA) - Model Evolution with Linear Integer Arithmetic Constraints.
Proceedings of the Logic for Programming, 2008

Scaling Up the Formal Verification of Lustre Programs with SMT-Based Techniques.
Proceedings of the Formal Methods in Computer-Aided Design, 2008

2007
An Abstract Decision Procedure for a Theory of Inductive Data Types.
JSAT, 2007

An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types.
Electr. Notes Theor. Comput. Sci., 2007

Combined Satisfiability Modulo Parametric Theories.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

An Abstract Framework for Satisfiability Modulo Theories.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2007

CVC3.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007

Trends and Challenges in Satisfiability Modulo Theories.
Proceedings of 4th International Verification Workshop in connection with CADE-21, 2007

Solving Quantified Verification Conditions Using Satisfiability Modulo Theories.
Proceedings of the Automated Deduction, 2007

2006
Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T).
J. ACM, 2006

Implementing the Model Evolution Calculus.
International Journal on Artificial Intelligence Tools, 2006

A new combination procedure for the word problem that generalizes fusion decidability results in modal logics.
Inf. Comput., 2006

Intelligent Systems and Formal Methods in Software Engineering.
IEEE Intelligent Systems, 2006

Lemma Learning in the Model Evolution Calculus.
Proceedings of the Logic for Programming, 2006

Splitting on Demand in SAT Modulo Theories.
Proceedings of the Logic for Programming, 2006

2005
Combining Nonstably Infinite Theories.
J. Autom. Reasoning, 2005

Preface.
Electr. Notes Theor. Comput. Sci., 2005

The Model Evolution Calculus with Equality.
Proceedings of the Automated Deduction, 2005

2004
Abstract DPLL and Abstract DPLL Modulo Theories.
Proceedings of the Logic for Programming, 2004

Combining Decision Procedures for Sorted Theories.
Proceedings of the Logics in Artificial Intelligence, 9th European Conference, 2004

DPLL( T): Fast Decision Procedures.
Proceedings of the Computer Aided Verification, 16th International Conference, 2004

A New Combination Procedure for the Word Problem That Generalizes Fusion Decidability Results in Modal Logics.
Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

2003
Preface.
Theor. Comput. Sci., 2003

Unions of non-disjoint theories and combinations of satisfiability procedures.
Theor. Comput. Sci., 2003

Cooperation of Background Reasoners in Theory Reasoning by Residue Sharing.
J. Autom. Reasoning, 2003

Combining Non-Stably Infinite Theories.
Electr. Notes Theor. Comput. Sci., 2003

The Model Evolution Calculus.
Proceedings of the Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28, 2003

2002
Deciding the Word Problem in the Union of Equational Theories.
Inf. Comput., 2002

Combining Decision Procedures for Positive Theories Sharing Constructors.
Proceedings of the Rewriting Techniques and Applications, 13th International Conference, 2002

A DPLL-Based Calculus for Ground Satisfiability Modulo Theories.
Proceedings of the Logics in Artificial Intelligence, European Conference, 2002

2000
Combining Equational Theories Sharing Non-Collapse-Free Constructors.
Proceedings of the Frontiers of Combining Systems, 2000

1999
Deciding the Word Problem in the Union of Equational Theories Sharing Constructors.
Proceedings of the Rewriting Techniques and Applications, 10th International Conference, 1999

1998
Constraint Logic Programming over Unions of Constraint Theories.
Journal of Functional and Logic Programming, 1998

1997
A New Approach for Combining Decision Procedure for the Word Problem, and Its Connection to the Nelson-Oppen Combination Method.
Proceedings of the Automated Deduction, 1997

1996
A New Correctness Proof of the {Nelson-Oppen} Combination Procedure.
Proceedings of the Frontiers of Combining Systems, 1996

Constraint Logic Programming over Unions of Constraint Theories.
Proceedings of the Second International Conference on Principles and Practice of Constraint Programming, 1996


  Loading...