LUCAS CARVALHO CORDEIRO
Av. Prof. Nilton Lins, 877 Málaga, Ap. 601
Manaus, Amazonas, Brazil. CEP: 69058-030
+55 · (92) · 98117 · 4512 [email protected]
CAREER SUMMARY
• Core competency in algorithms, software engineering, formal methods, program verification,
and embedded systems.
• 59 reviewed publications, including 8 journal papers and 51 workshop/conference contributions,
h-index 11, Best Paper Award at SBC SBESC’15 and ACM SAC’08, Distinguished Paper
Award at ACM ICSE’11, and two bronze medals in the overall ranking of the international
software verification competition at TACAS’12 and TACAS’13.
• Developer of XMPM, STB225, ESBMC, BMCLua, and DSVerifier tools.
• Active international research collaborations with University of Southampton, UK and University of Stellenbosh, South Africa.
• Proven track record of securing research funding from Samsung, Nokia Institute of Technology,
CNPq, FAPEAM, British Council, and Royal Society (career total in excess of BRL8,250,265 or
USD3,137,889).
• Research team leader (two PhD, six MSc, and eight BSc students), acted as course leader of
Electrical/Electronics Engineering from 2011 to 2015.
• Permanent member of the Graduate Program in Electrical Engineering and Collaborator of the
Graduate Program in Informatics at the Federal University of Amazonas.
• Strong software project management and development skills with full life-cycle exposure.
PROFESSIONAL EXPERIENCE
Federal University of Amazonas
Adjunct Professor
September 2009 - Present
Manaus, Brazil
· Continued work on ESBMC, which is an award-winning SMT-based context-bounded model checker
for C programs.
· Continued work on program verification, developed approaches to verify C/C++ programs via mathematical induction, discrete-time systems (digital filters and controllers), the Lua programming language.
· Developed and delivered undergraduate and graduate modules on algorithms, software verification,
real-time systems, digital systems, and embedded systems.
· Course Leader of Electrical Engineering since 2011, including the sub-areas of Electronics, Telecommunications, and Electrical Power Systems.
· Leader of a research team with one Ph.D. student, six M.Sc. students, and eight B.Sc. students.
· Secured competed research funding from Samsung, Nokia Institute of Technology, CNPq, FAPEAM,
British Council, and Royal Society.
Science & Technology Center for the Industrial Pole of Manaus
2008
Set-top Box Software Engineer
March 2007 - September
Manaus, Brazil
· Development of the Linux drivers for the ISDB-T (Brazilian market) tuner and DVB-T (European
market) tuner and demodulator silicon chips.
· Port of an ATSC-T (US market) tuner driver to a digital TV platform (Set-top Box).
1
· Development and integration of the DVB-S2 tuner used in satellite applications into the Linux user
space.
· Port of an IPTV middleware, development of software applications, and a Video on Demand portal for
the Set-top Boxes of NXP.
· Conception and implementation of automated unit and functional tests for the Linux device drivers by
using unit test framework tools and shell scripts (test automation).
· Coach customers to develop/customize software applications in digital TV platforms.
· Involved in several activities related to IP Set-top Box development at NXP semiconductors from San
Jose (USA) and Southampton (England).
BenQ Eletroeletrônica S.A
Software Engineer
October 2005 - March 2007
Manaus, Brazil
· Conception and implementation of a novel portable product for mobile phone data transfer on the point
of sales.
· Definition of target platforms and communication standards.
· Requirements definition, project planning, and tracking focused on features of the linuX Mobile Phone
Manager (XMPM). The features under coordination included GPRS, help system, connectivity, software
installation, phone settings, localization, and internationalization.
· Responsible for following-up progress and status of the features developed by different partners (deliverables, integration status, test status, defects, and change requests) and reporting status to the project
leader.
Siemens Eletroeletrônica S.A
Software Configuration and Build Manager
January 2005 - September 2005
Manaus, Brazil
· Configuration management planning, change management, version and release management, build management, and bug tracking process of the linuX Mobile Phone Manager (XMPM) project for generations
75 and 85 of Siemens Mobile Phones.
Institut fuer Automatisierungs- und Softwaretechnik
Trainee
September 2003 - March 2004
Stuttgart, Germany
· Microcontroller programming, development, and implementation of interface circuits for hardware
transducers.
· Integration of a real-time operating system (uCOS-II) and a bluetooth based communication into the
microcontroller M16C from Renesas.
· Design and modeling of electronic circuits with the Eagle tool.
EDUCATION
University of Southampton
May 2011
Ph.D. in Computer Science.
Thesis: SMT-Based Bounded Model Checking of Multi-threaded Software in Embedded Systems.
Supervisor: Prof. Dr. Bernd Fischer.
Scholarship holder of ORSAS/ECS.
Federal University of Amazonas
M.Sc. in Informatics.
Dissertation: An Agile HW/SW Development Methodology for Embedded Systems.
Supervisor: Prof. Dr. Raimundo S. Barreto.
Federal University of Amazonas
B.Sc. in Electrical Engineering.
Project: Developing Real-Time Applications with LEGO Mindstorms.
2
October 2007
December 2004
Scholarship holder of CAPES/DAAD from 03/2003 to 03/2004, in order to attend classes of the MSc
on Information Technology at the University of Suttgart (Germany).
Overall GPA: 8.313
PUBLICATIONS - JOURNAL ARTICLES
1. Gadelha, M. Y. R., Ismail, H. I., Cordeiro, L. C. “Handling Loops in Bounded Model Checking of
C Programs via k -Induction”. In International Journal on Software Tools for Technology Transfer,
Springer, 2015. DOI:10.1007/s10009-015-0407-9.
2. Trindade, A., Cordeiro, L. “Applying SMT-based Verification to Hardware/Software Partitioning
in Embedded Systems”. In Design Automation for Embedded Systems, Springer, 2015.
DOI:10.1007/s10617-015-9163-z.
3. Morse, J., Cordeiro, L., Nicole, D., Fischer, B. “Applying Symbolic Bounded Model Checking to
the 2012 RERS Greybox Challenge”. In Intl. Journal on Software Tools for Technology Transfer
(Print), v. 16, pp. 519-529, 2014.
4. Rosa, R., Lucena Jr., V., Cordeiro, L., Chaves Filho, J. “Dynamic and Automated Product
Derivation for Consumer Electronics Software Applications”. In IEEE Transactions on Consumer
Electronics, v. 59, pp. 883-891, 2013.
5. Morse, J., Cordeiro, L., Nicole, D., Fischer, B. “Model Checking LTL Properties over C Programs
with Bounded Traces”. In Journal of Software and Systems Modeling, Springer, v. 13, pp. 366,
2013.
6. Cordeiro, L., Fischer, B., and Marques-Silva, J. P. “SMT-Based Bounded Model Checking for
Embedded ANSI-C Software”. In IEEE Transactions on Software Engineering, v. 38, pp. 957974, 2012.
7. Freitas, M., Valenzuela, V., Gadelha, M., Silva Junior, W., Cordeiro, L., and Lucena Junior, V. “A
Distributed Extension of the Hybrid PRS System using Video Processing to Command a Robot
via Bluetooth”. In Intl. Journal of Computer Science and Network Security, v. 12, pp. 29-35,
2012.
8. Cordeiro, L., Mar, C., Valentin, E., Cruz, F., Patrick, D., Barreto, R., and Lucena Junior, V.
“An Agile Development Methodology Applied to Embedded Control Software under Stringent
Hardware Constraints”. In ACM SigSoft Software Engineering Notes, v. 33, pp. 24, 2008.
9. Cordeiro, L., Barreto, R., Barcelos, R., Oliveira, M., Lucena Junior, V., and Maciel, P. “TXM:
An Agile HW/SW Development Methodology for Building Medical Devices”. In ACM SigSoft
Software Engineering Notes, v. 32, pp. 28, 2007.
10. Cordeiro, L., Melo Junior, A., Paz Jr. D., Paz, E., Souza F., Alkmin J., Arago, A., and Campelo,
N. “Mapas de Isorresistividades Elétricas Aparentes do Solo Superficial da Cidade de Manaus”.
In Revista Brasileira de Geociências, 2004.
PUBLICATIONS - CONFERENCE CONTRIBUTIONS
1. Rocha, H. O., Cordeiro L. C., Barreto, R. S. Hunting Memory Bugs in C Programs with Map2Check
(Competition Contribution). To appear in the 22th Intl. Conf. on Tools and Algorithms for the
Construction and Analysis of Systems (TACAS), 2016.
2. Pereira, P. A., Albuquerque, H., Marques, H., Silva, I., Carvalho, C. B., Santos, V., Ferreira, R. S.,
Cordeiro, L. C. Verifying CUDA Programs using SMT-Based Context-Bounded Model Checking.
To appear in ACM Symposium on Applied Computing (SAC), Software Verification and Testing,
2016.
3
3. Ismail, H. I., Bessa, I. V., Cordeiro, L. C., Chaves Filho, J. E., Lima Filho, E. B. “DSVerifier: A
Bounded Model Checking Tool for Digital Systems”. In Proc. 22nd International SPIN Symposium
on Model Checking of Software (SPIN), LNCS 9232, pp. 126-131, 2015.
4. Rocha, H. O., Barreto, R. S., Cordeiro, L. C., “Memory Management Test-Case Generation of C
Programs using Bounded Model Checking”. In Proc. 13th International Conference on Software
Engineering and Formal Methods (SEFM), LNCS 9276, pp. 251-267, 2015.
5. Trindade, A. B., Ismail, H. I., Cordeiro, L. C. “Multi-Core Model Checking to Hardware-Software
Partitioning in Embedded Systems”. To appear in Proc. V Brazilian Symposium on Computing
Systems Engineering (SBESC), pp. 1-4, 2015.
6. Alves, E. H. S., Cordeiro, L. C., Lima Filho, E. B. “Fault Localization in Multi-Threaded C
Programs using Bounded Model Checking”. To appear in Proc. V Brazilian Symposium on
Computing Systems Engineering (SBESC), pp. 1-6, 2015.
7. Rocha, H., Ismail, H. I., Cordeiro, L. C., Barreto, R. S. “Model Checking Embedded C Software
using k -Induction and Invariants”. To appear in Proc. V Brazilian Symposium on Computing
Systems Engineering (SBESC), pp. 1-6, 2015. SBC Best Paper Award.
8. Sousa, F. R. M., Cordeiro, L. C., Lima Filho, E. B., “Bounded Model Checking of C++ Programs
Based on the Qt Framework”. In Proc. IEEE 4th Global Conference on Consumer Electronics
(GCCE), pp. 179–180, 2015.
9. Pereira, P. A., Albuquerque, H., Marques, H., Silva, I., Santos, V., Carvalho, C. B., Ferreira, R. S.,
Cordeiro, L. C. “Verificaçõ de Kernels em Programas CUDA usando Bounded Model Checking”.
To appear in Proc. XV Brazilian Symposium on High-Performance Computing (WSCAD-SSC),
pp. 1-12, 2015.
10. de Oliveira, R., Cordeiro, L., Lucena Jr., V. “Hardware Reconfiguration Based on Broadcast
Digital TV Signal”. In Proc. IEEE International Conference on Consumer Electronics (ICCE),
pp. 624-626, 2015.
11. Morse, J., Ramalho, M., Cordeiro, L., Nicole, D., Fischer, B. “ESBMC v1.22 (Competition Contribution)”. In Proc. 20th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (TACAS), LNCS 8413, pp. 405-407, 2014.
12. Bessa, I., Abreu, R., Cordeiro, L., Chaves Filho, J. “SMT-Based Bounded Model Checking of
Fixed-Point Digital Controllers”. In Proc. 40th Annual Conference of the IEEE Industrial Electronics Society (IECON), pp. 295-301, 2014.
13. Rosa, R., Cordeiro, L., Lucena Jr., V. “A Secondary Screen Architecture to Accurately Capture
Viewers’ Interactions in an iTV Environment”. In Proc. IEEE 3rd Global Conference on Consumer
Electronics (GCCE), pp. 264-265, 2014.
14. Januário, F., Cordeiro, L., Lima Filho, E., Lucena Jr., V. “BMCLua: Verification of Lua Programs
in Digital TV Interactive Applications”. In Proc. IEEE 3rd Global Conference on Consumer
Electronics (GCCE), pp. 707-708, 2014.
15. Trindade, A., Cordeiro, L. “Aplicando Verificação de Modelos para o Particionamento de Hardware/Software”. In 4th Brazilian Symposium on Computing Systems Engineering (SBESC), pp.
1-6, 2014.
16. Januário, F., Cordeiro, L., Lima Filho, E., Lucena Jr., V. “BMCLua: Verificação de Programas
Lua em Aplicações Interativas de TV Digital”. In 4th Brazilian Symposium on Computing Systems
Engineering (SBESC), pp. 1-6, 2014.
17. Bessa I., Ismail, H., Cordeiro, L., Chaves Filho, J. “Verification of Delta Form Realization in
Fixed-Point Digital Controllers Using Bounded Model Checking”. In 4th Brazilian Symposium on
4
Computing Systems Engineering (SBESC), pp. 49-54, 2014.
18. Ramalho, M., Cordeiro L., Cavalcante, A., Lucena Jr, V. “Verificação Baseada em Indução
Matemática de Programas C/C++”. In 3rd Brazilian Symposium on Computing Systems Engineering (SBESC), 2013.
19. Silva, V. Cordeiro L., Lucena Jr, V. “Verificação de Aplicações AmI Usando Java PathFinder”.
In 3rd Brazilian Symposium on Computing Systems Engineering (SBESC), 2013.
20. Abreu, R., Cordeiro, L., Lima Filho, E. “Verifying Fixed-Point Digital Filters using SMT-Based
Bounded Model Checking”. In 31st Brazilian Symposium on Telecommunications (SBrT), 2013.
DOI:10.14209/sbrt.2013.57
21. Januario, F., Cordeiro, L., Lima Filho, E. B. “Verificação de Códigos Lua Utilizando BMCLua”.
In 31st Brazilian Symposium on Telecommunications (SBrT), 2013. DOI:10.14209/sbrt.2013.92
22. Freitas, M., Ramalho, M., Cordeiro, L., Silva Jr., W., Lima Filho, E. “Verificação de Propriedades
de Filtros Digitais Implementados com Aritmética de Ponto Fixo”. In 31st Brazilian Symposium
on Telecommunications (SBrT), 2013. DOI:10.14209/sbrt.2013.226
23. Ramalho, M., Freitas, M., Sousa, F., Marques, H., Cordeiro, L., and Fischer, B. “SMT-Based
Bounded Model Checking of C++ Programs”. In Proc. 20th IEEE Intl. Conf. and Workshops
on Engineering of Computer-Based Systems (ECBS), pp. 147-156, 2013.
24. Morse, J., Cordeiro, L., Nicole, D., and Fischer, B. “Handling Unbounded Loops with ESBMC 1.20
(Competition Contribution)”. In Proc. 19th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 7795, pp. 621-624, 2013 (won the Bronze
Medal in the overall ranking).
25. Cohen, D., Barreto, R. , Oliveira, H., and Cordeiro, L. “A Car Racing Based Strategy for the Dynamic Voltage and Frequency Scaling Technique”. In Proc. 21st IEEE Intl. Symp. on Industrial
Electronics (ISIE), pp. 774-779, 2012.
26. Cordeiro, L., Morse, J., Nicole, D., and Fischer, B. “Context-Bounded Model Checking with
ESBMC 1.17 (Competition Contribution)”. In Proc. 18th Intl. Conf. on Tools and Algorithms
for the Construction and Analysis of Systems (TACAS), LNCS 7214, pp. 533-536, 2012 (won
the Bronze Medal in the overall ranking).
27. Lima, F., Cordeiro, L., and Souza, R. “Sistema de Monitoramento a Distância para Unidade de
Célula a Combustı́vel”. In 8th Brazilian Congress of Energy Planning (CBPE), 2012.
28. Rocha, H., Barreto, R., Cordeiro, L., and Dias-Neto, A. “Understanding Programming Bugs in
ANSI-C Software Using Bounded Model Checking Counter-Examples”. In Proc. 9th Intl. Conf.
on Integrated Formal Methods (iFM). LNCS 7321, pp. 128-142, 2012.
29. Caldas, R., Barreto, R., Cordeiro, L., and Campos, S. “A Formal Method for Modeling, Verification
and Synthesis of Embedded Reactive Systems”. In Proc. Intl. Conf. on Applied Computing (AC),
pp. 379-386, 2011.
30. Morse, J., Cordeiro, L., Nicole, D., and Fischer, B. “Context-Bounded Model Checking of LTL
Properties for ANSI-C Software”. In Proc. 9th Intl. Conf. on Software Engineering and Formal
Methods (SEFM), LNCS 7041, pp. 302-317, 2011.
31. Lucena Junior, V., Neto, J., Chaves Filho, J. E., Silva Junior, W., and Cordeiro, L. “Gift Young
Engineers: An Extra-Curricular Initiative for Updating Computer and Electrical Engineering
Courses”. In Proc. 41st ASEE/IEEE Frontiers in Education Conference (FIE), pp. 1-6, 2011.
32. Barreto, R., Cordeiro, L., and Fischer, B. “Verifying Embedded C Software with Timing Constraints using an Untimed Model Checker”. In Proc. Brazilian Symposium on Computing System
5
Engineering (SBESC), pp. 89-100, 2011.
33. Cordeiro, L. and Fischer, B. “Verifying Multi-threaded Software using SMT-based Context-Bounded
Model Checking”. In Proc. ACM/IEEE 33rd International Conference on Software Engineering
(ICSE), v. 1, pp. 331-340, 2011. ACM SIGSOFT Distinguished Paper Award.
34. Cordeiro, L., Fischer, B., and Marques-Silva, J. “Continuous Verification of Large Embedded
Software using SMT-Based Bounded Model Checking”. In Proc. 17th IEEE Intl. Conf. and
Workshops on Engineering of Computer-Based Systems, (ECBS), pp. 160-169, 2010.
35. Cordeiro, L. C. “SMT-Based Bounded Model Checking for Multi-threaded Software in Embedded
Systems”. In Proc. ACM/IEEE 32nd International Conference on Software Engineering (ICSE),
Doctoral Symposium, v.2., pp. 373-376, 2010.
36. Cordeiro, L., Fischer, B., Chen, H., and Marques-Silva, J. “Semiformal Verification of Embedded
Software in Medical Devices Considering Stringent Hardware Constraints”. In Proc. 6th IEEE
Intl. Conf. on Embedded Software and Systems (ICESS), pp. 396-403, 2009.
37. Cordeiro, L., Fischer, B., and Marques-Silva, J. “SMT-Based Bounded Model Checking for Embedded ANSI-C Software”. In Proc. 24th IEEE/ACM Intl. Conf. on Automated Software Engineering
(ASE), pp. 137-148, 2009.
38. Cordeiro, L., Mar, C., Valentin, E., Cruz, F., Patrick, D., Barreto, R. S., and Lucena Junior,
V. “A Platform-Based Software Design Methodology for Embedded Control Systems: An Agile
Toolkit”. In Proc. 15th IEEE Intl. Conf. and Workshops on the Engineering of Computer Based
Systems (ECBS), pp. 408-417, 2008.
39. Cruz, F., Barreto, R., Cordeiro, L., and Maciel, P. “ezRealtime: A Domain-Specific Modeling Tool
for Embedded Hard Real-Time Software Synthesis”. In Proc. Design, Automation and Test in
Europe (DATE), pp. 1510-1515, 2008.
40. Tefilo, M., Cordeiro, L., Barreto, R., and Pereira, J. “Mandos: A User Interaction Method in
Embedded Applications for Mobile Telephony”. In Proc. 1st IEEE International Conference on
Advances in Computer-Human Interaction (ACHI), pp. 271-276, 2008.
41. Cruz, F., Barreto, R., Cordeiro, L., and Maciel, P. “Towards a Model-Driven Engineering Approach
for Developing Embedded Hard Real-Time Software”. In Proc. 23rd ACM Symposium on Applied
Computing (SAC), pp. 308-314, 2008. ACM SIGAPP Best Paper Award.
42. Cordeiro, L., Barreto, R., and Oliveira, M. “Towards a Semiformal Development Methodology for
Embedded Systems”. In Proc. 3rd Intl. Conf. on Evaluation of Novel Approaches to Software
Engineering (ENASE), pp. 5-12, 2008.
43. Cordeiro, L., Barreto, R., Barcelos, R., Oliveira, M., Lucena Junior, V., and Maciel, P. “Agile
Development Methodology for Embedded Systems: A Platform-Based Desing Approach”. In Proc.
14th IEEE Intl. Conf. and Workshop on the Engineering of Computer Based Systems (ECBS),
pp.195-202, 2007.
44. Cordeiro, L., Becker, C., and Barreto, R. “Applying Scrum and Organizational Patterns to Multi
Site Software Development”. In Proc. 6th Latin American Conference on Pattern Languages of
Programming (SugarLoafPlop), pp. 46-67, 2007.
45. Cordeiro, L. and Louzado, D. “Aplicando Padrões de Gerência de Configuração de Software em
Projetos Geograficamente Distribuı́dos”. In Proc. 5th Latin American Conference on Pattern
Languages of Programming (SugarLoafPlop), pp. 207-221, 2005.
46. Alkmin J., de Melo Junior, A., da Paz, E., Campelo, N., Souza, F., Cordeiro, L., Carvalho, J., and
Aragão, A. “Comparação entre mapas de isorresistividades elétricas aparentes do solo superficial
6
de Manaus, a partir de séries de dados completos e estatı́sticos”. In 1st Regional Symposium of
Brazilian Geophysical Society, 2004.
47. Alkmin J., de Melo Junior, A., da Paz, E., Campelo, N., Souza, F., Cordeiro, L., Carvalho, J.,
and Aragão, A. “Malhas de Aterramento do Sistema Elétrico da Manaus Energia: um Estudo de
Caso”. In Second Conf. on Technological Innovation in Energy, 2003.
PUBLICATIONS - REVIEWED WORKSHOP CONTRIBUTIONS
1. Rodrigues, F. S., Cordeiro, L. C., Lima Filho, E. B. “Verificaçõ de Programas C++ Baseados no
Framework Multiplataforma Qt”. In IV Regional Meeting of Computer and Information Systems
(ENCOSIS), pp. 181–190, 2015.
2. Lima, M. S., Silva, E. S., Cordeiro, L. C. “Verificação de Modelos Aplicada aos Filtros Espaciais
em Processamento Digital de Imagens”. In IV Regional Meeting of Computer and Information
Systems (ENCOSIS), pp. 136–145, 2015.
3. Rocha, H., Cordeiro, L., Barreto, R., and Netto, J. “Exploiting Safety Properties in Bounded
Model Checking for Test Cases Generation of C Programs”. In Proc. 4th Brazilian Workshop on
Systematic and Automated Software Testing (SAST), pp.121-130, 2010.
4. Cordeiro, L. and Fischer, B. “Bounded Model Checking of Multi-threaded Software using SMT
solvers”. In 8th Intl. Workshop on Satisfiability Modulo Theories (SMT), 2010.
GRANTS
1. Verification of C/C++ Programs Based on Multi-Core Processors, Nokia Institute of Technology,
2014-2016, BRL451,231 (or USD171,594).
2. Hardware and Software Verification Based on Mathematical Induction for Embedded Systems,
Amazonas State Research Funding Agency, 2014-2016, BRL249,853 (or USD95,014).
3. SMT-based Bounded Model Checking of Multi-threaded Programs, British Council, 2014-2015,
GBP3,000 (or USD4,554).
4. Continuous Verification of C++ Programs Using SMT-based Bounded Model Checking, Nokia
Institute of Technology, 2011-13, BRL287,631 (or USD109,380).
5. SMT-Based Bounded Model Checking Timed LTL Properties for Embedded Software, Royal Society International Exchange Grant, 2011-13. GBP11,600 (or USD17,609) in collaboration with
Prof. Bernd Fischer from the University of Southampton.
6. Verification of Temporal Properties in Embedded Software using Satisfiability Modulo Theories, National Centre for Scientific and Technological Development, 2013-2016, BRL14,000 (or
USD5,324).
7. Research and training of human resources, at undergraduate and graduate courses, in the areas of
industrial automation, software development for mobile devices, and digital TV; Samsung / Institute of Development in Informatics, 2013-2016, BRL7,190,550 (or USD2,734,414) in collaboration
with Dr. Cı́cero Costa, Dr. Marly Costa, Dr. João Chaves Filho, Dr. Vicente Lucena Jr., Dr.
Andre Cavalcante, and Dr. Waldir Sabino Jr. from Federal University of Amazonas.
TEACHING
Undergraduate level
· Introduction to Algorithms, Federal University of Amazonas, 2007.
· C++ Programming, Federal University of Amazonas, 2008.
· Computer Networks, Federal University of Amazonas, 2009.
7
· Real-Time Programming, Federal University of Amazonas, from 2011 to 2014.
· Advanced Programming, Federal University of Amazonas, 2011, 2013.
· Computer Organization and Design, Federal University of Amazonas, from 2013 to 2014.
Graduate level
·
·
·
·
·
Embedded Systems and Linux for Digital TV, Baptist Superior College of Amazonas, 2008.
Design and Analysis of Algorithms, Federal University of Amazonas, 2011.
Real-Time Systems, Federal University of Amazonas, 2011, 2013.
Algorithms for Automation and Systems, Federal University of Amazonas, 2013.
Verification of Software and Systems, Federal University of Amazonas, 2014.
STUDENTS
Ph.D. Students (current)
· Francisco de Assis Pereira Januário (2015-2019). Verification of Lua Programs Based on k-Induction
(supervisor).
· Alessandro Bezerra Trindade (2015-2019). Applying SMT-based Verification to HW/SW Partitioning
for Embedded Systems with Many Cores (supervisor).
M.Sc. Students (current)
· Phillipe Arantes Pereira (2014-2016). Verification of GPU Kernels based on OpenCL programs.
· Mário Angel Praia Garcia (2014-2016). Verification of Automotive Applications Based on the OSEK/VDX
Operational Model.
· Hussama Ibrahim Ismail (2014-2016). Verification of GPU Kernels based on CUDA programs.
Ph.D. Students (graduated)
· Herbert de Oliveira Rocha (2012-2016). Verification of Software Systems Based on Code Transformation
using Bounded Model Checking (co-supervisor).
M.Sc. Students (graduated)
· Francisco de Assis Pereira Januário (2015). Verification of Lua Programs in Digital TV Interactive
Applications, lecturer at FUCAPI.
· Alessandro Bezerra Trindade (2015). Applying SMT-based Verification to Hardware/Software Partitioning in Embedded Systems, independent consultant.
· Renato Barbosa Abreu (2014). Verifying Fixed-Point Digital Filters using SMT-Based Bounded Model
Checking, first position at Nokia Institute of Technology.
· Mikhail Yasha Ramalho Gadelha (2013). Induction-Based Verification for C++ Programs, first position
at FUCAPI.
B.Sc. Students (graduated)
· Ícaro Nobrega de Sousa (2014). Desenvlvimento de um Sistema de Hardware e Software para Monitoramento Remoto e Controle Automático do Consumo Diário de Cargas Elétricas Residênciais, first
position at Samsung.
· Francisco Fagner do Rego Cunha (2014). Co-Projeto de Hardware/Software de uma Rede Reural Artifical Utilizando FPGA com o Processador NIOS II, first position at Electronic and Information Research
Center, Federal University of Amazonas.
· Jefferson Dionizio Soares de Souza (2013). Localização e Estimação de Tempo para Transporte Público
Urbano usando GPS e Internet, currently M.Sc. student.
8
· Marcelo Felipe Mazini dos Santos (2013). Desenvolvimento de um Terminal para Consulta de Preços,
first position at Yanconorte Comércio e Servio LTDA.
· George Corrêa de Araújo (2012). Desenvolvimento de um Plug-in do Eclipse para Ferramenta ESBMC
utilizando o Toolkit do ZEST, first position at Nokia Institute of Technology.
· Jhony Braga da Silva (2012). Sistema de Medição de Temperatura Integrado a TV Digital, first position
at Nokia Institute of Technology.
· Fábio de Souza Lima (2011). Uma Arquitetura de um Sistema Supervisório Aplicada a Célula Combustı́vel, first position at Samsung R&D.
PROFESSIONAL ACTIVITIES
Program committee member
· 38th Intl. Conference on Software Engineering, Austin, TX, USA, May 14 - 22, 2016.
· 22nd Intl. SPIN Symposium on Model Checking of Software, Stellenbosch, South Africa, August 24-26,
2015.
Jury committee member
· Intl. Competition on Software Verification of the Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, (2012-2014).
Co-organizer/session organizer
· 3rd ISSNIP Biosignals and Biorobotics Conference, Manaus, Brazil, January 9-11, 2012.
Reviewer for major journals and conferences
· IEEE Software, LNCS Transactions on Computational Science, Journal of Systems and Software, Formal Methods in System Design, and The Computer Journal.
· CAV 2014, ASE 2013, and ISMVL 2010.
PROFESSIONAL TRAINING
·
·
·
·
·
·
·
·
IPTV Middleware and Applications, Espial, England, 2007.
Digital TV Platform, NXP Semiconductors, USA, 2007.
Certified Scrum Master Training, Object Mentor, USA, 2006.
Agile Planning and Estimation, Object Mentor, USA, 2006.
C/C++ Programming for Windows, Embedded Systems Technologies, Brazil , 2006.
Software Configuration Management, Siemens Mobile, Germany, 2005.
Techniques and Tools for Development on Linux System, Conectiva, Curitiba, 2005.
Introduction to Capability Maturity Model Integration, Integrated System Diagnostics Brazil,
2005.
· Linux Administration, Conectiva, Brazil, 2004.
· Introduction to Embedded Linux, Conectiva, Brazil, 2004.
· Java 2 Micro Edition, Qualiti Software Processes, Brazil 2004.
AWARDS
Two gold and two bronze medals in the 4th Intl. Competition on Software Verification at the 21th Intl.
Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’15), European
Joint Conference on Theory and Practice of Software (ETAPS).
9
One gold medal in the 3rd Intl. Competition on Software Verification at the 20th Intl. Conf. on Tools
and Algorithms for the Construction and Analysis of Systems (TACAS’14), European Joint Conference
on Theory and Practice of Software (ETAPS).
Two silver and three bronze medals in the 2nd Intl. Competition on Software Verification at the 19th
Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’13),
European Joint Conference on Theory and Practice of Software (ETAPS).
Two gold and one bronze medals in the 1st Intl. Competition on Software Verification at the 18th Intl.
Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’12), European
Joint Conference on Theory and Practice of Software (ETAPS).
Distinguished paper award in the 33rd International Conference on Software Engineering (ICSE’11),
ACM Special Interest Group on Software Engineering (SIGSOFT).
Best paper award in the 23rd ACM Symposium on Applied Computing: Track on Real-Time Systems,
ACM Special Interest Group on Applied Computing (SIGAPP).
ORSAS Graduate Fellowship, Overseas Research Students Awards Scheme (ORSAS).
PERSONAL
Citizenship: Brazilian and Portuguese.
Languages: Portuguese (native), English (native standard), and German (high-school level).
REFERENCES
Prof. Dr. Bernd Fischer, University of Stellenbosh, Republic of South Africa.
[email protected]
Prof. Dr. João Marques-Silva, University College Dublin, Ireland.
[email protected]
Prof. Dr. Michael J Butler, University of Southampton, England.
[email protected]
10