Παρακολούθηση
Haniel Barbosa
Haniel Barbosa
Άλλα ονόματαHaniel Moreira Barbosa
Universidade Federal de Minas Gerais
Η διεύθυνση ηλεκτρονικού ταχυδρομείου έχει επαληθευτεί στον τομέα dcc.ufmg.br - Αρχική σελίδα
Τίτλος
Παρατίθεται από
Παρατίθεται από
Έτος
cvc5: A Versatile and Industrial-Strength SMT Solver
H Barbosa, C Barrett, M Brain, G Kremer, H Lachnitt, M Mann, ...
TACAS 2022: 28th International Conference on Tools and Algorithms for the …, 2022
4762022
CVC4Sy: Smart and fast term enumeration for syntax-guided synthesis
A Reynolds, H Barbosa, A Nötzil, C Barrett, C Tinelli
CAV 2019: 31st International Conference on Computer Aided Verification (CAV), 2019
852019
Revisiting enumerative instantiation
A Reynolds, H Barbosa, P Fontaine
TACAS 2018: 24th International Conference on Tools and Algorithms for the …, 2018
762018
Extending SMT solvers to higher-order logic
H Barbosa, A Reynolds, D El Ouraoui, C Tinelli, C Barrett
CADE 2019: 27th International Conference on Automated Deduction (CADE), 2019
602019
Congruence closure with free variables
H Barbosa, P Fontaine, A Reynolds
TACAS 2017: 23rd International Conference on Tools and Algorithms for the …, 2017
492017
Scalable Fine-Grained Proofs for Formula Processing
H Barbosa, JC Blanchette, P Fontaine
CADE 2017: 26th International Conference on Automated Deduction (CADE), 398-412, 2017
462017
Scalable Fine-Grained Proofs for Formula Processing
H Barbosa, JC Blanchette, M Fleury, P Fontaine
Journal of Automated Reasoning 64, 485-510, 2020
452020
Syntax-Guided Rewrite Rule Enumeration for SMT Solvers
A Nötzli, A Reynolds, H Barbosa, A Niemetz, M Preiner, CW Barrett, ...
SAT 2019: 22nd International Conference on Theory and Applications of …, 2019
41*2019
Flexible Proof Production in an Industrial-Strength SMT Solver
H Barbosa, A Reynolds, G Kremer, H Lachnitt, A Niemetz, A Nötzli, ...
IJCAR 2022: 11th International Joint Conference on Automated Reasoning, 2022
262022
Formal verification of PLC programs using the B Method
H Barbosa, D Déharbe
ABZ 2012: 3rd Abstract State Machines, Alloy, B, VDM, and Z, 353-356, 2012
242012
Alethe: Towards a generic SMT proof format
HJ Schurr, M Fleury, H Barbosa, P Fontaine
arXiv preprint arXiv:2107.02354, 2021
212021
Extending enumerative function synthesis via SMT-driven classification
H Barbosa, A Reynolds, D Larraz, C Tinelli
FMCAD 2019: 19th Conference on Formal Methods in Computer-Aided Design (FMCAD), 2019
162019
Datatypes with shared selectors
A Reynolds, A Viswanathan, H Barbosa, C Tinelli, C Barrett
IJCAR 2018: 9th International Joint Conference on Automated Reasoning (IJCAR …, 2018
162018
Fair and Adventurous Enumeration of Quantifier Instantiations
M Janota, H Barbosa, P Fontaine, A Reynolds
FMCAD 2021: 21st Conference on Formal Methods in Computer-Aided Design, 2021
132021
CVC4 at the SMT competition 2018
C Barrett, H Barbosa, M Brain, D Ibeling, T King, P Meng, A Niemetz, ...
arXiv preprint arXiv:1806.08775, 2018
132018
Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis
A Reynolds, H Barbosa, D Larraz, C Tinelli
IJCAR 2020: 10th International Joint Conference on Automated Reasoning, 2020
102020
Better SMT proofs for easier reconstruction
H Barbosa, JC Blanchette, M Fleury, P Fontaine, HJ Schurr
AITP 2019-4th Conference on Artificial Intelligence and Theorem Proving, 2019
102019
Efficient instantiation techniques in SMT (work in progress)
H Barbosa
5th Workshop on Practical Aspects of Automated Reasoning (PAAR) 1635, 1-10, 2016
102016
Carcara: An efficient proof checker and elaborator for SMT proofs in the Alethe format
B Andreotti, H Lachnitt, H Barbosa
TACAS 2023: 29th International Conference on Tools and Algorithms for the …, 2023
92023
Language and proofs for higher-order SMT (work in progress)
H Barbosa, JC Blanchette, S Cruanes, DE Ouraoui, P Fontaine
arXiv preprint arXiv:1712.01486, 2017
82017
Δεν είναι δυνατή η εκτέλεση της ενέργειας από το σύστημα αυτή τη στιγμή. Προσπαθήστε ξανά αργότερα.
Άρθρα 1–20