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
  Haniel Barbosa, Jasmin Christian Blanchette, and Pascal Fontaine.
  Draft article

Conference Papers

• Scalable fine-grained proofs for formula processing
  Haniel Barbosa, Jasmin Christian Blanchette, and Pascal Fontaine. CADE-26, 2017.
  Preprint ⋅ Report
• Congruence closure with free variables
  Haniel Barbosa, 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
  Haniel Barbosa, David Déharbe. SBMF, 2012.
  Paper
• Formal verification of PLC programs using the B Method
  Haniel Barbosa, David Déharbe. ABZ, 2012.
  Paper

Workshop Papers

• Language and proofs for higher-order SMT (work in progress)
  Haniel Barbosa, 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)
  Haniel Barbosa. PAAR@IJCAR, 2016.
  Paper ⋅ Bibtex
• Congruence closure with free variables (work in progress)
  Haniel Barbosa, Pascal Fontaine. QUANTIFY@CADE, 2015.
  Paper ⋅ Bibtex

Research Reports

• Formal verification of PLC programs using the B Method.
  Haniel Barbosa. Master's dissertation (PDF)