Formal Verification of PLC Programs Using the B Method. - Haniel Barbosa; David Déharbe (ABZ, 2012)

An Approach Using the B Method to Formal Verification of PLC Programs in an Industrial Setting. - Haniel Barbosa; David Déharbe (SBMF, 2012)

Efficient Instantiation Techniques in SMT (Work In Progress). - Haniel Barbosa (PAAR@IJCAR, 2016)

Scalable Fine-Grained Proofs for Formula Processing. - Haniel Barbosa; Jasmin Christian Blanchette; Pascal Fontaine (CADE, 2017)

Congruence Closure with Free Variables. - Haniel Barbosa; Pascal Fontaine; Andrew Reynolds 001 (TACAS (2), 2017)

Language and Proofs for Higher-Order SMT (Work in Progress). - Haniel Barbosa; Jasmin Christian Blanchette; Simon Cruanes; Daniel El Ouraoui; Pascal Fontaine (PxTP, 2017)

New techniques for instantiation and proof production in SMT solving. (Nouvelles techniques pour l'instanciation et la production des preuves dans SMT). - Haniel Barbosa (2017)

Datatypes with Shared Selectors. - Andrew Reynolds 001; Arjun Viswanathan 001; Haniel Barbosa; Cesare Tinelli; Clark W. Barrett (IJCAR, 2018)

Revisiting Enumerative Instantiation. - Andrew Reynolds 001; Haniel Barbosa; Pascal Fontaine (TACAS (2), 2018)

CVC4 at the SMT Competition 2018. - Clark W. Barrett; Haniel Barbosa; Martin Brain; Duligur Ibeling; Tim King 001; Paul Meng; Aina Niemetz; Andres Nötzli; Mathias Preiner; Andrew Reynolds 001; Cesare Tinelli (CoRR, 2018)

Extending SMT Solvers to Higher-Order Logic. - Haniel Barbosa; Andrew Reynolds 001; Daniel El Ouraoui; Cesare Tinelli; Clark W. Barrett (CADE, 2019)

cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis. - Andrew Reynolds 001; Haniel Barbosa; Andres Nötzli; Clark W. Barrett; Cesare Tinelli (CAV (2), 2019)

Extending enumerative function synthesis via SMT-driven classification. - Haniel Barbosa; Andrew Reynolds 001; Daniel Larraz; Cesare Tinelli (FMCAD, 2019)

Syntax-Guided Rewrite Rule Enumeration for SMT Solvers. - Andres Nötzli; Andrew Reynolds 001; Haniel Barbosa; Aina Niemetz; Mathias Preiner; Clark W. Barrett; Cesare Tinelli (SAT, 2019)

CVC4SY for SyGuS-COMP 2019. - Andrew Reynolds 001; Haniel Barbosa; Andres Nötzli; Clark W. Barrett; Cesare Tinelli (CoRR, 2019)

Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis. - Andrew Reynolds 001; Haniel Barbosa; Daniel Larraz; Cesare Tinelli (IJCAR (1), 2020)

Lifting Congruence Closure with Free Variables to λ-free Higher-order Logic via SAT Encoding. - Sophie Tourret; Pascal Fontaine; Daniel El Ouraoui; Haniel Barbosa (SMT, 2020)

Scalable Fine-Grained Proofs for Formula Processing. - Haniel Barbosa; Jasmin Christian Blanchette; Mathias Fleury; Pascal Fontaine (J. Autom. Reason., 2020)

Fair and Adventurous Enumeration of Quantifier Instantiations. - Mikolás Janota; Haniel Barbosa; Pascal Fontaine; Andrew Reynolds 001 (FMCAD, 2021)

Alethe: Towards a Generic SMT Proof Format (extended abstract). - Hans-Jörg Schurr; Mathias Fleury; Haniel Barbosa; Pascal Fontaine (PxTP, 2021)

On-line synthesis of parsers for string events. - João Saffran; Haniel Barbosa; Fernando Magno Quintão Pereira; Srinivas Vladamani (J. Comput. Lang., 2021)

Flexible Proof Production in an Industrial-Strength SMT Solver. - Haniel Barbosa; Andrew Reynolds 001; Gereon Kremer; Hanna Lachnitt; Aina Niemetz; Andres Nötzli; Alex Ozdemir; Mathias Preiner; Arjun Viswanathan 001; Scott Viteri; Yoni Zohar; Cesare Tinelli; et al. (IJCAR, 2022)

Even Faster Conflicts and Lazier Reductions for String Solvers. - Andres Nötzli; Andrew Reynolds 001; Haniel Barbosa; Clark W. Barrett; Cesare Tinelli (CAV (2), 2022)

Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language. - Andres Nötzli; Haniel Barbosa; Aina Niemetz; Mathias Preiner; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (FMCAD, 2022)

cvc5: A Versatile and Industrial-Strength SMT Solver. - Haniel Barbosa; Clark W. Barrett; Martin Brain; Gereon Kremer; Hanna Lachnitt; Makai Mann; Abdalrhman Mohamed; Mudathir Mohamed; Aina Niemetz; Andres Nötzli; Alex Ozdemir; Mathias Preiner; et al. (TACAS (1), 2022)

An Interactive SMT Tactic in Coq using Abductive Reasoning. - Haniel Barbosa; Chantal Keller; Andrew Reynolds 001; Arjun Viswanathan 001; Cesare Tinelli; Clark W. Barrett (LPAR, 2023)

Challenges in SMT Proof Production and Checking for Arithmetic Reasoning (Invited Paper). - Haniel Barbosa (SC-Square@ISSAC, 2023)

Automatic Verification of SMT Rewrites in Isabelle/HOL. - Hanna Lachnitt; Mathias Fleury; Leni Aniva; Andrew Reynolds 001; Haniel Barbosa; Andres Nötzli; Clark W. Barrett; Cesare Tinelli (SMT, 2023)

Carcara: An Efficient Proof Checker and Elaborator for SMT Proofs in the Alethe Format. - Bruno Andreotti; Hanna Lachnitt; Haniel Barbosa (TACAS (1), 2023)

Synthesising Programs with Non-trivial Constants. - Alessandro Abate; Haniel Barbosa; Clark W. Barrett; Cristina David; Pascal Kesseli; Daniel Kroening; Elizabeth Polgreen; Andrew Reynolds 001; Cesare Tinelli (J. Autom. Reason., 2023)

IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. - Hanna Lachnitt; Mathias Fleury; Leni Aniva; Andrew Reynolds 001; Haniel Barbosa; Andres Nötzli; Clark W. Barrett; Cesare Tinelli (Zenodo, 2023)

Generating and Exploiting Automated Reasoning Proof Certificates. - Haniel Barbosa; Clark W. Barrett; Byron Cook; Bruno Dutertre; Gereon Kremer; Hanna Lachnitt; Aina Niemetz; Andres Nötzli; Alex Ozdemir; Mathias Preiner; Andrew Reynolds 001; Cesare Tinelli; et al. (Commun. ACM, 2023)

Satisfiability Modulo Theories: A Beginner's Tutorial. - Clark W. Barrett; Cesare Tinelli; Haniel Barbosa; Aina Niemetz; Mathias Preiner; Andrew Reynolds 001; Yoni Zohar (FM (2), 2024)

Towards Producing Shorter Congruence Closure Proofs in a State-of-the-art SMT Solver (Extended Abstract). - Bruno Andreotti; Haniel Barbosa; Oliver Flatt (PAAR+SC²@IJCAR, 2024)

IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. - Hanna Lachnitt; Mathias Fleury; Leni Aniva; Andrew Reynolds 001; Haniel Barbosa; Andres Nötzli; Clark W. Barrett; Cesare Tinelli (TACAS (1), 2024)

cvc5 for SMT-COMP 2024. - Leni Aniva; Haniel Barbosa; Clark W. Barrett; Hanna Lachnitt; Daniel Larraz; Abdalrhman Mohamed; Mudathir Mohamed; Aina Niemetz; Alex Ozdemir; Mathias Preiner; Andrew Reynolds 001; Hans-Jörg Schurr; et al. (Zenodo, 2024)

lean-smt: An SMT Tactic for Discharging Proof Goals in Lean. - Abdalrhman Mohamed; Tomaz Mascarenhas; Muhammad Harun Ali Khan; Haniel Barbosa; Andrew Reynolds 001; Yicheng Qian; Cesare Tinelli; Clark W. Barrett (CAV (3), 2025)

Lean-SMT: An SMT tactic for discharging proof goals in Lean. - Abdalrhman Mohamed; Tomaz Mascarenhas; Harun Khan; Haniel Barbosa; Andrew Reynolds 001; Yicheng Qian; Cesare Tinelli; Clark W. Barrett (CoRR, 2025)