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. Accepted as system description at 26th International Conference on Automated Deduction (CADE-26).
    PreprintReport
  • Congruence closure with free variables
    Haniel Barbosa, Pascal Fontaine, and Andrew Reynolds. TACAS, 2017.
    PaperSlidesReport
  • 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

Research Reports

  • Formal verification of PLC programs using the B Method.
    Haniel Barbosa. Master's dissertation (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