Haniel Barbosa

47 papers A 5B 7C 1Journal 10Unranked 19

Year	Rank	Type	Title / Venue / Authors
2026	B	`conf`	Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions. CPP Tomaz Mascarenhas, Harun Khan, Abdalrhman Mohamed, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli
2026	—	`conf`	Hint-Based SMT Proof Reconstruction. TACAS (1) Joshua Clune, Haniel Barbosa, Jeremy Avigad
2026	J	`jnl`	Hint-Based SMT Proof Reconstruction. CoRR Joshua Clune, Haniel Barbosa, Jeremy Avigad
2026	B	`conf`	Producing Shorter Congruence Closure Proofs in a State-of-the-Art SMT Solver. VMCAI Bruno Andreotti, Haniel Barbosa
2026	J	`jnl`	Reconstruction of SMT proofs with Lambdapi. Acta Informatica Alessio Coltellacci, Bruno Andreotti, Haniel Barbosa, Gilles Dowek, Stephan Merz
2025	B	`conf`	Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL. ITP Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds, Hans-Jörg Schurr, Clark W. Barrett, Cesare Tinelli
2025	J	`jnl`	Lean-SMT: An SMT tactic for discharging proof goals in Lean. CoRR Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett
2025	—	`ed.`	Proceedings Twentieth International Symposium on Logical and Semantic Frameworks with Applications, LSFA 2025, Brasilia, Brazil, October 7-8, 2025. LSFA Haniel Barbosa, Christophe Ringeissen
2025	—	`conf`	lean-smt: An SMT Tactic for Discharging Proof Goals in Lean. CAV (3) Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett
2024	—	`ed.`	Formal Methods: Foundations and Applications - 26th Brazilian Symposium, SBMF 2023, Manaus, Brazil, December 4-8, 2023, Proceedings SBMF Haniel Barbosa, Yoni Zohar
2024	—	`conf`	IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. TACAS (1) Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2024	—	`conf`	Satisfiability Modulo Theories: A Beginner's Tutorial. FM (2) Clark W. Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar
2024	—	`conf`	Towards Producing Shorter Congruence Closure Proofs in a State-of-the-art SMT Solver (Extended Abstract). PAAR+SC²@IJCAR Bruno Andreotti, Haniel Barbosa, Oliver Flatt
2023	B	`conf`	An Interactive SMT Tactic in Coq using Abductive Reasoning. LPAR Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli, Clark W. Barrett
2023	—	`conf`	Automatic Verification of SMT Rewrites in Isabelle/HOL. SMT Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2023	—	`conf`	Carcara: An Efficient Proof Checker and Elaborator for SMT Proofs in the Alethe Format. TACAS (1) Bruno Andreotti, Hanna Lachnitt, Haniel Barbosa
2023	—	`conf`	Challenges in SMT Proof Production and Checking for Arithmetic Reasoning (Invited Paper). SC-Square@ISSAC Haniel Barbosa
2023	J	`jnl`	Generating and Exploiting Automated Reasoning Proof Certificates. Commun. ACM Haniel Barbosa, Clark W. Barrett, Byron Cook, Bruno Dutertre, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Cesare Tinelli, Yoni Zohar
2023	—	`ed.`	Proceedings of the 7th SC-Square Workshop co-located with the Federated Logic Conference, SC-Square@FLoC 2022, as a part of the 11th International Joint Conference on Automated Reasoning, IJCAR 2022, Haifa, Israel, August 12, 2022. SC-Square@FLoC Ali Kemal Uncu, Haniel Barbosa
2023	J	`jnl`	Synthesising Programs with Non-trivial Constants. J. Autom. Reason. Alessandro Abate, Haniel Barbosa, Clark W. Barrett, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, Andrew Reynolds, Cesare Tinelli
2022	—	`conf`	Even Faster Conflicts and Lazier Reductions for String Solvers. CAV (2) Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli
2022	A	`conf`	Flexible Proof Production in an Industrial-Strength SMT Solver. IJCAR Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, Clark W. Barrett
2022	B	`conf`	Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language. FMCAD Andres Nötzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2022	—	`conf`	cvc5: A Versatile and Industrial-Strength SMT Solver. TACAS (1) 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, Andrew Reynolds, Ying Sheng, Cesare Tinelli, Yoni Zohar
2021	—	`conf`	Alethe: Towards a Generic SMT Proof Format (extended abstract). PxTP Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa, Pascal Fontaine
2021	B	`conf`	Fair and Adventurous Enumeration of Quantifier Instantiations. FMCAD Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
2021	J	`jnl`	Fair and Adventurous Enumeration of Quantifier Instantiations. CoRR Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
2021	J	`jnl`	On-line synthesis of parsers for string events. J. Comput. Lang. João Saffran, Haniel Barbosa, Fernando Magno Quintão Pereira, Srinivas Vladamani
2020	—	`conf`	Lifting Congruence Closure with Free Variables to λ-free Higher-order Logic via SAT Encoding. SMT Sophie Tourret, Pascal Fontaine, Daniel El Ouraoui, Haniel Barbosa
2020	—	`conf`	Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis. IJCAR (1) Andrew Reynolds, Haniel Barbosa, Daniel Larraz, Cesare Tinelli
2020	J	`jnl`	Scalable Fine-Grained Proofs for Formula Processing. J. Autom. Reason. Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine
2019	J	`jnl`	CVC4SY for SyGuS-COMP 2019. CoRR Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2019	A	`conf`	Extending SMT Solvers to Higher-Order Logic. CADE Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, Clark W. Barrett
2019	B	`conf`	Extending enumerative function synthesis via SMT-driven classification. FMCAD Haniel Barbosa, Andrew Reynolds, Daniel Larraz, Cesare Tinelli
2019	—	`ed.`	Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019, Natal, Brazil, August 26, 2019. PxTP Giselle Reis, Haniel Barbosa
2019	A	`conf`	Syntax-Guided Rewrite Rule Enumeration for SMT Solvers. SAT Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark W. Barrett, Cesare Tinelli
2019	—	`conf`	cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis. CAV (2) Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2018	J	`jnl`	CVC4 at the SMT Competition 2018. CoRR Clark W. Barrett, Haniel Barbosa, Martin Brain, Duligur Ibeling, Tim King, Paul Meng, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Cesare Tinelli
2018	A	`conf`	Datatypes with Shared Selectors. IJCAR Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, Clark W. Barrett
2018	—	`conf`	Revisiting Enumerative Instantiation. TACAS (2) Andrew Reynolds, Haniel Barbosa, Pascal Fontaine
2017	—	`conf`	Congruence Closure with Free Variables. TACAS (2) Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
2017	—	`conf`	Language and Proofs for Higher-Order SMT (Work in Progress). PxTP Haniel Barbosa, Jasmin Christian Blanchette, Simon Cruanes, Daniel El Ouraoui, Pascal Fontaine
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	A	`conf`	Scalable Fine-Grained Proofs for Formula Processing. CADE Haniel Barbosa, Jasmin Christian Blanchette, Pascal Fontaine
2016	—	`conf`	Efficient Instantiation Techniques in SMT (Work In Progress). PAAR@IJCAR Haniel Barbosa
2012	—	`conf`	An Approach Using the B Method to Formal Verification of PLC Programs in an Industrial Setting. SBMF Haniel Barbosa, David Déharbe
2012	C	`conf`	Formal Verification of PLC Programs Using the B Method. ABZ Haniel Barbosa, David Déharbe