Leonardo José Simões de Freitas

possui doutorado em Ciência da Computação pela University of York na Inglaterra (2005), e mestrado em Ciências da Computação pela Universidade Federal de Pernambuco (UFPE) em 2002. Tem experiência de Engenharia de Software com enfase em métodos formais, atuando principalmente nos seguintes temas: Z, model checking, csp, theorem proving, concurrency, e process algebra. Trabalhou como senior researcher na Universidade de York (2006-2010) com Prof. Jim Woodcock, e em Newcastle (2010-2012) com Prof. Cliff Jones. Atualmente trabalha como Lecturer in Formal Methods and Tools em Newcastle University (2012-)

Informações coletadas do Lattes em 15/11/2022

Acadêmico

Formação acadêmica

Doutorado em PhD Computer Science

2002 - 2005

University of York
Título: Model Checking Circus
Orientador: Jim Woodcock
Palavras-chave: Model checking; Refinement; Circus - CSP + Z; Unifying Theories of Programming - UTP; Automata theory; Critical and Safety Systems. Grande área: Ciências Exatas e da TerraGrande Área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Matemática da Computação / Especialidade: Matemática Simbólica. Grande Área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Metodologia e Técnicas da Computação / Especialidade: Engenharia de Software. Setores de atividade: Desenvolvimento de Programas (Software); Consultoria em Sistemas de Informática; Outro.

Mestrado em Ciências da Computação

2000 - 2002

Universidade Federal de Pernambuco
Título: Implementação de Sistemas Concorrentes e Distribuídos em Java,Ano de Obtenção: 2002
Augusto César Alves Sampaio.Bolsista do(a): Conselho Nacional de Desenvolvimento Científico e Tecnológico, CNPq, Brasil. Palavras-chave: CSP - Concurrent Sequential Processes; CSP-Z - Integração de Formalismos; Modelagem Orientada à Objetos; Concorrência Formal; Programação Concorrente em Java; Role Model Based Design. Grande área: Ciências Exatas e da TerraGrande Área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação / Especialidade: Linguagem Formais e Autômatos. Grande Área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Metodologia e Técnicas da Computação / Especialidade: Linguagens de Programação. Setores de atividade: Informática.

Graduação em Ciência da Computação

1996 - 2000

Universidade Salvador

Pós-doutorado

2006

Pós-Doutorado. , University of York, YORK, Inglaterra. , Grande área: Ciências Exatas e da Terra, Grande Área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Metodologia e Técnicas da Computação / Especialidade: Linguagens de Programação. , Grande Área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação / Especialidade: Lógicas e Semântica de Programas.

Formação complementar

2002 - 2002

Summer School Specification Verification Refinemen. (Carga horária: 80h). , Abo Akademi University, ABO, Finlândia.

Idiomas

Inglês

Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.

Chinês

Compreende Pouco, Fala Pouco, Lê Pouco.

Espanhol

Compreende Bem, Fala Pouco, Lê Razoavelmente.

Português

Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.

Francês

Compreende RazoavelmenteLê Pouco.

Japonês

Compreende Pouco, Fala Pouco.

Áreas de atuação

Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Metodologia e Técnicas da Computação/Especialidade: Engenharia de Software.

Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Metodologia e Técnicas da Computação/Especialidade: Linguagens de Programação.

Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação/Especialidade: Linguagem Formais e Autômatos.

Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação/Especialidade: Lógicas e Semântica de Programas.

Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Matemática da Computação/Especialidade: Matemática Simbólica.

Participação em eventos

Internal Formal Methods Symposium.Colaborador da Organização. 2004. (Simpósio).

Participação em bancas

FREITAS, Leo. Julgamento de artigos para conferência. 2004. University of Kent.

Orientou

Fu Zheng

Masters in Software Enginieering; 2006; Dissertação (Mestrado em MSc in Software Engineering) - University of York,; Orientador: Leonardo José Simões de Freitas;

Produções bibliográficas

FREITAS, LEO ; WATSON, PAUL . Formalizing workflows partitioning over federated clouds: multi-level security and costs. International Journal of Computer Mathematics , v. 91, p. 881-906, 2013.
2011 FREITAS, LEO ; MCDERMOTT, JOHN . Formal methods for security in the Xenon hypervisor. International Journal on Software Tools for Technology Transfer (Print) , v. 13, p. 463-489, 2011.
2009 FREITAS, LEO ; WOODCOCK, JIM . FDR Explorer. Formal Aspects of Computing , v. 21, p. 133-154, 2009.
2009 FREITAS, LEO ; WOODCOCK, JIM ; ZHANG, YICHI . Verifying the CICS File Control API with Z/Eves: An experiment in the verified software repository. Science of Computer Programming (Print) , v. 74, p. 197-218, 2009.
2009 BUTTERFIELD, ANDREW ; FREITAS, LEO ; WOODCOCK, JIM . Mechanising a formal model of flash memory. Science of Computer Programming (Print) , v. 74, p. 219-237, 2009.
2008 FREITAS, LEO ; WOODCOCK, JIM . Mechanising Mondex with Z/Eves. Formal Aspects of Computing , v. 20, p. 117-139, 2008.
2007 FREITAS, LEO ; WOODCOCK, JIM . FDR Explorer. Electronic Notes in Theoretical Computer Science , v. 187, p. 19-34, 2007.
2002 FREITAS, Leo ; SAMPAIO, Augusto ; CAVALCANTI, Ana Lúcia . JACK - A Framework for Implementing CSP in Java. Sbes, 2002.
2001 FREITAS, Leo ; CAVALCANTE, A. L. C. ; MOURA, H. . Animating CSPm Using Action Semantics. Sbes 2001 Workshops, Rio de Janeiro - RJ, 2001.
Freitas, Leo ; Whiteside, Iain . Proof Patterns for Formal Methods. Lecture Notes in Computer Science. 1ed.: Springer International Publishing, 2014, v. , p. 279-295.
Freitas, Leo ; Jones, Cliff B. ; Velykis, Andrius ; Whiteside, Iain . A Model for Capturing and Replaying Proof Strategies. Lecture Notes in Computer Science. 1ed.: Springer International Publishing, 2014, v. , p. 183-199.
Jones, Cliff B. ; Freitas, Leo ; Velykis, Andrius . Ours Is to Reason Why. Lecture Notes in Computer Science. 1ed.: Springer Berlin Heidelberg, 2013, v. , p. 227-243.
Velykis, Andrius ; Freitas, Leo . Formal Modelling of Separation Kernel Components. Lecture Notes in Computer Science. 1ed.: Springer Berlin Heidelberg, 2010, v. , p. 230-244.
EMMS, MARTIN ; ARIEF, BUDI ; FREITAS, LEO ; HANNON, JOSEPH ; VAN MOORSEL, AAD . Harvesting High Value Foreign Currency Transactions from EMV Contactless Credit Cards Without the PIN. In: the 2014 ACM SIGSAC Conference, 2014, Scottsdale. Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security - CCS '14. New York: ACM Press, 2014. p. 716.
FREITAS, Leo ; CAVALCANTI, Ana Lúcia ; MOURA, H. . Animating CSPm Using Action Semantics. In: WorkShop de Métodos Formais, 2001, Rio de Janeiro, 2001.
Jim Woodcock ; CAVALCANTI, Ana Lúcia ; Godel, Ml.C. ; FREITAS, Leo . Circus Operational Semantics. Formal Aspects of Computing , 2008.
FREITAS, Leo ; Jim Woodcock . Z/Eves and the Mondex Electronics Purse. Formal Aspects of Computing , 2008.
FREITAS, Leo ; Jim Woodcock . FDR Explorer. Formal Aspects of Computing , 2008.
FREITAS, Leo ; Jim Woodcock . Verifying the CICS file control API in Z/Eves. Science of Computer Programming , 2008.
FREITAS, Leo ; Jim Woodcock . POSIX file store in Z/Eves: an experiement in the verified software repository. Science of Computer Programming , 2008.
Andrew Butterfield ; FREITAS, Leo ; Jim Woodcock . Formalising Flash Memory. Science of Computer Programming , 2008.
FREITAS, Leo ; CAVALCANTI, Ana Lúcia ; Jim Woodcock . State Rich Model Checking. Innovations in Systems and Software Engineering , 2007.

Outras produções

FREITAS, Leo ; JACK: Uma implementação de Algebra de Processos em Java. 2001.

FREITAS, Leo ; LESSA, D. . Bibliotecas de Componentes. 1999.

FREITAS, Leo ; MARIZ, M. ; SARAIVA, E. . DDDX. 1998.

FREITAS, Leo ; NOGUEIROL, D. . Automação Comercial para Escolas do 2 grau. 1997.

FREITAS, Leo ; Model Checking Strategy for Circus. 2003.

FREITAS, Leo ; DURAN, A. A. . Modelagem do satélite SACI-1 em CSP-Z. 2000.

FREITAS, Leo ; JÚNIROR, O. C. P. . Agentes Inteligentes para Negociação via Web. 2000.

FREITAS, Leo ; Animating CSPm with Action Semantics. 2000.

Prêmios

2007

Gratis researcher - 1 week visit, Microsoft Research, Redmond.

2007

SRI research collaboration bursary - 2 weeks, Stanford Research Institute (SRI).

2007

NASA - JPL collaboration, Jet Propulsion Laboratory (JPL) - Caltech US.

2006

Cambridge Proficiency in English (CPE), Cambridge University.

2002

Bussiness English Course - Level 3, Cambridge.

2000

Curso de Desenvolvimento Baseado em Componentes, Sociedade Brasileira de Computação - SBES.

2000

Curso de Arquitetura em Sistemas de Tempo Real, Sociedade Brasileira de Computação - SBES.

2000

Curso de Introdução a Métodos Formais para Sist. Concorrentes, Sociedade Brasileira de Computação - WMF.

2000

Curso de Java Avançado, Centro de Estudos Avançados do Recife - CESAR.

2000

Curso de RUP e UML, Centro de Estudos Avançados do Recife - CESAR.

2000

TOEFL - 250 Computer Based, TOEFL.

1998

Design Patterns e Frameworks, UFBA - VII Semana de Informática.

1998

Desenvolvedor Delphi 3 Client/Server, Borland (Inpise).

1997

Delphi 2 Avançado C/S, MaS Borland Traning Center - SP.

1996

Curso de Modelagem de dados e Engenharia de Software, UFBA - VI Semana de Informática.

Histórico profissional

Endereço profissional

University of York, Deparment Of Computer Science, Computing Laboratory. , Heslington, YO15DD - York, - Inglaterra, Telefone: (44190) 4434753, Fax: (44190) 4432807, URL da Homepage:

Experiência profissional

2002 - 2004

University of Kent

Vínculo: Colaborador, Enquadramento Funcional: Outro, Carga horária: 3

Outras informações:
Ensino para alunos de Graduação do curso de Ciência da Computação e Computação com Administração

2002 - 2004

University of Kent

Vínculo: PhD Research Student, Enquadramento Funcional: , Carga horária: 40, Regime: Dedicação exclusiva.

Outras informações:
PhD em métodos formais e sistemas críticos

Atividades

07/2004 - 08/2004
Outras atividades técnico-científicas , Computing Laboratory, Computing Laboratory.,Atividade realizada, Curso em Metodologia de Pesquisa.
05/2004 - 07/2004
Outras atividades técnico-científicas , Computing Laboratory, Computing Laboratory.,Atividade realizada, Curso em Ensino para alunos de pos-graduacao.
09/2002 - 06/2004
Ensino, Computer Science, Nível: Graduação,Disciplinas ministradas, Object Oriented Modelling and Programming in Java, Java Programming, Java Programming for Business/Computing Students

2001 - 2001

Universidade Federal de Pernambuco

Vínculo: Outro, Enquadramento Funcional: Outro, Carga horária: 8

Outras informações:
Estágio docência. Ministrei as aulas da disciplina de Métodos Formais para a graduação em conjunto com o Professor Augusto Sampaio (acas@cin.ufpe.br)

2001 - 2001

Universidade Federal de Pernambuco

Vínculo: Outro, Enquadramento Funcional: Outro, Carga horária: 8

Outras informações:
Estágio docência na disciplina de métodos formais em conjunto com o professor Augusto Sampaio (acas@cin.ufpe.br)

Atividades

05/2001 - 09/2001
Ensino, Bacharelado em Ciência da Computação, Nível: Graduação,Disciplinas ministradas, Métodos Formais

1999 - 2000

Universidade Salvador

Vínculo: Outro, Enquadramento Funcional: Outro, Carga horária: 20

Outras informações:
Bolsa de Iniciação científica e grupo de pesquisas em Redes ATM sem fio para o NUPERC (núcleo de pesquisa em redes de computadores da UNIFACS) supervisionado pelo professor José Augusto Suruagy Monteiro (suruagy@unifacs.br). Houve ainda a freqüência completa em duas das disciplinas do mestrado em redes de computadores (Avaliação de desempenho de redes e de sistemas)

Atividades

04/1999 - 02/2000
Pesquisa e desenvolvimento , Universidade Salvador, .,Linhas de pesquisa

1998 - 2000

Knowhow Informática

Vínculo: Colaborador, Enquadramento Funcional: Outro, Carga horária: 40

Outras informações:
Desenvolvimento modelagem e projeto orientado a objetos. Servidores COM/DCOM para sincronização de páginas ASP, bitmaps com gradiente, implementação de algoritmo de criptografia (BlowFish e MD5). Família de parsers para C++, Pascal, HTML e solver para expressões matemáticas com o objetivo de aumentar a produtividade no auxílio da construção de arquivos de ajuda (help authoring) e formatação de textos padronizada. Rotinas em ASM para Intel para gerenciamento, pesquisa, comparação e ordenação em memória utilizadas para funcionalidades de baixo nível, gerenciamento de arquivos binários em padrões propietarios e abertos. Como um exemplo da coleção dos componentes já desenvolvidos podemos citar: serviços do Windows NT; monitoramento de performance do SO; depuração "offline" para Delphi; contagem de instâncias remotas e locais para aplicativos; protocolo de mailslot; objetos de sincronização do SO e fila de threads, etc... (mais de 200.000 linhas de puro código orientado a objetos). Construção de Sites com tecnologia ASP, ADO-DB, CGI, etc. Para informações mais detalhadas veja o site www.knowhow-online.com.br

Atividades

08/1998 - 02/2000
Serviços técnicos especializados , Knowhow Informática, .,Serviço realizado, Desenvolvimento de Biblioteca Orientada a Objetos em Delphi (300.000 linhas em 18 bibliotecas).

1997 - 1998

Telecomunições da Bahia Simplestec

Vínculo: Colaborador, Enquadramento Funcional: Outro, Carga horária: 40, Regime: Dedicação exclusiva.

Outras informações:
Coordenador de desenvolvimento para o sistema distribuído on-line chamado DDDX para monitoramento da planta telefônica do estado da Bahia. Desenvolvido para a Telebahia (Telemar). Leitura de chamadas de portas seriais e outros sistemas fornecedores; necessidade de alta performance (parte do código em ASM). Monitoramento e disparo de alarmes para as centrais telefônicas. Programação para redes com Winsock para integração com outros sistemas e módulos desse mesmo sistema. Instrutor para curso de programação avançada e para banco de dados em Delphi 3 para a Telebahia. Administrador da rede NT local

1997 - 1998

Telecomunições da Bahia Simplestec

Vínculo: Outro, Enquadramento Funcional: Outro, Carga horária: 40

Atividades

12/1997 - 07/1998
Serviços técnicos especializados , Telecomunições da Bahia Simplestec, .,Serviço realizado, Implementação do Sistema DDDX de gerenciamento da planta DDD da Bahia.
03/1998 - 06/1998
Treinamentos ministrados , Telecomunições da Bahia Simplestec, .,Treinamentos ministrados, Curso de Delphi Básico 2 turmas de 30 alunos cada, Curso de Delphi Avançado com BD 2 turmas de 30 alunos cada

1997 - 1997

Simetria Métodos e Sistemas

Vínculo: Outro, Enquadramento Funcional: Outro, Carga horária: 40, Regime: Dedicação exclusiva.

Outras informações:
Desenvolvedor Delphi para aplicações comercias e de banco de dados. DBA para sistemas utilizando bancos de dados Paradox e SQL Server. Participante de curso para certificação ISO 9002/03. Instalação, suporte e manutenção de redes ethernet para windows 95/NT. Desenvolvedor e pesquisador Delphi para suporte ao time desenvolvimento bem como pesquisador de soluções para todo tipo de problema de desenvolvimento

Atividades

01/1997 - 12/1997
Serviços técnicos especializados , Simetria Métodos e Sistemas, .,Serviço realizado, Desenvolvimento de Aplicações comerciais em Delphi.

2006 - 2010

University of York

Vínculo: Celetista, Enquadramento Funcional: Senior Researcher (PosDoc), Carga horária: 40

2012 - Atual

Newcastle University

Vínculo: Celetista, Enquadramento Funcional: Lecturer in Formal Methods, Carga horária: 40