Students and Alumni

David Deharbe's photo

Graduated PhD students 2

Haniel Moreira Barbosa (UFRN/Université de Lorraine). Quantifier instantiation techniques in SMT solvers. Co-supervised with Pascal Fontaine, Stephan Merz. Valério Gutemberg Medeiros Júnior (UFRN). Verified generation of assembly code for the B method. 2016 Bruno Emerson Gurgel Gomes. Formal Design of Smart Card Applications (Desenvolvimento Formal de Aplicações para Smart Card). 2012. Umberto Souza Costa. An explicit-symbolic model checker (Um verificador de modelos explícito-simbólico). 2005. Co-supervisor; main supervisor: Sérgio Campos (UFMG).

Graduated Research Master students 11

Diego de Azevedo Oliveira. Automated test generation for the verification of a LLVM code generator for the B-method. Vítor Alcântara de Almeida. Co-supervised by Richard Bonichon. A Frama-C plug-in for interactive proof. Paulo Ewerton Fragoso Gomes. Contributions to the SMT-based verification for Event-B (Contribuições para o Processo de Verificação de Satisfatibilidade Módulo Teoria em Event-B). 2015. Haniel Moreira Barbosa. Formal Verification of PLC Programs using the B Method. 2012 Valério Gutemberg de Medeiros Júnior. Extending the B Method to the Formal Design of Micro-Controlled Embedded Systems (Extensão do método B ao projeto formal de sistemas embarcados micro-controlados). 2008. Stephenson de Sousa Lima Galvão. Formal Modeling of the Real-Time Operating System FreeRTOS with the B Method (Modelagem Formal do Sistema Operacional de Tempo Real FreeRTOS Utilizando o Método B). 2008. Cláudia Fernando Oliveira Kiermes Tavares. Automated SMT proof for the B method (Prova automática de Satisfatibilidade Módulo Teoria Aplicada ao Método B). 2007. Diego Caminha Barbosa de Oliveira. Deciding Difference Logic in a Nelson-Oppen Combination Framework. 2007. Sérgio Queiroz de Medeiros. Application of Software Engineering Techniques to the SystemC Language (Aplicação de técnicas de engenharia de software para a linguagem SystemC). 2006. Ítalo Herbert Santos Gomes. Mecanismo de acessibilidade da Web para deficientes visuais. 2005. Co-supervisor; main supervisor: Guido Lemos. Antônio Augusto Oliveira Viana da Silva. Contributions for the Automatic Vericiation of JavaCard Applets (Contribuições para Verificação Automática de Applets JavaCard). 2004. Jorgiano Márcio Bruno Vidal. Initial BDD ordering for the automatic verification of finite state-transition systems (Ordenação inicial de BDDs para a verificação automática de sistemas de transição finita). 2002. Bartira Dantas Paraguaçu. The ZCLcsp Architecture Description Language (A linguagem de descrição de arquitetura ZCLcsp). 2000.