Haniel Barbosa

Since December 2013 I am a PhD student at Inria Nancy (also associated with Université de Lorraine/FR and UFRN/BR) under the direction of Pascal Fontaine.

I work with instantiation and proof production in SMT solving and I am one of the developers of the veriT solver.

Drafts

• Scalable fine-grained proofs for formula processing
  H. B., Jasmin Christian Blanchette, and Pascal Fontaine. Submitted to the Journal of Automated Reasoning (JAR).
  Draft article

Conference Papers

• Scalable fine-grained proofs for formula processing
  H. B., Jasmin Christian Blanchette, and Pascal Fontaine. CADE-26, 2017.
  Postprint ⋅ Slides ⋅ Report
• Congruence closure with free variables
  H. B., Pascal Fontaine, and Andrew Reynolds. TACAS, 2017.
  Paper ⋅ Slides ⋅ Report
• An approach using the B method to formal verification of PLC programs in an industrial setting
  H. B. and David Déharbe. SBMF, 2012.
  Paper
• Formal verification of PLC programs using the B Method
  H. B. and David Déharbe. ABZ, 2012.
  Paper

Workshop Papers

• Language and proofs for higher-order SMT (work in progress)
  H. B., Jasmin Christian Blanchette, Simon Cruanes, Daniel El Ouraoui, and Pascal Fontaine. Accepted at 5th Workshop on Proof eXchange for Theorem Proving (PxTP 2017).
  Draft paper
• Efficient instantiation techniques in SMT (work in progress)
  H. B. PAAR@IJCAR, 2016.
  Paper ⋅ Bibtex
• Congruence closure with free variables (work in progress)
  H. B. and Pascal Fontaine. QUANTIFY@CADE, 2015.
  Paper ⋅ Bibtex

Theses

• New techniques for instantiation and proof production in SMT solving
  H. B. Ph.D. thesis. Inria, Université de Lorraine, UFRN. September 2017
  PDF ⋅ PDF + extended abstracts in FR and PT-BR ⋅ Slides
• Formal verification of PLC programs using the B Method
  H. B. M.Sc. thesis. UFRN. October 2012
  PDF

Contact

Loria, VeriDis Team, Room B225
615, rue du Jardin Botanique
F-54602, Villers-lès-Nancy, France

+33 (0) 3 54 95 84 76
haniel.barbosa@inria.fr