Hello, I am Herbert Oliveira Rocha.

Currently, I am a professor in the Departament of Computer Science at Federal University of Roraima. My research focuses on the development of automated verification and software testing techniques for software systems. In particular, I am interested in the verification and testing of the critical embedded systems.

PERSONAL DATA

• Researcher from/at:
  • Department of Computer Science of the Federal University of Roraima (2015 to present)
  • National Science and Technology Institute for Critical Embedded Systems INCT-SEC (2011 to 2012)
  • Federal University of Amazonas (2009 to 2015)
• Phone: +55 95 98400 5346
• Email: herbert.rocha@ufrr.br

ACHIEVEMENTS

CTFL	Docker	Starstruck	Arctic Code Vault Contributor	Pull Shark	Huawei Certified ICT Associate-AI v3.0

EDUCATION

• 2011 - 2015: Ph.D. in Computer Science. Federal University of Amazonas, UFAM, Brazil - Thesis: Verification of Software Systems based on Code Transformations using Bounded Model Checking. Advisor: Prof. PhD. Raimundo da Silva Barreto and Co-Advisor: Prof. PhD. Lucas Carvalho Cordeiro;
• 2009 - 2011: Master in Computer Science. Federal University of Amazonas, UFAM, Brazil. Thesis: Verification and Validation of Error in C Codes using Bounded Model Checker. Advisor: Prof. PhD. Raimundo da Silva Barreto
• 2006 - 2008: Undergraduate Degree in Technology of Analysis and Development Systems. Federal Institute of Education, Science and Technology of Roraima, IFRR, Brazil. Thesis: Development of Embedded Software for Control Orders of Restaurant using J2ME. Advisor: Prof. MSc. Pierre Viana Junior

CERTIFICATIONS AND AWARDS

• Certified Tester Foundation Level – CTFL
  International Software Testing Qualifications Board – ISTQB
  CTFL ID: 12-CTFL-01897-BR. 2012.
• 1st place in The Programming Marathon
  Federal Institute of Education, Science and Technology of Roraima, Undergraduate Degree in Technology of Analysis and Development Systemsma, IFRR, Brazil. 2007.

RESEARCH GROUP

Research Group of Project and Development for Optimized and Safe Embedded Systems - PRISM from the Department of Computer Science of the Federal University of Roraima.

LITERATURE PRODUCTION

1. ALHAWI, OMAR M. ; ROCHA, HERBERT ; GADELHA, MIKHAIL R. ; CORDEIRO, LUCAS C. ; BATISTA, EDDIE. Verification and refutation of C programs based on k-induction and invariant inference. INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER (INTERNET), v. 22, p. 1-21, 2020.

2. ROCHA, H. O.; MENEZES, R. S. ; CORDEIRO, LUCAS ; BARRETO, RAIMUNDO. Map2Check: Using Symbolic Execution and Fuzzing (Competition Contribution). In: 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2020, Dublin. 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2020. v. 12078. p. 403-407.

3. MENEZES, R. ; ROCHA, H. ; CORDEIRO, L. C. ; BARRETO, R. S. . Map2Check using LLVM and KLEE. In: 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2018, Thessaloniki. TACAS’18, 2018. v. 10806.

4. ROCHA, W. ; ROCHA, H. ; ISMAIL, HUSSAMA ; CORDEIRO, LUCAS ; FISCHER, B. . DepthK: A k-Induction Verifier Based on Invariant Inference for C Programs. In: 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2017, Uppsala. 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2017.

5. ROCHA, H. O.; ISMAIL, HUSSAMA ; CORDEIRO, LUCAS ; Barreto . Model Checking Embedded C Software Using k-Induction and Invariants. In: Djones Lettnin, Markus Winterholer. (Org.). Embedded Software Verification and Debugging. 1ed.New York: Springer-Verlag, 2017, v. , p. 159-182.

6. ROCHA, H.; Cordeiro ; Barreto . Hunting Memory Bugs in C Programs with Map2Check (Competition Contribution). In: 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2016, Eindhoven. European Joint Conferences on Theory and Practice of Software, ETAPS, 2016. v. 9636. p. 934-937.

7. BENTES, L. G. P ; ROCHA, H. ; BEZERRA, E. V. ; BARRETO, RAIMUNDO . JFORTES: Java FORmal unit TESt generation. In: VI Brazilian Symposium on Computing Systems Engineering, 2016, João Pessoa - Paraíba. VI Brazilian Symposium on Computing Systems Engineering. Porto Alegre - RS: SBC, 2016.

8. ROCHA, HERBERT; BARRETO, RAIMUNDO ; CORDEIRO, LUCAS . Memory Management Test-Case Generation of C Programs using Bounded Model Checking. In: 13th International Conference on Software Engineering and Formal Methods, 2015, York. Software Engineering and Formal Methods, 2015. v. 9276. p. 251-267.

9. ROCHA, HERBERT; ISMAIL, HUSSAMA ; CORDEIRO, LUCAS ; BARRETO, RAIMUNDO . Model Checking Embedded C Software Using k-Induction and Invariants. In: 2015 Brazilian Symposium on Computing Systems Engineering (SBESC), 2015, Foz do Iguacu. 2015 Brazilian Symposium on Computing Systems Engineering (SBESC), 2015. p. 90.

10. ROCHA, H. O.; Barreto . Corretude e Segurança de Sistemas Embarcados Críticos Usando Bounded Model Checkers. In: II Brazilian Conference on Critical Embedded Systems, 2012, Campinas. II Brazilian Conference on Critical Embedded Systems, 2012.

11. ROCHA, H. O.; Barreto ; Cordeiro ; DIAS NETO, A. C. . Understanding Programming Bugs in ANSI-C Software Using Bounded Model Checking Counter-Examples. In: 9th International Conference on Integrated Formal Methods, 2012, Pisa. Integrated Formal Methods, 2012. v. 7321/2. p. 128-142.

12. CUNHA, E. ; CUSTODIO, M. ; ROCHA, H. ; BARRETO, R. . Formal Verification of UML Sequence Diagrams in the Embedded Systems Context. In: 2011 Brazilian Symposium on Computing System Engineering (SBESC), 2011, Florianopolis. 2011 Brazilian Symposium on Computing System Engineering, 2011. p. 39-45.

13. ROCHA, H. O.; Cordeiro ; Barreto ; Netto . Exploiting Safety Properties in Bounded Model Checking for Test Cases Generation of C Programs. In: 4th Brazilian Workshop on Systematic and Automated Software Testing (SAST), 2010, Natal. Proceedings of IV Brazilian Workshop on Systematic and Automated Software Testing, 2010. p. 121-130.

14. ROCHA, H. O.; Jefferson Thomas de Oliveira ; Marcelo de Farias Matos ; Pierre da Costa Viana Júnior . Desenvolvimento de Software Embarcado para Controle de Pedidos de Pizzaria com J2ME. Norte Científico, v. 3, p. 8-22, 2008.

INTERESTS IN COMPUTING

• Verification and Validation of Software/Hardware
• Automated Reasoning
• Testing Software
• Embedded Systems
• Computer Vision
• Operating Systems
• Programming Languages
• Regular Expressions
• Web Systems
• Mobile Apps, and
• Design and Art