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, David Deharbe and Stephan Merz.

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


Conference Papers

  • Congruence closure with free variables
    Haniel Barbosa, Pascal Fontaine, and Andrew Reynolds. Accepted at 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017).
    Postprint (PDF)Report
  • Formal Verification of PLC programs using the B Method
    Haniel Barbosa, David Déharbe. ABZ, 2012.
  • An approach using the B method to formal verification of PLC programs in an Industrial Setting
    Haniel Barbosa, David Déharbe. SBMF, 2012.

Workshop Papers

Research Reports

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


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

+33 (0) 3 54 95 84 76