Cesare Tinelli

CoRR, 2022

Bit-Precise Reasoning via Int-Blasting.

[BibT_eX]

[DOI]

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2022

cvc5: A Versatile and Industrial-Strength SMT Solver.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language.

[BibT_eX]

[DOI]

Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

Even Faster Conflicts and Lazier Reductions for String Solvers.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 34th International Conference, 2022

Reasoning About Vectors Using an SMT Theory of Sequences.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description).

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

Flexible Proof Production in an Industrial-Strength SMT Solver.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

2021

Syntax-Guided Quantifier Instantiation (TACAS 2021 Artifact).

[BibT_eX]

[DOI]

Dataset, February, 2021

Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Satisfiability - Second Edition, 2021

VERDICT: A Language and Framework for Engineering Cyber Resilient and Safe System.

[BibT_eX]

[DOI]

Heber Herencia-Zapana

M. Fareed Arif

Moosa Yahyazadeh

Vidhya Tekken Valapil

Michael Durling

Omar Chowdhury

Syst., 2021

Towards Satisfiability Modulo Parametric Bit-vectors.

[BibT_eX]

[DOI]

J. Autom. Reason., 2021

On solving quantified bit-vector constraints using invertibility conditions.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2021

Syntax-Guided Quantifier Instantiation.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2021

Smt-Switch: A Solver-Agnostic C++ API for SMT Solving.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2021, 2021

Merit and Blame Assignment with Kind 2.

[BibT_eX]

[DOI]

Daniel Larraz

Mickaël Laurent

Proceedings of the Formal Methods for Industrial Critical Systems, 2021

Politeness and Stable Infiniteness: Stronger Together.

[BibT_eX]

[DOI]

Ying Sheng

Yoni Zohar

Christophe Ringeissen

Proceedings of the Automated Deduction - CADE 28, 2021

2020

Symbolic computation and satisfiability checking.

[BibT_eX]

[DOI]

J. Symb. Comput., 2020

Preface to the Special Issue on Automated Reasoning Systems.

[BibT_eX]

[DOI]

Armin Biere

Christoph Weidenbach

J. Autom. Reason., 2020

Smt-Switch: A Solver-agnostic C++ API for SMT Solving.

[BibT_eX]

[DOI]

Proceedings of the 18th International Workshop on Satisfiability Modulo Theories co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020), 2020

Reductions for Strings and Regular Expressions Revisited.

[BibT_eX]

[DOI]

Proceedings of the 2020 Formal Methods in Computer Aided Design, 2020

SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces.

[BibT_eX]

[DOI]

Proceedings of the 2020 Formal Methods in Computer Aided Design, 2020

First Results on How to Certify Subsumptions Computed by the EL Reasoner ELK Using the Logical Framework with Side Conditions.

[BibT_eX]

[DOI]

Patrick Koopmann

Proceedings of the 33rd International Workshop on Description Logics (DL 2020) co-located with the 17th International Conference on Principles of Knowledge Representation and Reasoning (KR 2020), 2020

A Decision Procedure for String to Code Point Conversion.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019

Refutation-based synthesis in SMT.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2019

Deduction Beyond Satisfiability (Dagstuhl Seminar 19371).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2019

Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, 2019

CVC4SY for SyGuS-COMP 2019.

[BibT_eX]

[DOI]

CoRR, 2019

Syntax-Guided Rewrite Rule Enumeration for SMT Solvers.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2019, 2019

Extending enumerative function synthesis via SMT-driven classification.

[BibT_eX]

[DOI]

Proceedings of the 2019 Formal Methods in Computer Aided Design, 2019

High-Level Abstractions for Simplifying Extended String Constraints in SMT.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

Invertibility Conditions for Floating-Point Formulas.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

Towards Bit-Width-Independent Proofs in SMT Solvers.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 27, 2019

Extending SMT Solvers to Higher-Order Logic.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 27, 2019

A Tour of Franz Baader's Contributions to Knowledge Representation and Automated Deduction.

[BibT_eX]

[DOI]

Proceedings of the Description Logic, Theory Combination, and All That, 2019

Theory Combination: Beyond Equality Sharing.

[BibT_eX]

[DOI]

Maria Paola Bonacina

Pascal Fontaine

Christophe Ringeissen

Proceedings of the Description Logic, Theory Combination, and All That, 2019

2018

Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Model Checking., 2018

Reasoning with Finite Sets and Cardinality Constraints in SMT.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2018

CVC4 at the SMT Competition 2018.

[BibT_eX]

[DOI]

CoRR, 2018

Solving Quantified Bit-Vectors Using Invertibility Conditions.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Datatypes with Shared Selectors.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

2017

Constraint solving for finite model finding in SMT solvers.

[BibT_eX]

[DOI]

Theory Pract. Log. Program., 2017

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

[BibT_eX]

[DOI]

Christel Baier

Jasmin Christian Blanchette

Int. J. Softw. Tools Technol. Transf., 2017

Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371).

[BibT_eX]

[DOI]

Carsten Fuhs

Viorica Sofronie-Stokkermans

Dagstuhl Reports, 2017

SyGuS Techniques in the Core of an SMT Solver.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Sixth Workshop on Synthesis, 2017

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

[BibT_eX]

[DOI]

Christel Baier

Acta Informatica, 2017

Qualification of a Model Checker for Avionics Software Verification.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 9th International Symposium, 2017

Designing Theory Solvers with Extensions.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems - 11th International Symposium, 2017

Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 29th International Conference, 2017

SMTCoq: A Plug-In for Integrating SMT Solvers into Coq.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 29th International Conference, 2017

Relational Constraint Solving in SMT.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 26, 2017

2016

An efficient SMT solver for string constraints.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2016

Extending SMTCoq, a Certified Checker for SMT (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the Proceedings First International Workshop on Hammers for Type Theories, 2016

CoCoSpec: A Mode-Aware Contract Language for Reactive Systems.

[BibT_eX]

[DOI]

Proceedings of the Software Engineering and Formal Methods - 14th International Conference, 2016

Efficient solving of string constraints for security analysis.

[BibT_eX]

[DOI]

Proceedings of the Symposium and Bootcamp on the Science of Security, 2016

Proof certificates for SMT-based model checkers for infinite-state systems.

[BibT_eX]

[DOI]

Alain Mebsout

Proceedings of the 2016 Formal Methods in Computer-Aided Design, 2016

Lazy proofs for DPLL(T)-based SMT solvers.

[BibT_eX]

[DOI]

Proceedings of the 2016 Formal Methods in Computer-Aided Design, 2016

The Kind 2 Model Checker.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 28th International Conference, 2016

Model Finding for Recursive Functions in SMT.

[BibT_eX]

[DOI]

Jasmin Christian Blanchette

Simon Cruanes

Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

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

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

2015

On Counterexample Guided Quantifier Instantiation for Synthesis in CVC4.

[BibT_eX]

[DOI]

CoRR, 2015

Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

Counterexample-Guided Quantifier Instantiation for Synthesis in SMT.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic.

[BibT_eX]

[DOI]

Proceedings of the 22nd IEEE Symposium on Computer Arithmetic, 2015

2014

Leveraging Linear and Mixed Integer Programming for SMT.

[BibT_eX]

[DOI]

Tim King

Proceedings of the 12th International Workshop on Satisfiability Modulo Theories, 2014

Finding conflicting instances of quantified formulas in SMT.

[BibT_eX]

[DOI]

Leonardo Mendonça de Moura

Proceedings of the Formal Methods in Computer-Aided Design, 2014

A tour of CVC4: How it works, and how to use it.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2014

A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 26th International Conference, 2014

A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 26th International Conference, 2014

StarExec: A Cross-Community Infrastructure for Logic Solving.

[BibT_eX]

[DOI]

Aaron Stump

Geoff Sutcliffe

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

2013

SMT proof checking using a logical framework.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2013

Incremental Invariant Generation Using Logic-Based Automatic Abstract Transformers.

[BibT_eX]

[DOI]

Pierre-Loïc Garoche

Proceedings of the NASA Formal Methods, 2013

Finite Model Finding in SMT.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

Quantifier Instantiation Techniques for Finite Model Finding in SMT.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-24, 2013

2012

Model Evolution with equality - Revised and implemented.

[BibT_eX]

[DOI]

Björn Pelzer

J. Symb. Comput., 2012

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

[BibT_eX]

[DOI]

Pierre-Loïc Garoche

CoRR, 2012

Ground interpolation for the theory of equality

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2012

LFSC for SMT Proofs: Work in Progress.

[BibT_eX]

[DOI]

Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, 2012

SMT-Based Model Checking.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods, 2012

Incremental Verification with Mode Variable Invariants in State Machines.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods, 2012

Introducing StarExec: a Cross-Community Infrastructure for Logic Solving.

[BibT_eX]

[DOI]

Aaron Stump

Geoff Sutcliffe

Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, 2012

Exploiting parallelism in the ME calculus.

[BibT_eX]

[DOI]

Tianyi Liang

Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning, 2012

2011

PKind: A parallel k-induction based model checker

[BibT_eX]

[DOI]

Proceedings of the Proceedings 10th International Workshop on Parallel and Distributed Methods in verifiCation, 2011

Instantiation-Based Invariant Discovery.

[BibT_eX]

[DOI]

Yeting Ge

Proceedings of the NASA Formal Methods, 2011

CVC4.

[BibT_eX]

[DOI]

Christopher L. Conway

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

Model Evolution with Equality Modulo Built-in Theories.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

2010

Foundations of Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

Proceedings of the Logic, 2010

The SMT-LIB Initiative and the Rise of SMT - (HVC 2010 Award Talk).

[BibT_eX]

[DOI]

Leonardo Mendonça de Moura

Silvio Ranise

Aaron Stump

Proceedings of the Hardware and Software: Verification and Testing, 2010

2009

Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Satisfiability, 2009

Computing finite models by reduction to function-free clause logic.

[BibT_eX]

[DOI]

J. Appl. Log., 2009

Solving quantified verification conditions using satisfiability modulo theories.

[BibT_eX]

[DOI]

Yeting Ge

Ann. Math. Artif. Intell., 2009

Ground Interpolation for Combined Theories.

[BibT_eX]

[DOI]

Amit Goel

Sava Krstic

Proceedings of the Automated Deduction, 2009

2008

The model evolution calculus as a first-order DPLL method.

[BibT_eX]

[DOI]

Artif. Intell., 2008

(LIA) - Model Evolution with Linear Integer Arithmetic Constraints.

[BibT_eX]

[DOI]

Alexander Fuchs

Proceedings of the Logic for Programming, 2008

Scaling Up the Formal Verification of Lustre Programs with SMT-Based Techniques.

[BibT_eX]

[DOI]

George Hagen

Proceedings of the Formal Methods in Computer-Aided Design, 2008

2007

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

[BibT_eX]

[DOI]

Igor Shikanian

J. Satisf. Boolean Model. Comput., 2007

Combined Satisfiability Modulo Parametric Theories.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

An Abstract Framework for Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2007

CVC3.

[BibT_eX]

[DOI]

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

Trends and Challenges in Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

Proceedings of 4th International Verification Workshop in connection with CADE-21, 2007

2006

Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(<i>T</i>).

[BibT_eX]

[DOI]

Robert Nieuwenhuis

Albert Oliveras

J. ACM, 2006

Implementing the Model Evolution Calculus.

[BibT_eX]

[DOI]

Alexander Fuchs

Int. J. Artif. Intell. Tools, 2006

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

[BibT_eX]

[DOI]

Silvio Ghilardi

Inf. Comput., 2006

Intelligent Systems and Formal Methods in Software Engineering.

[BibT_eX]

[DOI]

IEEE Intell. Syst., 2006

An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types.

[BibT_eX]

[DOI]

Igor Shikanian

Proceedings of the Combined Proceedings of the Fourth Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2006) and the First International Workshop on Probabilistic Automata and Logics (PaUL 2006), 2006

Lemma Learning in the Model Evolution Calculus.

[BibT_eX]

[DOI]

Alexander Fuchs

Proceedings of the Logic for Programming, 2006

Splitting on Demand in SAT Modulo Theories.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2006

2005

Combining Nonstably Infinite Theories.

[BibT_eX]

[DOI]

Calogero G. Zarba

J. Autom. Reason., 2005

The Model Evolution Calculus with Equality.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2005

2004

Preface.

[BibT_eX]

[DOI]

Proceedings of the Selected Papers from the Workshops on Disproving, 2004

Abstract DPLL and Abstract DPLL Modulo Theories.

[BibT_eX]

[DOI]

Robert Nieuwenhuis

Albert Oliveras

Proceedings of the Logic for Programming, 2004

Combining Decision Procedures for Sorted Theories.

[BibT_eX]

[DOI]

Calogero G. Zarba

Proceedings of the Logics in Artificial Intelligence, 9th European Conference, 2004

DPLL( T): Fast Decision Procedures.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

2003

Preface.

[BibT_eX]

[DOI]

Teodor Rus

Theor. Comput. Sci., 2003

Unions of non-disjoint theories and combinations of satisfiability procedures.

[BibT_eX]

[DOI]

Christophe Ringeissen

Theor. Comput. Sci., 2003

Cooperation of Background Reasoners in Theory Reasoning by Residue Sharing.

[BibT_eX]

[DOI]

J. Autom. Reason., 2003

Combining Non-Stably Infinite Theories.

[BibT_eX]

[DOI]

Calogero G. Zarba

Proceedings of the 4th International Workshop on First-Order Theorem Proving, 2003

The Model Evolution Calculus.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Inf. Comput., 2002

Combining Decision Procedures for Positive Theories Sharing Constructors.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 13th International Conference, 2002

A DPLL-Based Calculus for Ground Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

Proceedings of the Logics in Artificial Intelligence, European Conference, 2002

2000

Combining Equational Theories Sharing Non-Collapse-Free Constructors.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 2000

1999

Combining Satisfiability Procedures for Automated Deduction and Constraint -Based Reasoning

[BibT_eX]

[DOI]

PhD thesis, 1999

Deciding the Word Problem in the Union of Equational Theories Sharing Constructors.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 10th International Conference, 1999

1998

Constraint Logic Programming over Unions of Constraint Theories.

[BibT_eX]

[DOI]

Mehdi T. Harandi

J. Funct. Log. Program., 1998

1997

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

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1997

1996

A New Correctness Proof of the {Nelson-Oppen} Combination Procedure.

[BibT_eX]