Augusto Cezar Alves Sampaio

Professor Titular do Centro de Informática (CIn) da UFPE, possui graduação e mestrado em Ciência da Computação pela UFPE, doutorado pela Oxford University e Pós-Doutorado pela University of York. Em 2021, tornou-se Membro da Academia Pernambucana de Ciências. Em 2018, recebeu o Prêmio Mérito Científico da Sociedade Brasileira de Computação (SBC). Pesquisador Homenageado pelo Simpósio Brasileiro de Engenharia de Software (SBES), em 2017. Em 2016, recebeu o título de Doutor Honoris Causa da University of York. Em 2010, foi agraciado com o título de Comendador da Ordem Nacional do Mérito Científico, pela Presidência da República do Brasil. É o Chair do Formal Methods Europe Fellowship Award Committee. Foi membro do IFIP TC1. A principal área de interesse é Engenharia de Software, com ênfase em Métodos Formais. Tem contribuído com semântica, refinamento e transformação de especificações, modelos e programas concorrentes e orientados a objetos; técnicas composicionais de verificação de modelos (model checking); integração entre métodos formais e semiformais (como UML e SysML); modelos de componentes; e na geração automática de testes a partir de modelos. O foco atual da pesquisa é na modelagem, simulação e verificação de sistemas robóticos em contratos inteligentes (smart contracts). Coordenador Brasileiro do Projeto COMPASS (Comprehensive Modelling for Advanced Systems of Systems), financiado pela Comunidade Europeia, edital FP7, (2011-2014) e Coordenador da Cooperação entre a Motorola Mobility e o CIn-UFPE, desde 2002, com ênfase na geração automática de testes a partir de modelos formais de requisitos, tema também explorado em uma cooperação com a Embraer. É um dos autores do modelo de formação conhecido como Residência em Software, premiado pelo MCT e bastante consolidado. Tem participado ativamente da organização e de comitês de programas das principais conferências nacionais e internacionais em métodos formais e engenharia de software, bem como de comitês assessores da CAPES, do CNPq e de outras agências. Tem contribuído, administrativamente, no CIn-UFPE, como Vice-Coordenador da Graduação, Coordenador da Pós-Graduação, Coordenador de Pesquisa e Coordenador de Cooperação com a Indústria, além da Chefia do Departamento de Ciência da Computação.

Informações coletadas do Lattes em 01/04/2025

Acadêmico

Formação acadêmica

Doutorado em Software Engineering

1989 - 1993

University of Oxford
Título: An Algebraic Approach to Compiler Design
Orientador: Charles A. R. Hoare
Bolsista do(a): Conselho Nacional de Desenvolvimento Científico e Tecnológico, CNPq, Brasil.

Mestrado em Ciências da Computação

1986 - 1988

Universidade Federal de Pernambuco
Título: Zc: Uma Notação para Especificação de Sistemas Complexos, Ano de Obtenção: 1988
Silvio Romero de Lemos Meira.Bolsista do(a): Conselho Nacional de Desenvolvimento Científico e Tecnológico, CNPq, Brasil. Grande área: Ciências Exatas e da Terra

Graduação em Ciencia da Computacao

1982 - 1985

Universidade Federal de Pernambuco

Pós-doutorado

2024

Pós-Doutorado. , University of Oxford, OX, Inglaterra. , Bolsista do(a): Conselho Nacional de Desenvolvimento Científico e Tecnológico, CNPq, Brasil. , Grande área: Ciências Exatas e da Terra

2019 - 2019

Pós-Doutorado. , University of York, YORK, Inglaterra. , Bolsista do(a): Conselho Nacional de Desenvolvimento Científico e Tecnológico, CNPq, Brasil.

Idiomas

Inglês

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

Espanhol

Compreende Razoavelmente, Fala Pouco, Lê Razoavelmente, Escreve Pouco.

Francês

Lê Pouco.

Áreas de atuação

Grande área: Ciências Exatas e da Terra / Área: Ciência da Computaçã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: Metodos Formais.

Organização de eventos

Augusto Sampaio . Membro do Comitê de Programa do FASE (ETAPS) 2021. 2021. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do SEFM 2021. 2021. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do SBMF 2021. 2021. (Congresso).

Augusto Sampaio . Membro do Comitë de Programa do Applicable Formal Methods (appFM2021). 2021. (Congresso).

Augusto Sampaio . Chair do Formal Methods Europe (FME) Awards Committee. 2021. (Outro).

Augusto Sampaio . Chair da Journal-First track do ICST-2021. 2021. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do FASE (ETAPS) 2020. 2020. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do ICTAC 2020. 2020. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do SEFM 2020. 2020. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do SBMF 2020. 2020. (Congresso).

Augusto Sampaio . Chair do Formal Methods Europe (FME) Awards Committee. 2020. (Outro).

Augusto Sampaio . Membro do Comitê de Programa do FASE (ETAPS) 2019. 2019. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do ICTAC 2019. 2019. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do SEFM 2019. 2019. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do Formal Methods (FM) 2019. 2019. (Congresso).

Pedro ribeiro. ; Augusto Sampaio . Chair do Comitê de Programa do UTP 2019. 2019. (Congresso).

Augusto Sampaio . Chair da Journal-First track do FM-2019. 2019. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do ICTAC 2018. 2018. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do SEFM 2018. 2018. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do SBMF 2018. 2018. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do Formal Methods (FM) 2018. 2018. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do ICTAC 2017. 2017. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do ITP 2017. 2017. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do SEFM 2017. 2017. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do SBMF 2017. 2017. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do FM2016 - Formal Methods. 2016. (Congresso).

Augusto Sampaio . PC Chair do ICTAC 2016. 2016. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do SBMF 2016. 2016. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do SEFM 2016. 2016. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do TAP 2016. 2016. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do Doctoral Symposium of Formal Methods. 2015. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do FACS2015 - Formal Aspects of Component Software. 2015. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do FMi2015 - IEEE International Workshop on Formal Methods Integration. 2015. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do ProCoS 2015: Provably Correct Systems. 2015. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do SBMF 2015. 2015. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do SEFM 2015. 2015. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do WTDSoft 2015. 2015. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do ICTAC 2015. 2015. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do FM2014 - Formal Methods. 2014. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do ICTAC 2014. 2014. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do FMi 2014 - IEEE International Workshop on Formal Methods Integration. 2014. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do IFM 2014 - Integrated Formal Methods. 2014. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do SBMF 2014. 2014. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do SEFM 2014. 2014. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do SBES 2014. 2014. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do ICTAC 2013. 2013. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do SBMF 2013. 2013. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do SEFM 2013. 2013. (Congresso).

Augusto Sampaio . Membro do Comitê de Programa do SBES 2013. 2013. (Congresso).

Sampaio, A. . Membro do comite de programa do SBMF. 2012. (Congresso).

Sampaio, A. . Membro do comite de programa do SBES. 2012. (Congresso).

Sampaio, A. . Membro do comite de programa do SEMISH. 2012. (Congresso).

Sampaio, A. . Membro do Steering Committee do ICTAC. 2012. (Congresso).

Sampaio, A. . Membro do comite de programa do SEFM. 2012. (Congresso).

Sampaio, A. . Membro do comite de programa do Formal Methods (FM). 2012. (Congresso).

Sampaio, A. . Membro do comite de programa do SBMF. 2011. (Congresso).

Sampaio, A. . Membro do Steering Committee do ICTAC. 2011. (Congresso).

Sampaio, A. . Membro do comite de programa do SEFM. 2011. (Congresso).

Sampaio, A. . Membro do comite de programa do ICFEM. 2011. (Congresso).

Sampaio, A. . Membro do comite de programa do Formal Methods (FM). 2011. (Congresso).

Sampaio, A. . Membro do comite de programa do SBMF. 2010. (Congresso).

Sampaio, A. . Membro do comite de programa do SBES. 2010. (Congresso).

Sampaio, A. . Membro do Steering Committee do ICTAC. 2010. (Congresso).

Sampaio, A. . Membro do comite de programa do ICFEM. 2010. (Congresso).

Sampaio, A. . Membro do comite de programa do VSTTE. 2010. (Congresso).

Sampaio, A. . Membro do comite de programa do ICTSS. 2010. (Congresso).

Sampaio, A. . Coordenador do comite de programa do II Grandes Desafios. 2010. (Congresso).

Sampaio, A. . Membro do comite de programa do SBMF. 2009. (Congresso).

Sampaio, A. . Membro do comite de programa do SBES. 2009. (Congresso).

Sampaio, A. . Membro do Steering Committee do ICTAC. 2009. (Congresso).

Sampaio, A. . Membro do comite de programa do Formal Methods (FM). 2009. (Congresso).

Sampaio, A. . Membro do comite de programa do Integrated Formal Methods (IFM). 2009. (Congresso).

Sampaio, A. . Membro do comite de programa do SBMF. 2008. (Congresso).

Sampaio, A. . Membro do comite de programa do SBES. 2008. (Congresso).

Sampaio, A. . Membro do Steering Committee do ICTAC. 2008. (Congresso).

Sampaio, A. . Membro do comite de programa do SEFM. 2008. (Congresso).

Sampaio, A. . Membro do comite de programa do Formal Methods (FM). 2008. (Congresso).

Sampaio, A. . Membro do comite de programa da Unifying Theories of Programming (UTP). 2008. (Congresso).

Sampaio, A. . Membro do comite de programa do VSTTE. 2008. (Congresso).

Sampaio, A. . Membro do comite organizador fo CHARLA. 2008. (Congresso).

Sampaio, A. . Membro do comite de programa do SBMF. 2007. (Congresso).

Sampaio, A. . Membro do comite de programa do SBES. 2007. (Congresso).

Sampaio, A. . Membro do Steering Committee do ICTAC. 2007. (Congresso).

Sampaio, A. . Membro do comite de programa do SEFM. 2007. (Congresso).

Sampaio, A. . Membro do comite de programa do JAI. 2007. (Congresso).

Sampaio, A. . Membro do comite de programa do SAST. 2007. (Congresso).

SAMPAIO, A. C. A. . PC Chair do Formal Methods Doctoral Symposium (FM'06). 2006. (Congresso).

SAMPAIO, A. C. A. . Membro do Comitê de Programa do SBES2006. 2006. (Congresso).

SAMPAIO, A. C. A. . Membro do Comitê de Programa do ICTAC2006. 2006. (Congresso).

SAMPAIO, A. C. A. . Membro do Steering Comittee do SBMF2006. 2006. (Congresso).

SAMPAIO, A. C. A. . Membro do Steering Comittee do SBMF2007. 2006. (Congresso).

SAMPAIO, A. C. A. . Membro do Comitê de Programa da International Conferemce on Formal Methods (ICFEM) 2006. 2006. (Congresso).

SAMPAIO, A. C. A. . Membro do Comitê de Programa da Software Engineering and Formal Methods (SEFM) 2006. 2006. (Congresso).

BARROS, E. ; SAMPAIO, A. C. A. ; LIMA, M. . Membro do Comitê Organizador do SBCCI 2006. 2006. (Congresso).

SAMPAIO, A. C. A. . PC Chair do Simpósio Brasileiro de Métodos Formais (SBMF-2005). 2005. (Congresso).

SAMPAIO, A. C. A. . Membro do Comitê de Programa do SBES2005. 2005. (Congresso).

SAMPAIO, A. C. A. . Membro do Comitê de Programa do ICTAC2005. 2005. (Congresso).

SAMPAIO, A. C. A. . Membro do Comitê de Programa da Software Engineering and Formal Methods (SEFM) 2005. 2005. (Congresso).

SAMPAIO, A. C. A. . PC Chair da Comissão de Tutoriais do SBES 2005. 2005. (Congresso).

MOTA, A. ; SAMPAIO, A. C. A. ; A. Farias ; M. Cornelio . Membro da comissão organizadora do SBMF 2004. 2004. (Congresso).

SAMPAIO, A. C. A. ; CAVALCANTI, A. ; WOODCOCK, J. ; Zhiming Liu ; Antonio Cerone . Pernambuco School on Software Engineering - Refinement. 2004. (Congresso).

SAMPAIO, A. C. A. . Membro do Comitê de Programa do SBES2004. 2004. (Congresso).

SAMPAIO, A. C. A. . Membro do Comitê de Programa do ICTAC2004. 2004. (Congresso).

SAMPAIO, A. C. A. . Membro do Comitê de Programa da International Conferemce on Formal Methods (ICFEM) 2004. 2004. (Congresso).

SAMPAIO, A. C. A. . Membro do Comitê de Programa do Software Ebgineering and Formal Methods (SEFM) 2004. 2004. (Congresso).

SAMPAIO, A. C. A. . Membro do Steering Comittee do SBES2003. 2003. (Congresso).

SAMPAIO, A. C. A. . Membro do Steering Comittee do SBES2002. 2002. (Congresso).

SAMPAIO, A. C. A. . Membro do Comitê de Programa da JIISIC2002. 2002. (Congresso).

SAMPAIO, A. C. A. . Membro do Comitê de Programa da International Conferemce on Formal Methods (ICFEM) 2002. 2002. (Congresso).

SAMPAIO, A. C. A. ; HE, J. . Summer School on Object-Oriented Processes and Technologies. 2001. (Congresso).

SAMPAIO, A. C. A. . Membro do Steering Comittee do SBES2001. 2001. (Congresso).

SAMPAIO, A. C. A. . Membro do Comitê de Programa do Formal Methods Europe 2001 (FME 2001). 2001. (Congresso).

SAMPAIO, A. C. A. . PC Chair do Simpósio Brasileiro de Engenharia de Software (SBES-2000). 2000. (Congresso).

SAMPAIO, A. C. A. . Membro do Steering Comittee do SBES99. 1999. (Congresso).

SAMPAIO, A. C. A. . Membro do ComiTê de Programa do Fomal Methods (FM) 99 - World Congress on Formal Methods. 1999. (Congresso).

SAMPAIO, A. C. A. . Membro do Comitê de Programa do SBES98. 1998. (Congresso).

SAMPAIO, A. C. A. . PC Chair do Workshop Brasileiro de Hardware/Software Codesign. 1996. (Congresso).

Participação em bancas

Aluno: Marlom Jobsom Dias de Oliveira

Augusto Sampaio. AETing: An automated exploratory testing strategy based on code evolution coverage. 2020. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.

Aluno: Caio Henrique Bos Loureiro

Augusto Sampaio. Análise da modernização de sistemas monolíticos legados para micro-serviços à luz da dívida técnica: um estudo de caso corporativo. 2018. Dissertação (Mestrado em Ciências da Computação) - Universidade de São Paulo.

Aluno: Jonhnanthan Victor Pereira Oliveira

Augusto Sampaio. Revisiting the Refactoring Names. 2018. Dissertação (Mestrado em Ciência da Computação) - Universidade Federal de Campina Grande.

Aluno: Dalay Israel de Almeida Pereira

Augusto Sampaio. An Extension of a Tool for the Formal Support for Component-based Development. 2017. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

Aluno: Sérgio Barza

Augusto Sampaio. Model Checking of Requirements Written in Controlled Natural Language. 2016. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.

Aluno: Saulo Medeiros de Araujo

Augusto Sampaio. Otimizando Sistemas Itensivos em E/S Através de Programação Concorrente. 2015. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.

Aluno: Madiel de Sousa Conserva Filho

Marcel OliveiraSampaio, Augusto C. A.; Anamaria Moureira. Estendendo CRefine para o Suporte de Táticas de Refinamento. 2011. Dissertação (Mestrado em Matemática Aplicada e Estatistica) - Universidade Federal do Rio Grande do Norte.

Aluno: Breno Alexandro Ferreira de Miranda

Sampaio, Augusto C. A.; P. Machado;Iyoda, Juliano. Recommender Systems for Manual Testing. 2011. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.

Aluno: Adriana Carla Damasceno

Sampaio, Augusto C. A.Alexandre Cabral MotaM. Cornelio. Geração mecanizada de abstrações seguras para especificações CSP. 2008. Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.

Aluno: David Paulo Pereira

Ana Melo; Leliane Barros;SAMPAIO, A. C. A.. Um framework para coordenação do tratamento de exceções em sistemas tolerantes a falhas. 2007. Dissertação (Mestrado em Ciências da Computação) - Universidade de São Paulo.

Aluno: Emanuela Gadelha Cartaxo

P. Machado;SAMPAIO, A. C. A.; Jorge César Abrantes Figueiredo. Geração de Casos de Teste Funcional para Aplicações de Celulares. 2006. Dissertação (Mestrado em Ciência da Computação) - Universidade Federal de Campina Grande.

Aluno: Andre Dantas Rocha

SAMPAIO, A. C. A.; Paulo Masiero; Renata Fortes. Uma Ferramenta Baseada em Aspectos para Apoio ao Teste Funcional de Programas Java. 2005. Dissertação (Mestrado em Ciências da Computação e Matemática Computacional) - Universidade de São Paulo.

Aluno: Cristiano Bertolini

SAMPAIO, A. C. A.. Geração de Casos de Teste Estatisticamente Relevantes através da Descrição Formal de Programas. 2005. Dissertação (Mestrado em Ciência da Computação) - Pontifícia Universidade Católica do Rio Grande do Sul.

Aluno: Rohit Gheyi

SAMPAIO, A. C. A.; David Deharbe;P. Borba. Leis de Modelos e Projetos. 2004. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.

Aluno: Rohit Gheyi

SAMPAIO, A. C. A.. Basic Laws of Object Modeling. 2004. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.

Aluno: Marcel Vinicius Medeiros Oliveira

SAMPAIO, A. C. A.; Ana Melo;CAVALCANTI, A.. ArcAngel: a Tactic Language for Refinement and its Tool Support. 2002. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.

Aluno: Klissiomara Lopes Dias

SAMPAIO, A. C. A.; Virgínia Carvalho Carneiro de Paula;P. Borba. Estruturação de Aplicações Enterprise JAVA Beans. 2002. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.

Aluno: Ricardo André Cavalcante de Souza

SAMPAIO, A. C. A.; Daniel Schwabe; Alexandre Vasconcelos. Uma Extensão do Fluxo de Análise e Projeto do RUP para o Desenvolvimento de Aplicações WEB. 2002. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.

Aluno: Bruno Martis Moutinho

SAMPAIO, A. C. A.; Ana Melo; Francisco Carlos da Rocha Reverbel. Composição de Frameworks JAVA. 2001. Dissertação (Mestrado em Ciências da Computação e Matemática Computacional) - Universidade de São Paulo.

Aluno: Bartira Dantas Rocha

SAMPAIO, A. C. A.. A Linguagem de Discriminação de Arquiteturas ZCLesp. 2000. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

Aluno: Alessandro Cruvinel Machado de Araújo

SAMPAIO, A. C. A.; Jair Leite; Alexandre Vasconcelos. Framework de Análise e Projeto Baseado no RUP para o Desenvolvimento de Aplicações para a WEB. 2000. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.

Aluno: Fred Monteiro da Cruz Filho

SAMPAIO, A. C. A.; Thomaz Barros;BARROS, E.. Particionamento em Hardware/Software usando Redes de Petri. 2000. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.

Aluno: Sandro Alex Damasceno Costa

SAMPAIO, A. C. A.; Angelo Perkusich; Jorge César Abrantes Figueiredo; Evandro de Barros Costa; José Reinaldo Silva. Aspectos de Herança em uma Notação Orientada a Objetos Baseada em Redes de Petri. 1999. Dissertação (Mestrado em Informática) - Universidade Federal da Paraíba.

Aluno: Denise de Oliveira Dias Neves

SAMPAIO, A. C. A.; Francisco Pinheiro;MEIRA, S.. Desenvolvimento de Software como um Processo Contínuo e Reversível usando BON e JAVA. 1997. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.

Aluno: Francisco Vieira de Souza

SAMPAIO, A. C. A.. Gerenciamento de Memória GAMA-CMC. 1994. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.

Aluno: Marum Simão Filho

SAMPAIO, A. C. A.. Uma Ferramenta Gráfica de Apoio ao Projeto de Banco de Dados. 1994. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.

Aluno: VALÉRIA CESÁRIO TIMES

SAMPAIO, A. C. A.. MGeo: Um Modelo Orientado a Objetos para Aplicações Geográficas. 1994. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.

Aluno: Lin Tse Min

SAMPAIO, A. C. A.MEIRA, S.; Fabio Silva. A Semântica Formal de MooZ. 1993. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.

Aluno: Carlos Diego Nascimento Damasceno

Augusto Sampaio. Learning finite state machine models of evolving systems: From evolution over time to variability in space. 2020. Tese (Doutorado em Ciencia da Computacao) - Universidade de São Paulo.

Aluno: Filipe Alves Coelho

Augusto Sampaio. Modelagem de sistemas químicos como máquinas de estados finitos para fins de vericacão formal. 2018. Tese (Doutorado em Doutorado em Engenharia Química) - Universidade Estadual de Campinas.

Aluno: André Luís Ribeiro Didier

Augusto Sampaio. An Algebra of Temporal Faults. 2017. Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco.

Aluno: Henrique Emanuel Mostaert Rebelo

Augusto Sampaio. Contract Modularity in Design By Contract Languages. 2014. Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco.

Aluno: Rodrigo Fraxino de Araújo

Augusto Sampaio. Teste de Modelos de Sistemas Dinâmicos: Uma Contribuição para a Geração Automática de conjuntos de Teste. 2013. Tese (Doutorado em Ciências da Computação) - Universidade de São Paulo.

Aluno: Bruno Emerson Gurgel Gomes

David Deharbe; Anamaria Moureira;Marcel OliveiraSampaio, Augusto C. A.Rohit Gheyi. Desenvolvimento Formal de Aplicações para Smart Cards. 2012. Tese (Doutorado em Matemática Aplicada e Estatistica) - Universidade Federal do Rio Grande do Norte.

Aluno: Paulo Salem da Silva

Ana Melo; Flavio Silva; Marie-Claude Gaudel;Sampaio, Augusto C. A.; Jean-pierre Briot. Verification of behaviourist multi-agent systems by means of formally guided simulations. 2011. Tese (Doutorado em Ciências da Computação) - Universidade de São Paulo.

Aluno: Wilkerson de Lucena Andrade

P. Machado;T. MassoniRohit GheyiSampaio, Augusto C. A.; David Deharbe. Symbolic model-based testing for real-time systems. 2011. Tese (Doutorado em Ciência da Computação) - Universidade Federal de Campina Grande.

Aluno: Cristiano Bertolini

Sampaio, Augusto C. A.P. BorbaIyoda, Juliano; Cristiano Ferraz; Alvaro Moreira. Evaluation of GUI testing techniques for system crashing: from real to model-based controlled experiments. 2010. Tese (Doutorado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.

Aluno: Tiago Lima Massoni

Sampaio, Augusto C. A.Alexandre Cabral MotaIyoda, Juliano; Ana Melo;Marcel Oliveira. A model-driven approach to formal refactoring. 2008. Tese (Doutorado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.

Aluno: Rohit Gheyi

Sampaio, A.Alexandre Cabral Mota. A Refinement Theory for Alloy. 2007. Tese (Doutorado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.

Aluno: Alexandre Luis Correa

SAMPAIO, A. C. A.; Claudia Werner; Julio Leite. Reestruturando Especificações de Restrições de Modelos Elaboradas em OCL. 2006. Tese (Doutorado em Engenharia de Sistemas e Computação) - Universidade Federal do Rio de Janeiro.

Aluno: Sergio Castelo Branco Soares

SAMPAIO, A. C. A.MEIRA, S.; Jaelson Castro; Paulo Masiero; Guilherme Travassos. An Aspect-Oriented Implementation Method. 2004. Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco.

Aluno: Carla Alessandra Lima Reis

SAMPAIO, A. C. A.; Ana Maria de Alencar Price; Paulo Masiero. Uma Abordagem Flexível para Execução de Processos de Software Evolutivos. 2003. Tese (Doutorado em Computação) - Universidade Federal do Rio Grande do Sul.

Aluno: Dalton Dario Serey Guerrero

Wellington Santos Mota;SAMPAIO, A. C. A.; José Reinaldo Silva; TURNELL, M. F.; Antonio Marcus Lima. Redes de Petri Orientadas a Objetos. 2002. Tese (Doutorado em Engenharia Elétrica) - Universidade Federal da Paraíba.

Aluno: Gledson Elias da Silveira

SAMPAIO, A. C. A.; Carlos Ferraz;P. Borba; Claudia Werner. A Framework for Distribution, Management and Evolution of Component-Based Software Systems over Open Networks. 2002. Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco.

Aluno: Dalton Dario Serey Guerrero

SAMPAIO, A. C. A.. Especificação e Análise de Sistemas Concorrentes Utilizando Redes de Petri e Orientação a Objetos. 1999. Tese (Doutorado em Engenharia Eletrica) - Universidade Federal da Paraíba.

Aluno: Virgínia Carvalho Carneiro de Paula

SAMPAIO, A. C. A.; Luiz Fernando Gomes Soares; Noemi Rodriguez; George Roger Ribeiro Justo; Carlos Ferraz. ZCL: A Formal Framework for Specifying Dynamic Distributed Software Architectures. 1999. Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco.

Aluno: Vanderlei Moraes Rodrigues

SAMPAIO, A. C. A.. Transições Síncronas, Lógica Temporal e VHDL. 1998. Tese (Doutorado em Computação) - Universidade Federal do Rio Grande do Sul.

Aluno: André Luís Ribeiro Didier

Augusto Sampaio. An Algebra of Temporal Faults. 2016. Exame de qualificação (Doutorando em Ciências da Computação) - Universidade Federal de Pernambuco.

Aluno: Adirana Carla Damasceno

Augusto Sampaio. Symbolic Test Generation of Compositional Real-Time Systems. 2013. Exame de qualificação (Doutorando em Ciência da Computação) - Universidade Federal de Campina Grande.

Aluno: Leopoldo Motta Teixeira

Augusto Sampaio. Safe Evolution of Software Product Lines. 2012. Exame de qualificação (Doutorando em Ciências da Computação) - Universidade Federal de Pernambuco.

Aluno: Bruno Emerson Gurgel Gomes

David Deharbe; Anamaria Moureira;Sampaio, Augusto C. A.. Desenvolvimento formal de aplicações para Smart Cards. 2010. Exame de qualificação (Doutorando em Matemática Aplicada e Estatistica) - Universidade Federal do Rio Grande do Norte.

Aluno: Rohit Gheyi

SAMPAIO, A. C. A.; Ana Melo;MOTA, A.. A Refinement Theory for Alloy. 2006. Exame de qualificação (Doutorando em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.

Aluno: Rohit Gheyi

Sampaio, A.Alexandre Cabral Mota. A Refinement Theory for Alloy. 2006. Exame de qualificação (Doutorando em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.

Aluno: Tiago Lima Massoni

SAMPAIO, A. C. A.; Edward Hermann Haeusler;Alexandre Cabral Mota. A Model-driven Approach to Program Refactoring. 2005. Exame de qualificação (Doutorando em Ciências da Computação) - Universidade Federal de Pernambuco.

Aluno: Sergio Castelo Branco Soares

SAMPAIO, A. C. A.; Guilherme Travassos; Jaelson Castro. An Aspect-oriented Implementation Method. 2003. Exame de qualificação (Doutorando em Ciências da Computação) - Universidade Federal de Pernambuco.

Aluno: Dalton Dario Serey Guerrero

Benemar Souza; Antonio Marcus Lima; TURNELL, M. F.; José Reinaldo Silva;SAMPAIO, A. C. A.; Carlos Lucena. Especificação e Análise de Sistemas Concorrentes Utilizando Redes de Petri e Orientação a Objetos. 1999. Exame de qualificação (Doutorando em Engenharia Eletrica) - Universidade Federal da Paraíba.

Aluno: Vanderlei Moraes Rodrigues

SAMPAIO, A. C. A.. Transições Síncronas, Lógica Temporal e sua Aplicação na Verificação Formal de VHDL. 1997. Exame de qualificação (Doutorando em Computação) - Universidade Federal do Rio Grande do Sul.

Aluno: André Luís Ribeiro Didier

SAMPAIO, A. C. A.. Automatic Z Data Refinement. 2006. Trabalho de Conclusão de Curso (Graduação em Ciencia da Computacao) - Universidade Federal de Pernambuco.

Aluno: Rafael Oliveira Nóbrega

SAMPAIO, A. C. A.. Framework para Automação de Testes Funcionais utilizando o Rational Functional Tester. 2006. Trabalho de Conclusão de Curso (Graduação em Ciencia da Computacao) - Universidade Federal de Pernambuco.

Aluno: Andrey Pires Batista

SAMPAIO, A. C. A.. Repositório de Design Patterns para Desenvolvedores. 2005. Trabalho de Conclusão de Curso (Graduação em Ciencia da Computacao) - Universidade Federal de Pernambuco.

Aluno: Leonardo Cole Neto

SAMPAIO, A. C. A.. Reestruturando Mobile Server com AspectJ. 2002. Trabalho de Conclusão de Curso (Graduação em Ciencia da Computacao) - Universidade Federal de Pernambuco.

Aluno: Jairson Barbosa Rodrigues

SAMPAIO, A. C. A.. Gerência de Tempo: Uma Visão do PMBOK direcionada ao desenvolvimento de software. 2002. Trabalho de Conclusão de Curso (Graduação em Ciencia da Computacao) - Universidade Federal de Pernambuco.

Aluno: Sandrelly Luiz Coutinho

SAMPAIO, A. C. A.. Estendendo REFINE para Suportar Procedimentos e Recursão. 2000. Trabalho de Conclusão de Curso (Graduação em Ciencia da Computacao) - Universidade Federal de Pernambuco.

Aluno: Marcel Vinicius Medeiros Oliveira

SAMPAIO, A. C. A.. RTL - Uma Linguagem para Definição de Táticas de Refinamento. 2000. Trabalho de Conclusão de Curso (Graduação em Ciencia da Computacao) - Universidade Federal de Pernambuco.

Aluno: Sergio Castelo Branco Soares

SAMPAIO, A. C. A.. Desenvolvimento Sistemático de Programas Concorrentes Orientados a Objetos. 1999. Trabalho de Conclusão de Curso (Graduação em Ciencia da Computacao) - Universidade Federal de Pernambuco.

Augusto Sampaio. Comissão para Progressão para Professor Titular. 2015. Universidade Federal de Minas Gerais.

Sampaio, Augusto C. A.; Claudia Bauzer; Carlos Lucena. Concurso público para provimento de 1 vaga de Professor Titular. 2011. Universidade Estadual de Campinas.

Roberto Bigonha; Marco Casanova; Alberto Laender;Sampaio, Augusto C. A.. Concurso de Professor Adjunto. 2012. Universidade Federal de Minas Gerais.

Sampaio, Augusto C. A.; Teresa Ludermir; Henrique Pacca. Concurso para Professor Adjunto. 2011. Universidade Federal de Pernambuco.

SILVA, L.; Henrique Nou Schneider;SAMPAIO, A. C. A.. Concurso para Professor Assistente. 2004. Universidade Federal de Sergipe.

Ivan Saraiva Silva; Guido Lemos de Sousa Filho;SAMPAIO, A. C. A.. Concurso Público de Provas e Títulos para o Nível I das Classes de Professor Adjunto na área de Métodos Formais. 1998. Universidade Federal do Rio Grande do Norte.

Ângela Souza; Ana Soares;SAMPAIO, A. C. A.. Concurso para Professor Assistente. 1997.

SAMPAIO, A. C. A.. Avaliação Trienal da Capes dos Programas de Pós-Graduação. 2004. Coordenação de Aperfeiçoamento de Pessoal de Nível Superior.

Célio Albuquerque; Edson Cárceres;Sampaio, A.. Concurso de Teses de Doutorado. 2012. Coordenação de Aperfeiçoamento de Pessoal de Nível Superior.

Luis Lamb;Sampaio, Augusto C. A.; Roberto Cesar. Concurso de teses de doutorado. 2011. Coordenação de Aperfeiçoamento de Pessoal de Nível Superior.

Sampaio, Augusto C. A.; Fátima Marques; Luciano Gaspary; Luiz Gonçalves; Saulo Bortolon. Concurso de Trabalhos de Iniciação Científica - CTIC. 2009. Sociedade Brasileira de Computação - Porto Alegre.

Decio Fonseca;SAMPAIO, A. C. A.. XV Concurso de Trabalhos de Iniciação Científica da SBC. 1996. Universidade Federal de Pernambuco.

SAMPAIO, A. C. A.. Seleção de bolsistas de Iniciação Científica. 1996. Universidade Federal de Pernambuco.

Orientou

Gabriel Nogueira Leite

Extracting formal smart contract specifications from natural language with LLMs; Início: 2023; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; (Orientador);

Danilo Rafael de Lima Cabral

Predição de Custo de Gás utilizando Clientes Ethereum; Início: 2022; Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco, Fundação de Apoio à UFPE; (Orientador);

Davi Medeiros Cabral

Safe evolution of smart contracts including loops; Início: 2021; Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco; (Orientador);

Bruno Medeiros de Oliveira

Gas analysis and sound optimisation for smart contracts; Início: 2020; Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco; (Orientador);

Filipe Marques Chaves de Arruda

Início: 2023; Universidade Federal de Pernambuco, Fundação de Apoio à UFPE;

Madiel Conserva Filho

Início: 2020; Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco;

Matheus Vinícius Teotonio do Nascimento Andrade

Arquitetura de microsserviços no backend de sistemas robóticos para competição de futebol; Início: 2024; Trabalho de Conclusão de Curso (Graduação em Ciencia da Computacao) - Universidade Federal de Pernambuco; (Orientador);

Uanderson Ricardo Ferreira da Silva

Arquitetura de microfrontends no frontend de sistemas robóticos para competição de futebol; Início: 2024; Trabalho de Conclusão de Curso (Graduação em Ciencia da Computacao) - Universidade Federal de Pernambuco; (Orientador);

Pedro Vitor Cunha

Modelagem e verificação de robôs para competição 2D; Início: 2024; Iniciação científica (Graduando em Ciência da Computação) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; (Orientador);

Marcus Vinícius de Faria Santos

Modelagem, verificação e implementação de controladores de drones com foco em competição; Início: 2023; Iniciação científica (Graduando em Ciencia da Computacao) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; (Orientador);

Andresa Almeida da Silva

Arquitetura de micro-serviços para enxame de robôs para competição na categoria SSL; Início: 2023; Iniciação científica (Graduando em Ciencia da Computacao) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; (Orientador);

Filipe Marques Chaves de Arruda

Capture & Replay with Text-Based Reuse and Framework Agnosticism; 2022; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Augusto Cezar Alves Sampaio;

Juliandson Estanislau Ferreira

Verification of smart contracts in blockchains; 2022; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Tháis Melise Lopes Pina

AUTO TEST GENERATOR: A FRAMEWORK TO GENERATE TEST CASES FROM REQUIREMENTS IN NATURAL LANGUAGE; 2019; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, Fundação de Apoio à UFPE; Orientador: Augusto Cezar Alves Sampaio;

Rafaela Gonçalves de Almeida

AUTOMATIC TEST CASE GENERATION FOR CONCURRENT FEATURES FROM NATURAL LANGUAGE SPECIFICATIONS; 2019; Dissertação (Mestrado em Informática Aplicada) - Universidade Federal Rural de Pernambuco, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Coorientador: Augusto Cezar Alves Sampaio;

Rodrigo Benedito Otoni

Compositional Analysis of Classical Properties of Concurrency; 2018; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Hugo Leonardo da Silva Araujo

Testing Hybrid Systems from Natural Language Requirements; 2017; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Augusto Cezar Alves Sampaio;

BRUNO CÉSAR FERREIRA SILVA

CPN SIMULATION-BASED TEST CASE GENERATION FROM NATURAL LANGUAGE REQUIREMENTS; 2016; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, ; Orientador: Augusto Cezar Alves Sampaio;

Bruno Medeiros de Oliveira

Simulation of Hybrid Systems from Natural Language Requirements; 2016; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Augusto Cezar Alves Sampaio;

Pedro Ribeiro Gonçalves Antonino

A Refinement Based Strategy for Locally Verifying Networks of CSP Processes; 2014; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Augusto Cezar Alves Sampaio;

David Menezes Cardoso

A framework to support the implementation of monitorable services; 2012; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, ; Orientador: Augusto Cezar Alves Sampaio;

José Dihego da Silva Oliveira

ALGEBRAIC LAWS FOR PROCESS; 2011; Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Centro de Informática, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Augusto Cezar Alves Sampaio;

Renata Bezerra e Silva de Araújo

Extração Automática de Modelos CSP a partir de Casos de Uso; 2011; Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Centro de Informática, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Coorientador: Augusto Cezar Alves Sampaio;

Vitor Torres Braga

Um Processo para Projeto Arquitetural de Software Dirigido a Modelos e Orientado a Serviços; 2011; Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Centro de Informática, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Adriano José Oliveira Gomes

Model-Based Safety Assessment via Probabilistic Model Checking; 2010; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Coorientador: Augusto Cezar Alves Sampaio;

Juliana Nereida Dantas Mafra

Test Case Selector: Uma Ferramenta para Seleção de Testes; 2010; Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Centro de Informática, ; Coorientador: Augusto Cezar Alves Sampaio;

Lucas Albertins de Lima

Test Case Prioritization Based on Data Reuse for Black-Box Environments; 2009; Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Centro de Informática, ; Orientador: Augusto Cezar Alves Sampaio;

Joabe Bezerra de Jesus Júnior

Design and Formal Verification of Fly-By-Wire Flight Control Systems; 2009; Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Centro de Informática, ; Coorientador: Augusto Cezar Alves Sampaio;

Flávia Mérylyn Carneiro Falcão

Multi-Sincronização em Message Sequence Charts; 2008; Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Centro de Informática, ; Orientador: Augusto Cezar Alves Sampaio;

Manoel Messias da Silva Menezes Junior

Mapeando CSP em UML-RT; 2008; Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Centro de Informática, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Augusto Cezar Alves Sampaio;

Rafael Machado Duarte

Paraallelizing Java Programs Using Transformation Laws; 2008; Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Centro de Informática, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Coorientador: Augusto Cezar Alves Sampaio;

Patrícia Muniz Ferreira

Geração Automática de Modelos UML-RT a partir de Especificações CSP; 2006; Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Sidney de Carvalho Nogueira

Geração Automática de Casos de Teste a Partir de Especificações CSP; 2006; Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Augusto Cezar Alves Sampaio;

Gustavo Fonseca Limaverde Cabral

Formal Specification Generation from Requirement Documents; 2006; Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Manuela de Almeida Xavier

Definição e Implementação do Sistema de Tipos da Linguagem Circus; 2006; Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Coorientador: Augusto Cezar Alves Sampaio;

Robson Godoi de Albuquerque Maranhão

Uma Disciplina de Análise e Projeto para Aplicações Concorrentes Baseada no RUP; 2005; Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco, ; Orientador: Augusto Cezar Alves Sampaio;

Rodrigo Teixeira Ramos

Desenvolvimento Rigoroso com UML-RT; 2005; Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Augusto Cezar Alves Sampaio;

Antonio Augusto Rodrigues de Albuquerque Maranhão

Design de uma Linguagem Multiparadigma Modular para o Ensino de Conceitos de Programação; 2004; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, ; Orientador: Augusto Cezar Alves Sampaio;

Walter Miranda Mesqita Neto

Uma Estratégia para Composição Formal de Frameworks; 2004; Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco, ; Orientador: Augusto Cezar Alves Sampaio;

Renata Elaine Mesel Kaufman

Modelagem e Análise de Objetos como Processos em CSP: Padrão de Projeto e Estudo de Caso; 2003; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Augusto Cezar Alves Sampaio;

Adalberto Cajueiro de Farias

Efficient Analysis of CSP-Z Specifications; 2003; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Augusto Cezar Alves Sampaio;

Leonardo José Simões de Freitas

JACK: A Process Algebra Implementation in Java; 2002; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Augusto Cezar Alves Sampaio;

Bruno de Oliveira Lira

Mecanização de Leis Algébricas para Programação Orientada a Objetos; 2002; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, ; Coorientador: Augusto Cezar Alves Sampaio;

Tiago Lima Massoni

Um Processo de Software com Suporte para Implementacao Progressiva; 2001; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Coorientador: Augusto Cezar Alves Sampaio;

Juliano Manabu Iyoda

ParTS - Uma Ferramenta de Suporte ao Particionamento Hardware/Software; 2000; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Augusto Cezar Alves Sampaio;

Adnan Mahamoud Sherif

Formal Specification and Validation of Real Time Systems; 2000; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Augusto Cezar Alves Sampaio;

Érika Carlos Medeiros

Um Ambiente para Desenvolvimento Formal de Programas em OBJ3; 1999; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Augusto Cezar Alves Sampaio;

Leonardo Reis Lucena

Um Ambiente Unificador para as Semânticas de Statecharts; 1999; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Augusto Cezar Alves Sampaio;

Alexandre Cabral Mota

Formalização e Análise do Saci-1 Em CSP-Z; 1997; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Augusto Cezar Alves Sampaio;

VIitgínia Adélia de Oliveira Cordeiro

De Mooz Para Eiffel:Uma Abordagem Rigorosa Para Desenvolvimento de Sistemas; 1994; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Coorientador: Augusto Cezar Alves Sampaio;

Rafaela Gonçalves de Almeida

Increasing coverage of concurrent mobile applications via permutation of test cases; 2024; Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Joabe Bezerra de Jesus Júnior

Formal Round-Trip Engineering for Control Systems; 2023; Tese (Doutorado em Pós-Graduação em Ciência da Computação) - Centro de Informática, ; Orientador: Augusto Cezar Alves Sampaio;

Hugo Leonardo da Silva Araujo

A framework for testing cyber-physical systems: input generation and causality analysis; 2023; Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Flávia Mérylyn Carneiro Falcão

Compositional Analysis and Design of SysML Models; 2022; Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco, ; Orientador: Augusto Cezar Alves Sampaio;

Filipe Marques Chaves de Arruda Consistent

Consistent Test Automation from Natural Language in an Industrial Context; 2022; Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco, Fundação de Apoio à UFPE; Orientador: Augusto Cezar Alves Sampaio;

Tarciana Dias da Silva

Sound Parallelisation of Java Programs; 2017; Tese (Doutorado em Pós-Graduação em Ciência da Computação) - Centro de Informática, ; Orientador: Augusto Cezar Alves Sampaio;

Madiel de Sousa Conserva Filho

Local Livelock Analysis of Component-Based Models; 2017; Tese (Doutorado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte, ; Coorientador: Augusto Cezar Alves Sampaio;

José Dihego da Silva Oliveira

Constructive Extensibility of Trustworthy Component-based Systems; 2016; Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco, ; Orientador: Augusto Cezar Alves Sampaio;

Gustavo Henrique Porto de Carvalho

NAT2TEST: GENERATING TEST CASES FROM NATURAL LANGUAGE REQUIREMENTS BASED ON CSP; 2016; Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco, ; Orientador: Augusto Cezar Alves Sampaio;

Lucas Albertins de Lima

FORMALISATION OF SYSML DESIGN MODELS AND AN ANALYSIS STRATEGY USING REFINEMENT; 2016; Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco, ; Coorientador: Augusto Cezar Alves Sampaio;

Giovanny Fernando Lucero Palma

Algebraic Laws for Object Oriented Programming with References; 2015; Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco, ; Orientador: Augusto Cezar Alves Sampaio;

Sidney de Carvalho Nogueira

Test Generation and Compositional Conformance Verification from Input-Output CSP Models; 2012; Tese (Doutorado em Pós-Graduação em Ciência da Computação) - Centro de Informática, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Augusto Cezar Alves Sampaio;

Rodrigo Teixeira Ramos

Systematic Development of Trustworthy Component-Based Systems; 2011; Tese (Doutorado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Augusto Cezar Alves Sampaio;

Adalberto Cajueiro de Farias

Abstraction of Infinite and Communicating CSPz Processes; 2009; Tese (Doutorado em Pós-Graduação em Ciência da Computação) - Centro de Informática, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Coorientador: Augusto Cezar Alves Sampaio;

Adnan Sherif

A Framework for Specification and Validation of Real Time Systems; 2006; Tese (Doutorado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Augusto Cezar Alves Sampaio;

ADOLFO ALMEIDA DURAN

An Algebraic Approach to the Design of Compilers for Object-Oriented Languages; 2005; Tese (Doutorado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Augusto Cezar Alves Sampaio;

Márcio Lopes Cornélio

Refactoring as Formal Refinement; 2004; Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Coorientador: Augusto Cezar Alves Sampaio;

Roberta Vilhena Vieira

GAADT - Um Algorimo Genético Baseado em Tipos Abstratos de Dados; 2003; Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Augusto Cezar Alves Sampaio;

Alexandre Cabral Mota

Model Checking Data-Dependent CSP-Z Processes; 2001; Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Augusto Cezar Alves Sampaio;

Leila Maciel de Almeida Silva

An Algebraic Approach to Hardware/Software Partitioning; 2000; Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Augusto Cezar Alves Sampaio;

Madiel Conserva Filho

2019; Universidade Federal de Pernambuco, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Augusto Cezar Alves Sampaio;

André Luís Ribeiro Didier

2017; Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Augusto Cezar Alves Sampaio;

Giovanny Lucero Palma

2016; Universidade Federal de Pernambuco, ; Augusto Cezar Alves Sampaio;

Leila Maciel de Almeida e Silva

2015; Universidade Federal de Pernambuco, ; Augusto Cezar Alves Sampaio;

Marcel Vinicius Medeiros Oliveira

2012; Centro de Informática, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Augusto Cezar Alves Sampaio;

Juliano Manabu Iyoda

Integração de Métodos Formais e semi-formais usando HOL; 2008; Centro de Informática, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Augusto Cezar Alves Sampaio;

Leila Maciel de Almeida e Silva

Leis Algébricas para Linguagens Orientadas a Objetos e Aplicações; 2008; Centro de Informática, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Augusto Cezar Alves Sampaio;

Carolina Baldisserotto, Maíra Fernandes e Leonardo Lima

Use Case Designer (UCD): An Assistant to Define Feature Use Cases based on a Controlled Natural Language; 2006; Monografia; (Aperfeiçoamento/Especialização em Curso Sequencial de Formação Complementar) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

José Galiza e Evisson Fernandes

Test Case Selection Tool; 2006; Monografia; (Aperfeiçoamento/Especialização em Curso Sequencial de Formação Complementar) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Pollyana Barbosa, Shirlly Silva e Valéria Bezerra

Automatic Test Cases Generation using Tool PTK by Motorola; 2006; Monografia; (Aperfeiçoamento/Especialização em Curso Sequencial de Formação Complementar) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Adilton Magalhães, Paulo Barbosa, Pedro Cardoso Silva

Test Case Designer - A Tool to Generate Automated Test Cases based on TAF Framework; 2005; Monografia; (Aperfeiçoamento/Especialização em Curso Sequencial de Formação Complementar) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Thiago Holanda Rego

Griffon Tool; 2004; Monografia; (Aperfeiçoamento/Especialização em Curso Sequencial de Formação Complementar) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Adriana Damasceno

Babel - A Protocol Translation Tool; 2004; Monografia; (Aperfeiçoamento/Especialização em Curso Sequencial de Formação Complementar) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

André Lacerda e Felipe de Andrade

A Propposed Standard for High Level Tests; 2004; Monografia; (Aperfeiçoamento/Especialização em Curso Sequencial de Formação Complementar) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Danielly Karine da Silva Cruz

Otimizacao do Processo de Teste da Motorola; 2003; Monografia; (Aperfeiçoamento/Especialização em Curso Sequencial de Formação Complementar) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

José Edson FIlho e Sidney Nogueira

Improvement Automating Test Cases; 2003; Monografia; (Aperfeiçoamento/Especialização em Curso Sequencial de Formação Complementar) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Börge Karlsson, Rodrigo Teixeira e Thiago Santos

Phoenix - Estudo de Caso da Aplicação de Padrões para Reestruturação de uma Ferramenta de Testes; 2003; Monografia; (Aperfeiçoamento/Especialização em Curso Sequencial de Formação Complementar) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Jorge Cavalcanti e Glauco Vasconcelos Jr

; X-Classes - Uma Ferramenta para Geração de Mutantes; 2003; Monografia; (Aperfeiçoamento/Especialização em Curso Sequencial de Formação Complementar) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Isadora Marvão e Wanessa Lopes

Automation Process of Test Cases; 2003; Monografia; (Aperfeiçoamento/Especialização em Curso Sequencial de Formação Complementar) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Carlos Melo, João Farias e Paulo ALves Jr

; Sistema de Apoio à Automação de Testes - TASS; 2003; Monografia; (Aperfeiçoamento/Especialização em Curso Sequencial de Formação Complementar) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Neli Espíndola Duarte

Modelagem dos Processos de Teste do Time TDMA; 2003; Monografia; (Aperfeiçoamento/Especialização em Curso Sequencial de Formação Complementar) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Luís Carlos da Silva e Maria Chantal da Silva

CMMI in Sanity and Feature Test Processes; 2003; Monografia; (Aperfeiçoamento/Especialização em Curso Sequencial de Formação Complementar) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Helga Souza e Carlos Albuquerque

Uso do Test Central no Processo de Testes; 2003; Monografia; (Aperfeiçoamento/Especialização em Curso Sequencial de Formação Complementar) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Audir Filho, Bergson Barros, Humberto Neto, Gustavo Alves

PTFA ddON-Cel (Configurando, Executando e Gerando Logs Amigáveis); 2003; Monografia; (Aperfeiçoamento/Especialização em Curso Sequencial de Formação Complementar) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Renata Maria Bezerra Pereira

Rational Unified Process; 2002; Monografia; (Aperfeiçoamento/Especialização em Especialização em Informática na Educação) - Universidade Federal de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Gabriel Nogueira Leite

Generating formal specifications for smart contracts from textual descriptions in natural language; 2023; Trabalho de Conclusão de Curso; (Graduação em Ciencia da Computacao) - Universidade Federal de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Victor Hugo Silva do Nascimento

Síntese de arquitetura orientada a serviços a partir de casos de uso; 2016; Trabalho de Conclusão de Curso; (Graduação em Ciência da Computação) - Universidade Federal de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Tomaz de Aquino dos Santos Junior

CRITÉRIOS DE COBERTURA DE TESTES GERADOS A PARTIR DE LINGUAGEM NATURAL; 2015; Trabalho de Conclusão de Curso; (Graduação em Ciência da Computação) - Universidade Federal de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Eduardo Bastos Rocha

VERIFICAÇÃO DE CONFORMIDADE A PARTIR DE MODELOS EM CSP DERIVADOS DE REQUISITOS EM CNL; 2013; Trabalho de Conclusão de Curso; (Graduação em Ciência da Computação) - Universidade Federal de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Eudes José Gomes Cavalcanti Sobrinho

BOAS PRÁTICAS PARA O DESENVOLVIMENTO ÁGIL DE SERVIÇOS EM STARTUPS; 2013; Trabalho de Conclusão de Curso; (Graduação em Ciência da Computação) - Universidade Federal de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Gabrielle Batista Campos

ORIENTAÇÕES PARA O DESENVOLVIMENTO DE APLICAÇÕES MÓVEIS SENSÍVEIS AO CONTEXTO; 2013; Trabalho de Conclusão de Curso; (Graduação em Ciência da Computação) - Universidade Federal de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Hugo Leonardo da Silva Araujo

EXTENSÃO DA FERRAMENTA TARGET PARA GERAÇÃO AUTOMATIZADA DE CASOS DE TESTE A PARTIR DO USO DE VARIÁVEIS; 2013; Trabalho de Conclusão de Curso; (Graduação em Ciência da Computação) - Universidade Federal de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Diogo Cavalcanti Peixoto

Integrando SOA e MDD ao RUP; 2011; Trabalho de Conclusão de Curso; (Graduação em Graduação em Ciência da Computação) - Centro de Informática; Orientador: Augusto Cezar Alves Sampaio;

Pedro Ribeiro Gonçalves Antonino

Transformações Automatizadas para Herança de Processos em OhCircus; 2011; Trabalho de Conclusão de Curso; (Graduação em Graduação em Ciência da Computação) - Centro de Informática; Orientador: Augusto Cezar Alves Sampaio;

Renato Parente

Corretude de Transições de Modelos de Análise para Projeto no RUP; 2010; Trabalho de Conclusão de Curso; (Graduação em Graduação em Ciência da Computação) - Centro de Informática; Orientador: Augusto Cezar Alves Sampaio;

Camila Sá da Fonseca

Evolução Automatizada de Modelos Arquiteturais Concorrentes; 2010; Trabalho de Conclusão de Curso; (Graduação em Graduação em Ciência da Computação) - Centro de Informática; Orientador: Augusto Cezar Alves Sampaio;

Gleibson Rodrigo Silva de Oliveira

Geração de Modelos de Teste em CSP a Partir de Casos de Uso; 2009; Trabalho de Conclusão de Curso; (Graduação em Graduação em Ciência da Computação) - Centro de Informática; Orientador: Augusto Cezar Alves Sampaio;

David Menezes Cardoso

Um modelo para monitoramento do fluxo de execução de serviços; 2008; Trabalho de Conclusão de Curso; (Graduação em Graduação em Ciência da Computação) - Centro de Informática; Orientador: Augusto Cezar Alves Sampaio;

José Dihego da Silva Oliveira

Automação de Leis de Refatoração Arquitetural; 2008; Trabalho de Conclusão de Curso; (Graduação em Graduação em Ciência da Computação) - Centro de Informática; Orientador: Augusto Cezar Alves Sampaio;

Renata Bezerra e Silva de Araújo

Regression Test Selection to reduce escaped defects; 2008; Trabalho de Conclusão de Curso; (Graduação em Graduação em Ciência da Computação) - Centro de Informática; Orientador: Augusto Cezar Alves Sampaio;

Fernando Valente Kakimoto

Síntese de Projeto Arquitetural a partir de Realizações de Casos; 2008; Trabalho de Conclusão de Curso; (Graduação em Graduação em Ciência da Computação) - Centro de Informática; Orientador: Augusto Cezar Alves Sampaio;

André Barros Braga

Automatização e análise de completude para aplicações de transformações em modelos com concorrência; 2008; Trabalho de Conclusão de Curso; (Graduação em Graduação em Ciência da Computação) - Centro de Informática; Orientador: Augusto Cezar Alves Sampaio;

Bruno Rodrigues de Castro Ribeiro

Geração do Projeto da Arquitetura no RUP a partir da Análise de Casos de Uso; 2007; Trabalho de Conclusão de Curso; (Graduação em Graduação em Ciência da Computação) - Centro de Informática; Orientador: Augusto Cezar Alves Sampaio;

Flávia Leite Soares

Realizando Padrões de Workflow Em Sistemas Baseados em Componentes; 2007; Trabalho de Conclusão de Curso; (Graduação em Graduação em Ciência da Computação) - Centro de Informática; Orientador: Augusto Cezar Alves Sampaio;

Ricardo Silva Melo Fernandes

Automação de Testes; 2006; Trabalho de Conclusão de Curso; (Graduação em Ciencia da Computacao) - Universidade Federal de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Gustavo da Fonseca Limaverde Cabral

Automação do Processo de Transformação de Modelos UML-RT; 2004; Trabalho de Conclusão de Curso; (Graduação em Ciencia da Computacao) - Universidade Federal de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Gustavo Henrique Ribeiro de Oliveira

Análise de Ferramentas de Cobertura de Testes; 2004; Trabalho de Conclusão de Curso; (Graduação em Ciencia da Computacao) - Universidade Federal de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Carla Maria Pinheiro do Nascimento

ZRC-Refine: Uma Ferramenta para Refinamento; 2003; Trabalho de Conclusão de Curso; (Graduação em Ciencia da Computacao) - Universidade Federal de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Rodrigo Teixeira Ramos

Geração Automática de JAVA Assertions a partir de Especificações CSPZ; 2002; Trabalho de Conclusão de Curso; (Graduação em Ciencia da Computacao) - Universidade Federal de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Manuela de Almeida Xavier

Refine: Procedimentos e Recursão; 2002; Trabalho de Conclusão de Curso; (Graduação em Ciencia da Computacao) - Universidade Federal de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Gabriel Almeida Schneider

Geração Automática de Testes a Partir de Requisitos em Linguagem Natural; 2021; Iniciação Científica; (Graduando em Ciência da Computação) - Universidade Federal de Pernambuco, Projeto CIn-UFPE / Motorola; Orientador: Augusto Cezar Alves Sampaio;

Hugo Leonardo da Silva Araujo

Ferramenta de suporte à geração de casos de teste a partir de modelos CSP; 2012; Iniciação Científica; (Graduando em Ciencia da Computacao) - Universidade Federal de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Diogo Filipe Dornelas Falcão

Uma ferramenta para geração de vetores de testes a partir de especificações SCR; 2012; Iniciação Científica; (Graduando em Ciencia da Computacao) - Universidade Federal de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Raquel Soares de Almeida

Álgebras de Refinamento e Aplicações; 1998; Iniciação Científica; (Graduando em Ciencia da Computacao) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Augusto Cezar Alves Sampaio;

Renata Campelo Spencer Netto

PISH: Projeto Integrado de Software e Hardware; 1997; Iniciação Científica; (Graduando em Ciencia da Computacao) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Augusto Cezar Alves Sampaio;

Juliano Manabu Iyoda

Álgebras de Refinamento e Aplicações; 1997; Iniciação Científica; (Graduando em Ciencia da Computacao) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Augusto Cezar Alves Sampaio;

Leonardo Freire de Andrade

Gláucia Maria dos Santos Ferreira

Álgebras de Refinamento e Aplicações; 1996; Iniciação Científica; (Graduando em Ciencia da Computacao) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Augusto Cezar Alves Sampaio;

Juan Perna

Correct hardware synthesis; 2009; Orientação de outra natureza; (Ciencia da Computacao) - Universidade Federal de Pernambuco; Orientador: Augusto Cezar Alves Sampaio;

Produções bibliográficas

JESUS, JOABE ; Sampaio, Augusto . Local deadlock analysis of Simulink models based on timed behavioural patterns and theorem proving. SCIENCE OF COMPUTER PROGRAMMING , v. 236, p. 103113, 2024.
TER BEEK, MAURICE H. ; CHAPMAN, ROD ; CLEAVELAND, RANCE ; GARAVEL, HUBERT ; GU, RONG ; TER HORST, IVO ; KEIREN, JEROEN J. A. ; LECOMTE, THIERRY ; LEUSCHEL, MICHAEL ; ROZIER, KRISTIN YVONNE ; Sampaio, Augusto ; SECELEANU, CRISTINA ; THOMAS, MARTYN ; WILLEMSE, TIM A. C. ; ZHANG, LIJUN . Formal Methods in Industry. FORMAL ASPECTS OF COMPUTING , v. 1, p. 1, 2024.
ANTONINO, PEDRO ; FERREIRA, JULIANDSON ; Sampaio, Augusto ; ROSCOE, A. W. ; ARRUDA, FILIPE . A refinement-based approach to safe smart contract deployment and evolution. Software and Systems Modeling , v. 1, p. 1, 2024.
FALCÃO, FLÁVIA ; Lima, Lucas ; Sampaio, Augusto ; ANTONINO, PEDRO . A formal component model for UML based on CSP aiming at compositional verification. Software and Systems Modeling , v. 1, p. 1, 2023.
Cavalcanti, Ana ; CONSERVA FILHO, MADIEL ; RIBEIRO, PEDRO ; Sampaio, Augusto . Laws of Timed State Machines. COMPUTER JOURNAL , v. 67, p. 2066-2107, 2023.
DIHEGO, JOSÉ ; Sampaio, Augusto ; OLIVEIRA, MARCEL . A refinement checking based strategy for component-based systems evolution. JOURNAL OF SYSTEMS AND SOFTWARE , v. 167, p. 110598, 2020.
ARRUDA, FILIPE ; BARROS, FLÁVIA ; Sampaio, Augusto . Automation and consistency analysis of test cases written in natural language: An industrial context. SCIENCE OF COMPUTER PROGRAMMING , v. 189, p. 102377, 2020.
Cavalcanti, Ana ; Sampaio, Augusto ; MIYAZAWA, ALVARO ; RIBEIRO, PEDRO ; FILHO, MADIEL CONSERVA ; DIDIER, ANDRÉ ; LI, WEI ; TIMMIS, JON . Verified simulation for robotics. SCIENCE OF COMPUTER PROGRAMMING , v. 174, p. 1-137, 2019.
Nogueira, Sidney ; ARAUJO, HUGO ; ARAUJO, RENATA ; Iyoda, Juliano ; Sampaio, Augusto . Test case generation, selection and coverage from natural language. SCIENCE OF COMPUTER PROGRAMMING , v. 181, p. 84-110, 2019.
SILVA, BRUNO CESAR F. ; CARVALHO, GUSTAVO ; Sampaio, Augusto . CPN simulation-based test case generation from controlled natural-language requirements. SCIENCE OF COMPUTER PROGRAMMING , v. 181, p. 111-139, 2019.
CONSERVA FILHO, M.S. ; OLIVEIRA, M.V.M. ; Sampaio, A. ; Cavalcanti, Ana . Compositional and Local Livelock Analysis for CSP. INFORMATION PROCESSING LETTERS , v. 1, p. 1, 2018.
Sampaio, Augusto ; WANG, FARN . Theoretical aspects of computing. THEORETICAL COMPUTER SCIENCE , v. 744, p. 1-2, 2018.
GHEYI, ROHIT ; BORBA, PAULO ; Sampaio, Augusto ; RIBEIRO, MÁRCIO . An idiom to represent data types in Alloy. Information and Software Technology , v. 82, p. 173-176, 2017.
Lima, Lucas ; MIYAZAWA, ALVARO ; Cavalcanti, Ana ; CORNÉLIO, MÁRCIO ; Iyoda, Juliano ; Sampaio, Augusto ; HAINS, RALPH ; LARKHAM, ADRIAN ; LEWIS, VAUGHAN . An integrated semantics for reasoning about SysML design models using refinement. Software & Systems Modeling , v. 16, p. 875-902, 2017.
ARAUJO, HUGO ; CARVALHO, GUSTAVO ; MOHAQEQI, MORTEZA ; MOUSAVI, MOHAMMAD REZA ; Sampaio, Augusto . Sound Conformance Testing for Cyber-Physical Systems: Theory and Implementation. SCIENCE OF COMPUTER PROGRAMMING , v. 1, p. 1, 2017.
FALASCHI, MORENO ; Sampaio, Augusto . Editorial. FORMAL ASPECTS OF COMPUTING , v. 29, p. 381-382, 2017.
OLIVEIRA, M. V. M. ; ANTONINO, P. ; RAMOS, R. ; Sampaio, A. ; MOTA, A. ; ROSCOE, A. W. . Rigorous development of component-based systems using component metadata and patterns. Formal Aspects of Computing , v. 1, p. 1-68, 2016.
CARVALHO, GUSTAVO ; Cavalcanti, Ana ; Sampaio, Augusto . Modelling timed reactive systems from natural-language requirements. Formal Aspects of Computing (Internet) , v. 1, p. 1-41, 2016.
Nogueira, Sidney ; Sampaio, Augusto ; Mota, Alexandre . Test generation from state based use case models. Formal Aspects of Computing (Internet) , v. 26, p. 441-490, 2014.
CARVALHO, GUSTAVO ; FALCÃO, DIOGO ; BARROS, FLÁVIA ; Sampaio, Augusto ; Mota, Alexandre ; MOTTA, LEONARDO ; BLACKBURN, MARK . Test case generation from natural language requirements based on SCR specifications. Science of Computer Programming (Print) , v. 95, p. 275-297, 2014.
Sampaio, Augusto ; Nogueira, Sidney ; Mota, Alexandre ; ISOBE, YOSHINAO . Sound and mechanised compositional verification of input-output conformance. Software Testing, Verification & Reliability , v. 24, p. 289-319, 2014.
Naumann, David A. ; Sampaio, Augusto ; Silva, Leila . Refactoring and representation independence for class hierarchies. Theoretical Computer Science , v. 433, p. 60-97, 2012.
Gomes, Adriano ; Mota, Alexandre ; Sampaio, Augusto ; Ferri, Felipe ; Watanabe, Edson . Constructive model-based analysis for safety assessment. International Journal on Software Tools for Technology Transfer (Internet) , v. 1, p. 1-30, 2012.
Duarte, Rafael ; Mota, Alexandre ; Sampaio, Augusto . Introducing concurrency in sequential Java via laws. Information Processing Letters (Print) , v. 111, p. 129-134, 2011.
Perna, Juan ; Woodcock, Jim ; Sampaio, Augusto ; Iyoda, Juliano . Correct hardware synthesis. Acta Informatica , v. 48, p. 363-396, 2011.
Ramos, Rodrigo ; Sampaio, Augusto ; Mota, Alexandre . Conformance notions for the coordination of interaction components. Science of Computer Programming (Print) , v. 75, p. 350-373, 2010.
M. Cornelio ; Cavalcanti, Ana ; Sampaio, Augusto . Sound Refactorings. Science of Computer Programming (Print) , v. 75, p. 106-133, 2010.
Sherif, Adnan ; Cavalcanti, Ana ; Jifeng, He ; Sampaio, Augusto . A process algebraic framework for specification and validation of real-time systems. Formal Aspects of Computing , v. 22, p. 153-191, 2010.
Duran, Adolfo ; Cavalcanti, Ana ; Sampaio, Augusto . An algebraic approach to the design of compilers for object-oriented languages. Formal Aspects of Computing , v. 22, p. 489-535, 2010.
FalcÃ£o, FlÃ¡via ; IYODA, J ; Iyoda, Juliano ; Sampaio, Augusto . Multiple Synchrony in MSC. Electronic Notes in Theoretical Computer Science , v. 240, p. 149-166, 2009.
Cabral, Gustavo ; Sampaio, Augusto . Automated formal specification generation and refinement from requirement documents. Journal of the Brazilian Computer Society (Impresso) , v. 14, p. 87-106, 2008.
FERREIRA, P ; SAMPAIO, A ; Mota, A . Viewing CSP Specifications with UML-RT Diagrams?. Electronic Notes in Theoretical Computer Science , v. 195, p. 57-74, 2008.
XAVIER, M ; Cavalcanti, A ; SAMPAIO, A . Type Checking Circus Specifications. Electronic Notes in Theoretical Computer Science , v. 195, p. 75-93, 2008.
Farias, Adalberto ; Mota, Alexandre ; Sampaio, Augusto . Compositional abstraction of CSP Z processes. Journal of the Brazilian Computer Society (Impresso) , v. 14, p. 23-44, 2008.
Cavalcanti, Ana ; Sampaio, Augusto ; Woodcock, Jim . Unifying classes and processes. Software and Systems Modeling (Print) , Alemanha, v. 4, n.3, p. 277-296, 2005.
CORNELIO, M ; Cavalcanti, A ; SAMPAIO, A . Refactoring Towards a Layered Architecture. Electronic Notes in Theoretical Computer Science , v. 130, p. 281-300, 2005.
Silva, Leila ; Sampaio, Augusto ; Barros, Edna . A Constructive Approach to Hardware/Software Partitioning. Formal Methods in System Design , v. 24, p. 45-90, 2004.
BORBA, P ; SAMPAIO, A. C. A. ; CAVALCANTI, A. ; M. Cornelio . Algebraic reasoning for object-oriented programming. Science of Computer Programming (Print) , v. 52, p. 53-100, 2004.
SAMPAIO, A ; Alexandre Cabral Mota ; Rodrigo Ramos . Class and Capsule Refinement in UML for Real Time. Electronic Notes in Theoretical Computer Science , v. 95, p. 23-51, 2004.
Cavalcanti, Ana ; Sampaio, Augusto ; Woodcock, Jim . A Refinement Strategy for Circus. Formal Aspects of Computing , Inglaterra, v. 15, n.2-3, p. 146-181, 2003.
Cavalcanti, A ; SAMPAIO, A ; WOODCOCK, J . Refinement of Actions in Circus,. Electronic Notes in Theoretical Computer Science , v. 70, p. 132-162, 2002.
CORNELIO, M ; Cavalcanti, A ; SAMPAIO, A . Refactoring by Transformation. Electronic Notes in Theoretical Computer Science , v. 70, p. 311-330, 2002.
Mota, A ; SAMPAIO, A. C. A. . Model-checking CSP-Z: strategy, tool support and industrial application. Science of Computer Programming (Print) , Holanda, v. 40, n.1, p. 59-96, 2001.
P. Borba ; SAMPAIO, A. C. A. . Basic Laws of ROOL: an Object-Oriented Language. Revista de Informática Teórica e Aplicada , Brasil, v. 7, n.1, p. 49-68, 2000.
Cavalcanti, A ; Sampaio, Augusto ; WOODCOCK, J. . An inconsistency in procedures, parameters, and substitution in the refinement calculus. Science of Computer Programming (Print) , Amsterdam, v. 33, n.1, p. 87-96, 1999.
Cavalcanti, Ana ; Sampaio, Augusto ; Woodcock, Jim . Procedures and Recursion in the Refinement Calculus. Journal of the Brazilian Computer Society (Impresso) , BRASIL, v. 5, n.1, p. 5-19, 1998.
Campos, Marcilia A. ; Sampaio, Augusto C. A. ; Brainer, Alexandre H. F. . Mechanising the theory of intervals using OBJ3????????????? ??????? ? ?????? ?????????? ?????????????? OBJ3. Reliable Computing , Amsterdam, v. 2, p. 97-102, 1996.
HOARE, C. A. R. ; Jifeng, He ; Sampaio, A. . Normal form approach to compiler design. Acta Informatica , Estados Unidos, v. 30, p. 701-739, 1993.
Simon Foster (Org.) ; Augusto Sampaio (Org.) . The Application of Formal Methods: Essays Dedicated to Jim Woodcock on the Occasion of His Retirement. 1. ed. Springer, 2024. v. 1. 388p .
RIBEIRO, PEDRO (Org.) ; Sampaio, Augusto (Org.) . Lecture Notes in Computer Science. 1. ed. Springer International Publishing, 2019. v. 1. 200p .
Augusto Sampaio ; Farn Wang (Org.) . Theoretical Aspects of Computing. 1. ed. Elsevier - Theoretical Computer Science, 2018. v. 744. 170p .
Augusto Sampaio ; Farn Wang. . Theoretical Aspects of Computing ? ICTAC 2016. 1. ed. Berlin: Springer - Lecture Notes in Computer Science, 2016. v. 1. 479p .
P. Borba (Org.) ; CAVALCANTI, A. (Org.) ; Sampaio, Augusto (Org.) ; WOODCOCK, J. (Org.) . Testing Techniques in Software Engineering. 1. ed. Berlin: Springer Berlin / Heidelberg, 2010. v. 6153. 287p .
SAMPAIO, A. C. A. . Proceedings of the Second Brazilian Symposium on Formal Methods (SBMF 2005). 184. ed. Elsevier ENTCS - Electronic Notes in Theoretical Computer Scince, 2007. v. 1. 234p .
CAVALCANTI, A. (Org.) ; SAMPAIO, A. C. A. (Org.) ; WOODCOCK, J. (Org.) . Refinement Techniques in Software Engineering. Berlin: Springer (Lecture Notes in Computer Science - Tutorial, Vol 3167), 2006. v. 3167. 391p .
SAMPAIO, A. C. A. . Simpósio Brasileiro de Métodos Formais. 2. ed. SBC - Sociedade Brasileira de Computação, 2005. 200p .
SAMPAIO, A. C. A. . Simpósio Brasileiro de Engenharia de Software. 14. ed. Porto Alegre: SBC - Sociedade Brasileira de Computação, 2000. v. 1. 387p .
SAMPAIO, A. C. A. . An Algebraic Approach To Compiler Design. 1. ed. Londres: World Scientific, 1997. v. 4. 200p .
WOODCOCK, J. ; CAVALCANTI, A. ; Simon Foster ; OLIVEIRA, MARCEL ; Augusto Sampaio ; Frank Zeyda . UTP, Circus, and Isabelle. In: J.P. Bowen; Q. Li; Q. Xu. (Org.). Theories of Programming and Formal Methods: Essays Dedicated to Jifeng He on the Ocasion of his 80th Birthday. 1ed.: Springer - Lecture Notes in Computer Science, 2023, v. 14080, p. 19-51.
Cavalcanti, Ana ; Barnett, Will ; Baxter, James ; CARVALHO, GUSTAVO ; FILHO, MADIEL CONSERVA ; MIYAZAWA, ALVARO ; RIBEIRO, PEDRO ; Sampaio, Augusto . RoboStar Technology: A Roboticist¿s Toolbox for Combined Proof, Simulation, and Testing. Software Engineering for Robotics. 1ed.: Springer International Publishing, 2021, v. , p. 249-293.
Gibson-Robinson, Thomas ; Broadfoot, Guy ; CARVALHO, GUSTAVO ; Hopcroft, Philippa ; Lowe, Gavin ; Nogueira, Sidney ; O¿Halloran, Colin ; Sampaio, Augusto . FDR: From Theory to Industrial Application. In: Concurrency, Security, and Puzzles. (Org.). Lecture Notes in Computer Science. 1ed.Berlin: Springer International Publishing, 2017, v. 10160, p. 65-87.
P. Machado ; Sampaio, Augusto . Automatic Test-Case Generation. Testing Techniques in Software Engineering. Berlin: Springer Berlin / Heidelberg, 2010, v. 6153, p. 59-103.
SAMPAIO, A. C. A. ; Antônio Maranhão . Conceitos e Paradigmas de Programação via Projeto de Interpretadores. In: Tomasz Kowaltowski; Karin Breitman. (Org.). JAI - Jornadas de Atualização em Informática 2008. Rio de Janeiro: PUC Rio, 2008, v. , p. 13-54.
SAMPAIO, A. C. A. ; P. Borba . Transformation Laws for Sequential Object-Oriented Programming. In: Ana Cavalcanti; Augusto Sampaio; Jim Woodcock. (Org.). Refinement Techniques in Software Engineering. Berlin: Springer (Lecture Notes in Computer Science - Tutorial, Vol. 3167), 2006, v. 3167, p. 18-63.
CAVALCANTI, A. ; SAMPAIO, A. C. A. ; WOODCOCK, J. . Refinement: an Overview. In: Ana Cavalcanti; Augusto Sampaio; Jim Woodcock. (Org.). Refinement Techniques in Software Engineering. 1ed.Berlin: Springer (Lecture Notes in Computer Science - Tutorial, Vol. 3167), 2006, v. 3167, p. 1-17.
T. Massoni ; SAMPAIO, A. C. A. ; P. Borba . A RUP-Based Software Process Supporting Progressive Implementation. In: L. Favre. (Org.). UML and the Unified Process. Hershey: Idea Grup Inc, 2003, v. , p. 375-397.
HOARE, C. A. R. ; HE, J. ; SAMPAIO, A. C. A. . Algebraic Derivation of an Operational Semantics. In: G. Plotkin; C. Stirling; M. Tofte. (Org.). Proof, Language and Interaction: Essays in Honour of Robin Milner. Massachusetts: MIT, 2000, v. , p. 77-98.
Augusto Sampaio ; Iyoda, Juliano . Engenharia de Sistemas de Sistemas. Computação Brasil, p. 40.
CARVALHO, GUSTAVO ; Augusto Sampaio ; MOTA, A. ; BARROS, FLÁVIA . NAT2TEST: from Natural Language Requirements to Test Cases. Aerospace America Magazine - 2014 in Review, p. 45 - 45.
Gabriel Leite ; Filipe Arruda. ; Pedro Antonino ; Augusto Sampaio ; ROSCOE, A. W. . Extracting Formal Smart-Contract Specifications from Natural Language with LLMs. In: Formal Aspects of Component Software, 2024, Milão. Formal Aspects of Component Software. 20th International Conference, FACS 2024, 2024. v. 15189. p. 109-126.
Gustavo Carvalho ; Jose Dihego ; Augusto Sampaio . An Integrated Framework for Analysing, Simulating and Testing UML Models. In: Simpósio Brasileiro de Métodos Formais, 2024, Vitória. Formal Methods: Foundations and Applications, 2024. v. 15403. p. 86-104.
FERREIRA, J. ; Pedro Antonino ; Augusto Sampaio ; ROSCOE, A. W. ; Filipe Arruda. . Trusted Deployer: A Tool for Safe Creation and Upgrade of Ethereum Smart Contracts. In: Simpósio Brasileiro de Métodos Formais, 2024, Vitória. Formal Methods: Foundations and Applications, 2024. v. 15403. p. 194-204.
Rafaela Almeida ; Sidney Nogueira ; Augusto Sampaio . Sound Test Case Generation for Concurrent Mobile Features. In: Brazilian Symposium on Formal Methods, 2023, Manaus. SBMF - Brazilian Symposium on Formal Methods, 2023. v. 14414. p. 92-109.
Marcus Santos ; Madiel Conserva. ; Augusto Sampaio . A Model-based Approach to the Development and Verification of Robotic Systems for Competitions. In: Latin American Robotics Symposium and Brazilian Symposium on Robotics, 2023, Salvador. LARS/SBR - Latin American Robotics Symposium and Brazilian Symposium on Robotics, 2023. p. 236-241.
Pedro Antonino ; FERREIRA, J. ; SAMPAIO, A ; ROSCOE, A. W. . Specification is Law: Safe Creation and Upgrade of Ethereum Smart Contracts.. In: Software Engineering and Formal Methods (SEFM 2022), 2022, Berlin. Schlingloff, BH., Chai, M. (eds) Software Engineering and Formal Methods. SEFM 2022., 2022. v. 13550. p. 227-243.
Joabe Jesus ; Sampaio, A. . Compositional Verification of Simulink Block Diagrams Using tock-CSP and CSP-Prover. In: Brazilian Symposium on Formal Methods, 2022. SBMF 2022, 2022. p. 91-108.
Mingzhuo Zhang ; Dehui du ; Augusto Sampaio ; Ana Cavalcanti ; Conserva Filho, Madiel S. ; Menghan Zhang . Verification of RoboSim Models Using UPPAAL. In: Theoretical Aspects of Software Engineering (TASE), 2021, Shangai. The 15th International Symposium on Theoretical Aspects of Software Engineering (TASE), 2021, 2021. p. 1-8.
Hugo Araujo. ; Gustavo Carvalho ; MOUSAVI, MOHAMMAD REZA ; Augusto Sampaio . Multi-objective Search for Effective Testing of Cyber-Physical Systems. In: SEFM - Software Engineering Formal Methods, 2019, Oslo. Software Engineering and Formal Methods. SEFM 2019. Berlin: Springer - Lecture Notes in Computer Science, 2019. v. 11724. p. 183-202.
CAVALCANTI, A. ; MIYAZAWA, ALVARO ; Augusto Sampaio . Modelling and Verification for Swarm Robotics. In: IFM - Integrated Formal Methods, 2018, Ireland. 14th International Conference on integrated Formal Methods, 2018. v. 11023. p. 1-19.
Rafaela Almeida ; Sidney Nogueira ; Augusto Sampaio . Automatic Test Case Generation for Concurrent Features from Natural Language Descriptions. In: SBMF - Simpósio Brasileiro de Métodos Formais, 2018, Salvador. SBMF 2018, 2018. v. 11254. p. 163-179.
Flávia Falcão ; Lucas Lima ; Augusto Sampaio . Safe and Constructive Design with UML Components. In: SBMF Simpósio Brasileiro de Métodos Formais, 2018, Salvador. SBMF 2018, 2018. v. 11254. p. 234-251.
Tainã Santos ; Gustavo Carvalho ; Augusto Sampaio . Formal Modelling of Environment Restrictions from Natural-Language Requirements. In: SBMF - Simpósio Brasileiro de Métodos Formais, 2018, Salvador. SBMF 2018, 2018. v. 11254. p. 252-270.
ARAUJO, HUGO ; CARVALHO, GUSTAVO ; Sampaio, Augusto ; MOUSAVI, MOHAMMAD REZA ; TAROMIRAD, MASOUMEH . A Process for Sound Conformance Testing of Cyber-Physical Systems. In: 2017 IEEE International Conference on Software Testing, Verification and Validation: Workshops (ICSTW), 2017, Tokyo. 2017 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW), 2017. p. 46-50.
Rodrigo Otoni ; CAVALCANTI, A. ; Augusto Sampaio . Local Analysis of Determinism for CSP. In: Simpósio Braileiro de Métodos Formais (SBMF), 2017, Recife. SBMF 2017: Formal Methods: Foundations and Applications. Lecture Notes in Computer Science (LNCS), 2017. v. 10623. p. 107-124.
OLIVEIRA, BRUNO ; CARVALHO, GUSTAVO ; MOUSAVI, MOHAMMAD REZA ; Sampaio, Augusto . Simulation of hybrid systems from natural-language requirements. In: 2017 13th IEEE Conference on Automation Science and Engineering (CASE 2017), 2017, Xi'an. 2017 13th IEEE Conference on Automation Science and Engineering (CASE), 2017. p. 1320.
Filipe Arruda. ; Augusto Sampaio ; BARROS, FLÁVIA . Capture & Replay with Text-Based Reuse and Framework Agnosticism. In: Software Engineering and Knowledge Engineering, 2016, San Francisco. SEKE 2016 - Software Engineering and Knowledge Engineering, 2016. p. 1.
Madiel Conserva ; Marcel Oliveira ; Sampaio, Augusto ; CAVALCANTI, A. . Local Livelock Analysis of Component-Based Models. In: ICFEM, 2016. International Conference on Formal Engineering Methods, 2016. v. 10009. p. 279-295.
Augusto Sampaio ; Filipe Arruda. . Formal Testing from Natural Language in an Industrial Context. In: SBMF, 2016, Natal. Brazilian Symposium on Formal Methods, 2016. v. 10090. p. 21-38.
Sergio Barza. ; Gustavo Carvalho ; Iyoda, Juliano ; Augusto Sampaio ; Alexandre Cabral Mota ; F. Barros . Model Checking Requirements. In: SBMF, 2016, Natal. Brazilian Symposium on Formal Methods, 2016. v. 10090. p. 217-234.
Lucas Lima ; Iyoda, Juliano ; Augusto Sampaio . Refinement Verification of Sequence Diagrams Using CSP. In: SBMF, 2016, Natal. Brazilian Symposium on Formal Methods, 2016. v. 10090. p. 235-252.
Cavalcanti, Ana ; HIERONS, ROBERT M. ; Nogueira, Sidney ; Sampaio, Augusto . A Suspension-Trace Semantics for CSP. In: 2016 10th International Symposium on Theoretical Aspects of Software Engineering (TASE), 2016, Shanghai. 2016 10th International Symposium on Theoretical Aspects of Software Engineering (TASE), 2016. p. 3-13.
DIHEGO, JOSÉ ; Sampaio, Augusto ; OLIVEIRA, MARCEL . Constructive extensibility of trustworthy component-based systems. In: the 30th Annual ACM Symposium, 2015, Salamanca. Proceedings of the 30th Annual ACM Symposium on Applied Computing - SAC '15. p. 1808-1814.
Gustavo Carvalho ; F. Barros ; Carvalho, Ana ; CAVALCANTI, A. ; MOTA, A. ; Sampaio, Augusto . NAT2TEST Tool: From Natural Language Requirements to Test Cases Based on CSP. In: SEFM (tool paper), 2015, York. Software Engineering and Formal Methods, 2015. p. 283-290.
Jose Dihego ; Sampaio, Augusto . Aspect-Oriented Development of Trustworthy Component-based Systems. In: ICTAC - International Colloquium on Theoretical Aspects of Computing, 2015, Cali. Theoretical Aspects of Computing - ICTAC 2016, 2015. v. 9399. p. 425-444.
Tarciana Dias ; Sampaio, Augusto ; Mota, Alexandre . Verifying Transformations of Java Programs Using Alloy. In: SBMF - Brazilian Symposium on Formal Methods, 2015, Belo Horizonte. Formal Methods: Foundations and Applications - 18th Brazilian Symposium, SBMF. Berlim: Springer - Lecture Notes in Computer Science, 2015. v. 9526. p. 110-126.
Sidney Nogueira ; Hugo Araujo. ; Renata Araujo ; IYODA, J ; Sampaio, Augusto . Automatic Generation of Test Cases and Test Purposes from Natural Language. In: SBMF - Brazilian Symposium on Formal Methods, 2015, Belo Horizonte. Formal Methods: Foundations and Applications - 18th Brazilian Symposium, SBMF. Berlim: Springer - Lecture Notes in Computer Science, 2015. v. 9526. p. 145-161.
Bruno Silva ; CARVALHO, GUSTAVO ; Sampaio, Augusto . Test Case Generation from Natural Language Requirements Using CPN Simulation. In: SBMF - Brazilian Symposium on Formal Methods, 2015, Belo Horizonte. Formal Methods: Foundations and Applications - 18th Brazilian Symposium, SBMF. Berlim: Springer - Lecture Notes in Computer Science, 2015. v. 9526. p. 178-193.
Lima, Lucas ; Iyoda, Juliano ; Sampaio, Augusto . A Formal Semantics for Sequence Diagrams and a Strategy for System Analysis.. In: Proceedings of the 2nd International Conference on Model-Driven Engineering and Software Development (MODELSWARD 2014), 2014, Lisboa. Proceedings of the 2nd International Conference on Model-Driven Engineering and Software Development (MODELSWARD 2014), 2014. p. 317-324.
Pedro Antonino ; Augusto Sampaio ; Woodcock, Jim . A Refinement Based Strategy for Local Deadlock Analysis of Networks of CSP Processes. In: Formal Methods, 2014, Cingapura. FM 2014: Formal Methods, 2014. v. 8442. p. 62-77.
Frank Zeyda ; T. Santos ; CAVALCANTI, A. ; Augusto Sampaio . A Modular Theory of Object Orientation in Higher-Order UTP. In: Formal Methods, 2014, Cingapura. FM 2014: Formal Methods, 2014. v. 8442. p. 627-642.
Pedro Antonino ; Marcel Oliveira ; Augusto Sampaio ; Klaus Kristenses ; Jeremy Bryans . Leadership Election: An Industrial SoS Application of Compositional Deadlock Verification. In: NASA Formal Methods, 2014, Houston. NASA Formal Methods, 2014. v. 8430. p. 31-45.
Gustavo Carvalho ; Carvalho, Ana. ; Rocha, Eduardo ; CAVALCANTI, A. ; Sampaio, Augusto . A Formal Model for Natural-Language Timed Requirements of Reactive Systems. In: ICFEM, 2014, Luxemburgo. International Conference on Formal Engineering Methods, 2014. v. 8829. p. 43-58.
Marcel Oliveira ; Sampaio, Augusto ; Conserva Filho, Madiel S. . Model-Checking Circus State-Rich Specifications. In: IFM, 2014, Bartinoro. Integrated Formal Methods, 2014. v. 8739. p. 39-54.
Giovanny Lucero ; David Naumann ; Sampaio, Augusto . Laws of Programming for References. In: APLAS - 11th Asian Symposium,, 2013, Melbourne. Programming Languages and Systems - 11th Asian Symposium, APLAS 2013. v. 8301. p. 124-130.
Jose Dihego ; Pedro Antonino ; Sampaio, Augusto . Algebraic Laws for Process Subtyping. In: 15th International Conference on Formal Engineering Methods, ICFEM 2013, 2013, Queenstown. Formal Methods and Software Engineering - 15th International Conference on Formal Engineering Methods, ICFEM 2013, 2013. v. 8144. p. 4-19.
Gustavo Carvalho ; Sampaio, Augusto ; Alexandre Cabral Mota . A CSP Timed Input-Output Relation and a Strategy for Mechanised Conformance Verification. In: 15th International, 2013, Queenstown. Formal Methods and Software Engineering - 15th International Conference on Formal Engineering Methods, ICFEM 2013, 2013. v. 8144. p. 148-164.
CARVALHO, GUSTAVO ; FALCÃO, DIOGO ; BARROS, FLÁVIA ; Sampaio, Augusto ; Mota, Alexandre ; MOTTA, LEONARDO ; BLACKBURN, MARK . Test case generation from natural language requirements based on SCR specifications. In: the 28th Annual ACM Symposium, 2013, Coimbra. Proceedings of the 28th Annual ACM Symposium on Applied Computing - SAC '13. New York: ACM Press, 2013. p. 1217-1222.
Gustavo Carvalho ; Digo Falcão ; Mota, Alexandre ; Sampaio, Augusto . A Process Algebra Based Strategy for Generating Test Vectors from SCR Specifications. In: SBMF - Simpósio Brasileiro de Métodos Formais, 2012, Natal. Proceedings of the Brazilian Symposium on Formal Methods. Berlin: Splringer, 2012.
CARDOSO, DAVID ; Sampaio, Augusto . A framework for monitorable services implementation. In: 2012 Sixth Brazilian Symposium on Software Components, Architectures and Reuse (SBCARS), 2012, Natal. 2012 Sixth Brazilian Symposium on Software Components, Architectures and Reuse.
Joabe Jesus ; Alexandre Cabral Mota ; Sampaio, Augusto C. A. ; Luiz Grijo . Architectural verification of control systems using CSP. In: ICFEM'11 Proceedings of the 13th international conference on Formal methods and software engineering, 2011, Durham. ICFEM'11 Proceedings of the 13th international conference on Formal methods and software engineering. Berlin, Heidelberg: Springer-Verlag, Lecture Notes in Computer Science (DOI: 10.1007/978-3-642-24559-6_23), 2011. v. 6991. p. 323-339.
Silva, Leila ; Naumann, David A. ; Sampaio, Augusto . Refactoring and representation independence for class hierarchies. In: the 12th Workshop, 2010, Maribor. Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs - FTFJP '10. New York: ACM Press. v. 12. p. 1-6.
Gomes, Adriano ; MOTA, A. ; Sampaio, Augusto C. A. ; Ferri, Felipe ; Buzzi, Julio . Systematic Model-Based Safety Assessment via Probabilistic Model Checking. In: Isola - International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, 2010, Creta. 4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation. Berlin: Springer - Lecture Notes in Computer Science (DOI: 10.1007/978-3-642-16558-0_50), 2010. v. 4.
Rodrigo Ramos ; SAMPAIO, A. C. A. ; Alexandre Cabral Mota . Systematic Development of Trustworthy Component Systems. In: FM2009 - 16th International Symposium on Formal Methods, 2009, Eindhoven. 16th International Symposium on Formal Methods. Berlin: Springer Verlag - Lecture Notes in Computer Science (DOI: 10.1007/978-3-642-05089-3_10), 2009.
SAMPAIO, A. C. A. ; Sidney Nogueira ; Alexandre Cabral Mota . Compositional Verification of Input Output Conformance via CSP Refinement Checking. In: ICFEM - International Conference on Formal Engineering Methods, 2009, Rio de Janeiro. International Conference on Formal Engineering Methods. Berlin: Springer Verlag - Lecture Notes in Computer Science (DOI: 10.1007/978-3-642-10373-5_2), 2009.
Renata Kaufman ; SAMPAIO, A. C. A. ; Alexandre Cabral Mota . Formalisation and Analysis of Objects as CSP Processes. In: Simpósio Brasileiro de Métodos Formais, 2009, Gramado. Lecture Notes in Computer Science (DOI: 10.1007/978-3-642-10452-7_16), 2009. v. 5902. p. 236-250.
Rohit Gheyi ; T. Massoni ; P. Borba ; SAMPAIO, A. C. A. . A Complete Set of Object Modeling Laws for Alloy. In: SBMF - Simpósio Brasileiro de Métodos Formais, 2009, Gramado. Lecture Notes in Computer Science (DOI: 10.1007/978-3-642-10452-7_14), 2009. v. 5902. p. 204-219.
Juliana Mafra ; Breno Miranda ; IYODA, J. ; SAMPAIO, A. C. A. . Test Case Selector: Uma Ferramenta para Seleção de Testes. In: SAST - Workshop Brasileiro de Teste de Software Sistemático e Automatizado, 2009, Gramado. Workshop Brasileiro de Teste de Software Sistemático e Automatizado. Porto Alegre: SBC - Sociedade Brasileira de Computação, 2009.
Lima, Lucas ; Iyoda, Juliano ; Sampaio, Augusto ; Aranha, Eduardo . Test case prioritization based on data reuse an experimental study. In: 2009 3rd International Symposium on Empirical Software Engineering and Measurement (ESEM), 2009, Lake Buena Vista. 2009 3rd International Symposium on Empirical Software Engineering and Measurement.
Ramos, Rodrigo ; Sampaio, Augusto ; Mota, Alexandre . Framework composition conformance via refinement checking. In: the 2008 ACM symposium, 2008, Fortaleza. Proceedings of the 2008 ACM symposium on Applied computing - SAC '08. New York: ACM Press. v. 23. p. 119-125.
Sidney Nogueira ; SAMPAIO, A. C. A. ; Alexandre Cabral Mota . Guided Test Generation from CSP Models. In: ICTAC - International Colloquium on Theoretical Aspects of Computing, 2008, Istanbul. ICTAC 2008 - International Colloquium on Theoretical Aspects of Computing. Berlin: Springer - Lecture Notes in Computer Science (DOI: 10.1007/978-3-540-85762-4_18), 2008. v. 5160. p. 258-273.
Silva, Leila ; Sampaio, Augusto ; Liu, Zhiming . Laws of Object-Orientation with Reference Semantics. In: , 2008, Cape Town. . p. 217-226.
Rodrigo Ramos ; SAMPAIO, A. C. A. ; MOTA, A. . Transformation Laws for UML-RT. In: IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS?06), 2006, Bologna - Itália. IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS?06). Berlin: Springer - Lecture Notes in Computer Science, 2006. v. 4037. p. 123-138.
SAMPAIO, A. C. A. ; Hermano Moura ; Alexandre Vasconcelos . Residência em Software. In: Simpósio Brasileiro de Qualidade de Software (Sessão Prêmio Dorgival Brandão Júnior da Qualidade e Produtividade de Software), 2006, Vila Velha. Simpósio Brasileiro de Qualidade de Software. Porto Alegre: SBC, 2006. p. 150-157.
T. Santos ; CAVALCANTI, A. ; SAMPAIO, A. C. A. . Object-Orientation in the UTP. In: Unifying Theories of Programming (UTP 2006), 2006, Walworth Castle. Unifying Theories of Programming, International Symposium, Revised Selected Papers. Berlin: Springer - Lecture Notes in Computer Science (DOI: 10.1007/11768173_2). v. 4010. p. 18-37.
Gustavo Cabral ; SAMPAIO, A. C. A. . Formal Specification Generation from Requirement Documents. In: SBMF - Simpósio Brasileiro de Métodos Formais, 2006, Natal. SBMF - Simpósio Brasileiro de Métodos Formais. Porto Alegre: SBC, 2006. p. 217-232.
Patrícia Ferreira ; SAMPAIO, A. C. A. ; MOTA, A. . Viewing CSP specifications with UML-RT diagrams. In: SBMF - Simpósio Brasileiro de Métodos Formais, 2006, Natal. SBMF - Simpósio Brasileiro de Métodos Formais. Porto Alegre: SBC, 2006. p. 73-88.
Manuela Xavier ; CAVALCANTI, A. ; SAMPAIO, A. C. A. . Type Checking Circus Specifications. In: SBMF - Simpósio Brasileiro de Métodos Formais, 2006, Natal. SBMF - Simpósio Brasileiro de Métodos Formais. Porto Alegre: SBC, 2006. p. 105-120.
A. Sherif ; HE, J. ; CAVALCANTI, A. ; SAMPAIO, A. C. A. . A Framework for Specification and Validation of Real-Time Systems Using Circus Actions. In: International Colloquiun Theoretical Aspects of Computing - ICTAC 2004, 2005, Guiyang, China. Lecture Notes in Computer Science. Londres: Springer, 2004. v. 3407. p. 478-493.
Rodrigo Ramos ; SAMPAIO, A. C. A. ; MOTA, A. . A Semantics for UML-RT Active Classes via Mapping into Circus. In: IFIP Conference on Formal Methods for Open Object-based Distributed Systems, 2005, Atenas. 7th IFIP Conference on Formal Methods for Open Object-based Distributed Systems. Lecture Notes in Computer Science.. Londres: Springer - Lecture Notes in Computer Science, 2005. v. 3535. p. 99-114.
Mesquita, W. ; Sampaio, A. ; de Melo, A.C.V. . A strategy for the formal composition of frameworks. In: , 2005, Koblenz. . p. 404-413.
Sampaio, Augusto ; Albuquerque, Carlos ; Vasconcelos, Joåo ; Cruz, Luckerson ; Figueiredo, Luis ; Cavalcante, Sergio . Software test program. In: the 27th international conference, 2005, St. Louis. Proceedings of the 27th international conference on Software engineering - ICSE '05. New York: ACM Press. p. 611-612.
A. Farias ; MOTA, A. ; SAMPAIO, A. C. A. . Efficient CSPZ Data Abstraction. In: Integrated Formal Methods, 2004, Canterbury. 4th International Conference on Integrated Formal Methods. Lecture Notes in Computer Science (LNCS). Berlin: Springer Verlag, 2004. v. 2999. p. 108-127.
Leonardo Cole ; Eduardo Piveta ; SAMPAIO, A. C. A. . RUP Based Analysis and Design with Aspects. In: SBES - Simpósio Brasileiro de Engenharia de Software, 2004, Brasília. SBES 2004 - Simpósio Brasileiro de Engenharia de Software. Porto Alegre: SBC - Sociedade Braileira de Computação, 2004. v. XVIII. p. 210-224.
P. Borba ; SAMPAIO, A. C. A. ; M. Cornelio . A Refinement Algebra for Object-Oriented Programming. In: ECOOP - European Conference on Object-Oriented Programming, 2003, Darmstadt. ECOOP 2003. Berlin: Springer-Verlag (Lecture Notes in Computer Science), 2003. v. 2743. p. 457-482.
A. Sherif ; SAMPAIO, A. C. A. ; S. Cavalcanti . Specification and Validation of the SACI-1 On-Board Computer Using Timd-CSP-Z and Petri Nets. In: Application and Theory of Petri Nets, 2003, Eindhoven. 24th International Conference on Application and Theory of Petri Nets. Berlin: Springer-Verlag (Lecture Notes in Computer Science) Vol. 2679, 2003. v. 2679. p. 161-180.
A. Duran ; CAVALCANTI, A. ; SAMPAIO, A. C. A. . A Strategy for Compiling Classes, Inheritance, and Dynamic Binding. In: Formal Methods, 2003, Pisa. FME 2003: Formal Methods. Berlin: Springer Verlag, 2003. v. 2805. p. 301-320.
SAMPAIO, A. C. A. ; WOODCOCK, J. ; CAVALCANTI, A. . Refinement in Circus. In: FME - Formal Methods Europe, 2002, Compenhaguem. FME 2002: Formal Methods - Getting IT Right. Berlin: Springer-Verlag (Lecture Notes in Computer Science), 2002. v. 2391. p. 451-470.
MOTA, A. ; P. Borba ; SAMPAIO, A. C. A. . Mechanical Abstraction of CSP-Z Processes. In: FME - Formal Methods Europe, 2002, Compenhaguem. FME 2002 - Formal Methods - Getting IT Right. Berlin: Springer-Verlag (Lecture Notes in Computer Science), 2002. v. 2391. p. 163-183.
A. Duran ; SAMPAIO, A. C. A. ; CAVALCANTI, A. . Refinement Algebra for Formal Bytecode Generation. In: ICFEM - International Conference on Formal Engineering Methods, 2002, Shangai. Formal Methods and Software Engineering. Berlin: Springer-Verlag (Lecture Notes in Computer Science), 2002. v. 2495. p. 347-358.
L. Freitas ; SAMPAIO, A. C. A. ; CAVALCANTI, A. . JACK: A Framework for Process Algebra Implementation in Java. In: Simpósio Brasileiro de Engenharia de Software, 2002, Gramado. XVI Simpósio Brasileiro de Engenharia de Software. Gramado: SBC - Sociedade Brasileira de Computação, 2002. v. 16. p. 98-113.
A. Farias ; MOTA, A. ; SAMPAIO, A. C. A. . Efficient Analysis of Infinite CSP-Z Specifications. In: Workshop de Métodos Formais, 2002, Gramado. V Workshop de Métodos Formais. Gramado: SBC - Sociedade Brasileira de Computação, 2002. v. 5. p. 113-128.
B. Oliveira ; CAVALCANTI, A. ; SAMPAIO, A. C. A. . The Automation of a Normal Form Reduction Strategy for Object-Oriented Programming. In: Workshop de Métodos Formais, 2002, Gramado. V Workshop de Métodos Formais. Gramado: SBC - Sociedade Brasileira de Computação, 2002. v. 5. p. 193-208.
CAVALCANTI, A. ; SAMPAIO, A. C. A. . From CSP-OZ to Java with Processes. In: International Parallel and Distributed Processing Symposium - IPDPD 2002, 2002. Workshop on Formal Methods for Parallel Programming - FMPP. v. 16. p. 1-15.
A. Sherif ; SAMPAIO, A. C. A. ; S. Cavalcanti . An Integrated Approach to Specification and Validation of Real-Time Systems. In: Formal Methods Europe (FME'2001), 2001, Berlin. FME2001: Formal Methods for Increasing Software Productivity. Berlin: Springer-Verlag (Lecture Notes in Computer Science), 2001. v. 2021. p. 278-299.
SILVA, L. ; SAMPAIO, A. C. A. ; G. Jones . Serialising Parallel Processes in a Hardware/Software Partitioning Context. In: Formal Methods Europe - FME'2001, 2001, Berlin. FME 2001 - Formal Methods for Increasing Software Productivity. Berlin: Springer-Verlag (Lecture Notes in Computer Sceince), 2001. v. 2021. p. 344-363.
P. Borba ; SAMPAIO, A. C. A. . Basic Laws of ROOL: an Object-Oriented Language. In: Workshop de Metodos Formais, 2000, Joao Pessoa. SBES'2000 - Workshops, 2000. v. 14. p. 33-44.
SILVA, L. ; SAMPAIO, A. C. A. ; BARROS, E. ; IYODA, J. . An Algebraic Approach to Combining Processes in a Hardware/Software Partitioning Environment. In: Algebraic Methodology and Software Technology - AMAST, 1999, Manaus. (AMAST'98). New York: Springer-Verlag (Lecture Notes in Computer Science), 1999. v. 1548. p. 308-324.
IYODA, J. ; SAMPAIO, A. C. A. ; SILVA, L. . ParTS: A Partitioning Transformation System. In: FM'99 - World Congress on Formal Methods, 1999, Toulouse. Lecture Notes in Computer Science, 1999. v. 1709. p. 1400-1419.
SAMPAIO, A. C. A. ; SILVA, L. ; BARROS, E. ; IYODA, J. . An Algebraic Approach to Codesign. In: Workshop on Provably Correct Systems, 1999, Toulouse. Formal Methods Europe. Toulouse: Springer-Verlag, 1999.
MOTA, A. ; SAMPAIO, A. C. A. . Model-Checking CSP-Z. In: FASE'98 - Fundamental Approaches to Software Engineering, 1998, Lisboa. ETAPS'98 - European Joint Conferences on Theory and Practice of Software. New York: Springer-Verlag, 1998. v. 1382. p. 205-220.
MOTA, A. ; SAMPAIO, A. C. A. . Model-Checking Processes With States: An Industrial Case Study. In: Anais do XII Simposio Brasileiro de Engenharia de Software, 1998, Maringá. (SBES'98). Maringa/PR: SBC, 1998. v. 12. p. 23-36.
SAMPAIO, A. C. A. ; SILVA, L. ; BARROS, E. . A Normal Form Reduction Strategy For Hardware/Software Partitioning. In: Formal Methods Europe, 1997, Gratz. (FME'97). Graz/Austria: Springer-Verlag, 1997. v. 1313. p. 624-643.
SILVA, L. ; SAMPAIO, A. C. A. ; BARROS, E. . Projeto Integrado de Hardware e Software Com Ênfase Em Corretude: Um Estudo de Caso. In: XXIV Seminario Integrado de Software e Hardware, 1997, Brasília. (XVII Congresso da SBC). BRASÍLIA/DF: SBC, 1997. v. 27. p. 47-58.
SAMPAIO, A. C. A. ; SPENCER, R. . De Occam Para O Transputer: Compilacao Via Reescrita de Termos. In: X Simposio Brasileiro de Engenharia de Software, 1996. (SBES'96). SÃO CARLOS/SP. p. 103-117.
SAMPAIO, A. C. A. ; PIRES, A. . Formalizacao Algebrica de Um Metodo Para Particionamento Hardware/Software. In: IX Simposio Brasileiro de Concepcao de Circuitos Integrados, 1996. (SSBCCI'96). Recife/PE. p. 285-296.
SAMPAIO, A. C. A. ; SILVA, L. ; BARROS, E. . A Transformational Approach to Hardware/Software Partitioning. In: Hardware Synthesis and Verification Workshop, 1996, Ithaca. Hardware Synthesis and Verification Workshop, 1996.
SAMPAIO, A. C. A. . Reusing Algebraic Theories in Program Transformation. In: Program Transformation Workshop, 1996, Durham. Program Transformation Workshop, 1996.
SAMPAIO, A. C. A. ; LIMA, J. . Um Método de Desenvolvimento de Programas Para Obj3. In: XXII SEMISH/PANEL95, 1995. (SBC'95). Canela/RS. p. 1051-1062.
CAMPOS, M. ; SAMPAIO, A. C. A. ; BRAINER, A. . Proving Algebraic Properties Of Intervals Using OBJ3. In: XVIII SIMPÓSIO BRASILEIRO DE MATEMÁTICA APLICADA E COMPUTACIONAL, 1995. (SBMAC'95). Curitiba/PR. p. 118-122.
CORDEIRO, V. ; SAMPAIO, A. C. A. ; MEIRA, S. . From Mooz To Eiffel:A Rigorous Approach To System Development. In: FORMAL METHODS EUROPE'94, 1994. FROM MOOZ TO EIFFEL:A RIGOROUS APPROACH TO SYSTEM DEVELOPMENT. PARIS. p. 306-325.
BARROS, E. ; SAMPAIO, A. C. A. . Toward Provably Correct Hardware Partitioning Using Occam. In: PROCEEDINGS OF THE THIRD INTERNATIONAL WORKSHOP ON HARDWARE/SOFTWARE CODESIGN (IEEE COMPUTER SOCIETY PRESS), 1994. TOWARD PROVABLY CORRECT HARDWARE/SOFTWARE PARTITIONING USING OCCAM. FRANCE. p. 210-217.
CORDEIRO, V. ; SAMPAIO, A. C. A. ; MEIRA, S. . De Mooz Para Eiffel. In: XXI CONGRESSO DA SBC, 1994. (SBC'94). Caxambu/MG. p. 379-393.
CORDEIRO, V. ; SAMPAIO, A. C. A. ; MEIRA, S. . Um Estudo de Caso Real Em Refinamento de Especificações Formais Orientadas A Objetos. In: VIII SIMPÓSIO BRASILEIRO DE ENGENHARIA DE SOFTWARE, 1994. UM ESTUDO DE CASO REAL EM REFINAMENTO DE ESPECIFICAÇÕES FORMAIS ORIENTADAS A OBJETOS. CURITIBA/PR. p. 143-158.
BARROS, E. ; LIMA, M. ; SAMPAIO, A. C. A. . From Hardware/Software Partitioning To Layout Synthesis: A Transformation Approach. In: VIII SIMPÓSIO BRASILEIRO DE CONCEPÇÃO DE CIRCUITOS INTEGRADOS, 1994. (SBCCI'94). Gramado/RS. p. 089-100.
SAMPAIO, A. C. A. ; MEIRA, S. . Modular Extensions to Z. In: VDM'90: VDM and Z - Formal Methods in Software Development, 1990, Kiel. VDM'90: VDM and Z - Formal Methods in Software Development, 1990. v. 428. p. 211-232.
SAMPAIO, A. C. A. ; Paulo Cunha . Uma Análise de Adequação e Validação de Primitivas de Comunicação entre Processos. In: SBRC - Simpósio Brasileiro de Redes de Computadores, 1988, Belo Horizonte. VI SBRC - Simpósio Brasileiro de Redes de Computadores. Porto Alegre: SBC, 1988. v. 6.
SAMPAIO, A. C. A. ; MEIRA, S. . Especificação em Z de um Interpretador para uma Linguagem Simples. In: XV SEMISH - Congresso da SBC, 1988, Rio de Janeiro. XV SEMISH - Congresso da SBC. Porto Alegre: SBC, 1988. v. 15. p. 201-213.
SAMPAIO, A. C. A. ; MEIRA, S. . Zc : Uma Notação para Especificação de Sistemas Complexos. In: XV SEMISH - Congresso da SBC, 1988, Rio de Janeiro. XV SEMISH - Congresso da SBC. Porto Alegre: SBC, 1988. v. 15. p. 188-200.
Max Albuquerque ; Hermano Moura ; SAMPAIO, A. C. A. ; MEIRA, S. . GEMS - Um Gerenciador de Módulos de Software. In: II SBES - Simpósio Brasileiro de Engenharia de Software, 1988, Canela. II SBES - Simpósio Brasileiro de Engenharia de Software. Porto Alegre: SBC, 1988. v. 2. p. 61-74.
SAMPAIO, A. C. A. ; MEIRA, S. . Especificação Funcional de um Interpretador. In: ERMAC - SBMAC, 1987, Fortaleza. IV ERMAC - SMBAC, 1987.
Gustavo Carvalho ; Tarciana Dias ; Alexandre Cabral Mota ; Sampaio, Augusto C. A. . Analytical Comparison of Refinement Checkers.. In: 14th Brazilian Symposium on Formal Methods, Short Papers Proceedings, 2011, são Paulo. 14th Brazilian Symposium on Formal Methods, Short Papers Proceedings, 2011. p. 61-66.
Augusto Sampaio . Modelling, Simulation and Verification of Robotic Systems. 2019. (Apresentação de Trabalho/Conferência ou palestra).
Augusto Sampaio . The NAT2TEST Strategy. 2019. (Apresentação de Trabalho/Conferência ou palestra).
Augusto Sampaio . Testing from natural language in an industrial context. 2016. (Apresentação de Trabalho/Conferência ou palestra).
Augusto Sampaio . Refinement Algebra and Applications. 2015. (Apresentação de Trabalho/Conferência ou palestra).
Augusto Sampaio ; Giovanny Lucero ; David Naumann . Refinement Algebra for an O-O Language with References. 2015. (Apresentação de Trabalho/Conferência ou palestra).
Augusto Sampaio . Compositional Analysis for Systems of Systems. 2013. (Apresentação de Trabalho/Conferência ou palestra).
Sampaio, Augusto C. A. . Invited Speaker (Workshop COMPASS): The object-oriented formalism OhCircus. 2012. (Apresentação de Trabalho/Conferência ou palestra).
SAMPAIO, A. C. A. . Keynote speaker ICFEM-2009: Compositional Verification of Input-Output Conformance via CSP Refinement Checking. 2009. (Apresentação de Trabalho/Conferência ou palestra).
Sampaio, Augusto C. A. . Palestrante convidado (Workshop de Métodos Formais na Embraer): An Introduction to the model-based language Z. 2009. (Apresentação de Trabalho/Conferência ou palestra).
SAMPAIO, A. C. A. . Participação no Painel (SBMF-2008): Formal Methods in Industry. 2008. (Apresentação de Trabalho/Conferência ou palestra).
Sampaio, Augusto C. A. . Invited Speaker (Workshop Brasil-India): From Requirements to Test Cases Through (hidden) Test Models. 2008. (Apresentação de Trabalho/Conferência ou palestra).
SAMPAIO, A. C. A. . Invited speaker (IFIP WG2.3): Test sequence generation from process algebra use models. 2006. (Apresentação de Trabalho/Conferência ou palestra).
SAMPAIO, A. C. A. ; Ana Melo ; P. Machado ; Daltro Nunes ; Arnaldo Moura . Participação no Painel (SBMF-2006): Educação em Métodos Formais. 2006. (Apresentação de Trabalho/Conferência ou palestra).
SAMPAIO, A. C. A. . Invited speaker (IFIP WG2.3): Laws of Object-Oriented Programming. 2005. (Apresentação de Trabalho/Conferência ou palestra).
SAMPAIO, A. C. A. ; MOTA, A. ; Rodrigo Ramos . Palestra convidada (WMF-2003): Class and Capsule Refinement in UML for Real Time. Palestrante Convidado. 2003. (Apresentação de Trabalho/Conferência ou palestra).
SAMPAIO, A. C. A. . Invited speaker (Columbia University): An Algebraic Approach to Compiler Design. 1996. (Apresentação de Trabalho/Conferência ou palestra).
Sampaio, Augusto C. A. . Concurrency in CSP. 2011. (Curso de curta duração ministrado/Outra).
Sampaio, Augusto C. A. . Conceitos e Paradigmas de Programação via Projeto de Interpretadores. 2008. (Curso de curta duração ministrado/Outra).
SAMPAIO, A. C. A. . Transformation Laws for Sequential Object-Oriented Programming. 2006. (Curso de curta duração ministrado/Especialização).
CAVALCANTI, A. ; SAMPAIO, A. C. A. ; WOODCOCK, J. . Refinement Techniques in Software Engineering. 2006. (Editoração/Livro).
SAMPAIO, A. C. A. . Simpósio Brasileiro de Métodos Formais (SBMF) 2005. 2005. (Editoração/Anais).
SAMPAIO, A. C. A. ; P. Borba . Transformation Laws for Sequential Object-Oriented Programming. 2004. (Curso de curta duração ministrado/Especialização).
SAMPAIO, A. C. A. . Programming language concepts and paradigms. 2001. (Curso de curta duração ministrado/Especialização).
SAMPAIO, A. C. A. . Object-oriented analysis and design. 2001. (Curso de curta duração ministrado/Especialização).
SAMPAIO, A. C. A. . Simpósio Brasileiro de Métodos Formais (SBES) 2000. 2000. (Editoração/Anais).

Projetos de pesquisa

2022 - Atual

Síntese e verificação de simulação de sistemas robóticos, Descrição: Trata-se do Projeto PQ 1A do pesquisador. O contexto geral deste projeto é o desenvolvimento rigoroso de sistemas robóticos. A ênfase é na síntese automática de simulações para estes sistemas, bem como na verificação de propriedades clássicas (e de domínio específico). A entrada para a geração da simulação é um modelo abstrato de projeto de um sistema robótico em uma notação baseada em máquinas de estados, denominada RoboChart, que possui uma semântica formal definida na álgebra de processos CSP (Communicating Sequential Processes). O produto da síntese é um modelo em uma linguagem, RoboSim, também diagramática e baseada em máquinas de estados. Além disso, RoboSim é agnóstica a tecnologias de implementação de simulação. RoboSim, já projetada como fruto de trabalhos anteriores, também tem uma semântica formal definida em CSP. Isso permite provar que a síntese de RoboChart em RoboSim preserva uma noção de conformidade, garantindo que a simulação gerada não viola o comportamento do modelo mais abstrato em RoboChart. Além da síntese em RoboSim, o projeto aqui proposto explora a efetiva implementação de simulações em diversas plataformas, como Arduino, Simulink/Stateflow e UPPAAL. O objetivo de uma implementação em Arduino é validar a abordagem em um contexto real, considerando os aspectos físicos do ambiente no qual o sistema robótico estará inserido. A tradução para Simulink/Stateflow permite animar o modelo, exercitando estados e transições do Stateflow. É possível, também, verificar se \emph{traces} de execuções do Stateflow são consistentes com os \emph{traces} permitidos pelo modelo RoboSim. A tradução para UPPALL permite verificar propriedades de forma bastante eficiente. Apesar de ser possível verificar propriedades da simulação abstrata em RoboSim, usando, por exemplo, a ferramenta FDR, que é um verificador de moldelos para CSP, em geral a análise em FDR é muito suscetível à explosão de estados. A tradução para UPAALL oferece uma alternativa que permite verificações mais eficientes para modelos complexos. Além disso, é possível realizar algumas análises estocásticas em UPPALL, por exemplo, envolvendo um modelo do ambiente físico do sistema robótico, o que não é possível na versão clássica de CSP. Vários estudos de caso serão desenvolvidos para validar a estratégia de simulação apresentada. Alguns exemplos são: robô para colher maçãs, segway, e um drone, com navegação autônoma, para coletar caramujos (em áreas rurais remotas, de difícil acesso para agentes de saúde) que sejam potenciais hospedeiros do Schistosoma mansoni.. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (2) / Mestrado acadêmico: (2) / Doutorado: (3) . , Integrantes: Augusto Cezar Alves Sampaio - Coordenador., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro.
2021 - Atual

Residência em Robótica e Inteligência Artificial Aplicadas a Testes, Projeto certificado pelo(a) coordenador(a) Alexandre Cabral Mota em 17/06/2022., Descrição: O projeto do Curso de Pós-Graduação Lato Sensu (Especialização) de Residência em Robótica e Inteligência Artificial Aplicadas a Testes de Software envolve três dimensões complementares e paralelas: (i) Capacitação; (ii) Inovação e Pesquisa; e (iii) Automação e Execução de Testes de Software. O projeto segue a filosofia de uma residência tecnológica (inspirada nas residências médicas). Existem dois ambientes para execução do projeto: a sala de aula e o laboratório. Os alunos têm dedicação exclusiva e, em meio turno, dedicam-se a assistir às aulas (i). No outro turno, realizam no laboratório atividades práticas de Inovação e Pesquisa (ii) e Automação e Execução de Testes de Software (iii). O curso capacita (na teoria e prática) os alunos em programação de braços robóticos e técnicas de inteligência artificial aplicadas a teste de software. Braços robóticos (adquiridos prontos no mercado  este projeto não engloba construção de robôs) são reprogramados para realizar testes de interface, que envolvem tanto interface gráfica como gestual (toques na tela, rotações e translações em dispositivos). Testes assim são usualmente executados por humanos. Inteligência artificial suporta a descoberta de defeitos de forma sistemática e preditiva. Tal modelo de residência provê ao aluno tanto capacitação teórica em sala de aula (pela manhã) quanto experiência de trabalho em atividades práticas de automação e execução de teste de software (pela tarde). Desafios de inovação e pesquisa na área de robótica e inteligência artificial aplicadas a teste de software são solucionados tanto pela equipe fixa do projeto (líder técnico e engenheiros) quanto pelos alunos em suas monografias. E, em adição às duas primeiras dimensões, as atividades práticas de automação e execução de teste de software utilizando robôs e técnicas de inteligência artificial completam a formação teórica dos alunos. Tal ambiente prático tem dois papéis: é onde os alunos ficam imersos durante um turno do dia vivenciando experiências de trabalho, e é o celeiro que tanto gera desafios de inovação e pesquisa quanto serve como laboratório onde tais soluções são testadas. Estas três dimensões constituem um ambiente integrado de atividades simultâneas de capacitação teórica e prática, inovação, pesquisa e desenvolvimento. III -. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (4) / Especialização: (20) . , Integrantes: Augusto Cezar Alves Sampaio - Integrante / A. MOTA - Coordenador.
2020 - Atual

Formal analysis of blockchain components, Descrição: This project investigates different applications of formal analysis in the context of blockchain systems. The prime example is (and the focus of the project will be) the formal analysis of smart contracts to ensure that they behave as intended by the developer. The methods and technologies developed in the project have the potential to propel the adoption of blockchain systems. The Project is a cooperation between CIn-UFPE, in Brazil, and TBTL, in Oxford-UK.. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Mestrado acadêmico: (1) Doutorado: (1) . , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / Bruno Oliveira - Integrante / Pedro Antonino - Integrante / ROSCOE, A. W. - Integrante / Juliandson Ferreira - Integrante.
2020 - Atual

Model Transformation from RoboSim to Network of Timed Automata for UPPAAL, Descrição: We propose a model transformation method based on TA patterns and mapping rules, and develop a real-time automatic transformation tool from RoboSim model to NTA model for UPPAAL. This work was successfully applied to the real case Alpha algorithm. The next steps are: 1. Automatic generation of properties for robots. 2. Propose a new DSML for modeling specific environment.. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Mestrado acadêmico: (2) . , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / Madiel Conserva - Integrante / Dehui du - Integrante / Mingzhuo Zhang - Integrante / Menghan Zhang - Integrante / Ana Cavalcanti - Integrante.
2017 - Atual

RoboTIC@ - Information and Communication Technology for Robotics and Applications, Descrição: The main objective of this project is to create a systematic and rigorous methodology to specify, verify, design and implement robotic applications. It is one of the projects of INES (https://ines.org.br/) and is part of the RoboStar initiative (https://www.cs.york.ac.uk/RoboStar/). The focus is on the design of a graphical simulation language, RoboSim, and mapping models in RoboSim to several target platforms: Arduino, B and Simulink/Stateflow, among others. Development of the final implementations from the simulations is also in scope. Finally, we will also consider probabilistic models, modelling of the environment and the development of real world applications.. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (3) / Mestrado acadêmico: (4) / Doutorado: (4) . , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / A. CAVALCANTI - Integrante / J. WOODCOCK - Integrante / Alexandre Cabral Mota - Integrante / Sidney Nogueira - Integrante / Iyoda, Juliano - Integrante / Marcel Oliveira - Integrante / CORNÉLIO, MÁRCIO - Integrante / Madiel Conserva - Integrante / Jones Albuquerque - Integrante / Thierry Lecomte - Integrante.
2017 - Atual

Um Framework Baseado em Modelos para Análise e Teste Composicionais de Sistemas Reativos, Descrição: Este projeto propõe um framework integrado para análise (via verificação de modelos) e teste de sistemas reativos. A estratégia, baseada em MDE - Model Driven Engineering (Engenharia Dirigida a Modelos), é composicional, no sentido de que a análise e o teste de sistemas complexos reutilizam verificações e testes de componentes destes sistemas; composicionalidade é explorada aqui como uma importante ferramenta para permitir escalabilidade, que constitui um dos principais desafios das estratégias de verificação formal. Como entrada para a estratégia de análise e testes, utilizamos tanto uma Linguagem Natural Controlada (CNL, Controlled Natural Language) como a linguagem SysML. A CNL é um subconjunto de Inglês como uma gramática bem definida, o que permite que textos escritos na mesma sejam passíveis de processamento computacional. SysML é uma linguagem semiformal cuja semântica é definida em linguagem natural e através do uso de meta-modelos, também semiformais. O framework proposto integra e estende, significativamente, duas ações de pesquisa em andamento. Uma é a ferramenta NAT2TEST, que gera testes a partir de requisitos temporais, descritos em CNL, de sistemas reativos. A outra é uma estratégia de análise de propriedades de sistemas modelados em SysML. A integração envolve as seguintes contribuições: (i) definição de uma noção de componentes para modelos SysML, que será a base para permitir tanto análise quanto teste composicional; (ii) regras de composição de componentes SysML de forma que propriedades clássicas (como ausência de deadlock, livelock e não determinismo) sejam preservadas por construção; (iii) tradução de componentes SysML para CML (Compass Modelling Language), permitindo o reuso de uma estratégia de análise desenvolvida anteriormente, só que agora explorando aspectos de composicionalidade; (iv) tradução de componentes SysML para o modelo de componentes CoCo, o que permitirá o uso de um framework de verificação que está sendo desenvolvido na Universidade de Oxford, uma parceira acadêmica neste projeto; (v) realização de experimentos para analisar as vantagens comparativas das abordagens descritas em (iii) e (iv); (vi) tradução de modelos SysML (particularmente de diagramas de estados) para Data Flow Reactive Systems (DFRS, uma representação interna usada na NAT2TEST), de forma a permitir a efetiva integração entre a estratégia de análise e a de testes; (vii) extensão da estratégia de geração na NAT2TEST para gerar testes composicionais (reutilizando testes de componentes já testados quando estes são integrados em sistemas mais complexos); (viii) validação prática do framework, com foco em escalabilidade, em aplicações na área de aviação, em parceria com a Embraer, uma parceira industrial neste projeto.. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Mestrado acadêmico: (2) Doutorado: (2) . , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / Alexandre Cabral Mota - Integrante / Sidney Nogueira - Integrante / Flávia Falcão - Integrante / Lucas Lima - Integrante / Iyoda, Juliano - Integrante / Gustavo Carvalho - Integrante / Tarciana Dias - Integrante / Malcel Oliveira - Integrante / CORNÉLIO, MÁRCIO - Integrante / Hugo Araujo - Integrante / Filipe Arruda - Integrante.
2016 - 2019

Reducing Cost of Software: A Scalable Model-Based Verification Framework, Descrição: In many manufacturing industries, the escalating cost of software development is widely recognised as a serious challenge and is becoming a significant barrier to innovation [9]. Formal verification provides a potential solution to this, however, there are presently no scalable verification methods that can handle embedded software designed in open model-driven engineering (MDE) languages, such as SysML and UML. This project will develop a scalable model-based verification framework that will allow MDE languages to be verified within an industrial context. The core research questions are: 1. How can the semantics of MDE languages be specified in a way that allows a formal semantics to be defined for heterogeneous systems that are modelled in several tools (as most industrial systems are)? 2. How can MDE languages be verified using compositional, and thus industrially scalable, formal verification technologies? 3. How can MDE languages be translated into provably equivalent source code? At the core of the proposed framework is a new formal language that we will develop, called Communicating Components (CoCo). Standard MDE languages such as SysML and UML will be translated into CoCo, and we will develop a scalable verification strategy based on FDR. We will also investigate how theorem proving can allow us to create provably correct source code generators.. , Situação: Concluído; Natureza: Pesquisa. , Integrantes: Augusto Cezar Alves Sampaio - Integrante / A. W. Roscoe - Coordenador / Philippa Hopcroft - Integrante / Guy Broadfoot - Integrante.
2016 - Atual

INCT para Engenharia de Software (INES), Descrição: O objetivo geral deste Instituto é desenvolver técnicas, ferramentas e processos de engenharia de software que sirvam de base para aplicações avançadas, como por exemplo a plataforma aberta de serviços voltada para Cidades Inteligentes descrita no programa de pesquisa da Seção 3. Esperamos avanços em técnicas como Linhas de Produtos de Software (LPS), especificação e testes de sistemas distribuídos, e engenharia de software experimental, entre outras, explorando também a integração entre as técnicas, coordenando os esforços e competências das diversas instituições e pesquisadores envolvidos. Desta forma, esperamos que as técnicas e ferramentas propostas forneçam vantagens competitivas às empresas que as adotem, tanto melhorando a confiabilidade, como a produtividade no desenvolvimento de aplicações para cidades inteligentes. Os objetivos específicos do Instituto: * Desenvolver pesquisa científica de vanguarda com padrão internacional na área de Engenharia de Software, com foco em Cidades Inteligentes * Formar recursos humanos qualificados na área de Engenharia de Software * Difundir conhecimento para a sociedade * Difundir conhecimento para o setor empresarial *. , Situação: Em andamento; Natureza: Pesquisa. , Integrantes: Augusto Cezar Alves Sampaio - Coordenador.
2015 - Atual

Validação de Software e Automação de Testes, Descrição: Trata-se de uma cooperação de P&D em parceria com a Motorola Mobility, incluindo os seguintes subprojetos principais: Automação de Testes Tem como objetivo concepção de estratégias inovadoras de geração automática de testes, o desenvolvimento de casos de testes, a automação de testes funcionais automáticos e implementação e operacionalização dos laboratórios para testes de estabilidade e desempenho. Técnicas de geração de testes a partir de texto em linguage, natural, bem como automação baseada em captura e resuso são importantes objetivos deste subprojeto. Validação de Software Responsável pela criação de estratégias de testes, estratégias inovadoras de seleção dos tipos de testes a serem aplicados, planejamento da execução de tais ciclos de testes, execução propriamente dita, registro dos defeitos identificados e, por fim, acompanhamento junto aos times de desenvolvimento de software da correção e re-validação das correções ora efetuadas. Localização O objetivo é recriar a experiência de usuário final do produto na sua língua nativa. Durante o processo de internacionalização é necessária a adaptação (além da tradução) do software, a fim de aderir aos requisitos regionais / locais, considerando formatos de data e hora, bem como exigências linguísticas, como regras gramaticais, gênero, número, entre outros usos gerais consistentes da terminologia local. É preciso também externar todos os elementos da interface do software visíveis para o usúario para que eles realmente possam ser localizados (traduzidos). Um dos objetivos centrais aqui é a criação de estratégias automatizadas de suporte à localização. CV Lab O laboratório de Carrier Validation, CV Lab, tem como objetivo garantir que os produtos desenvolvidos pela Motorola atendam aos requisitos estabelecidos pelas operadoras de telefonia celular. Usando os equipamentos do CV Lab é possível simular as mais diversas redes, em diferentes configurações, permitindo validar o funcionamento dos smartphones de acordo com as características das funcionalidades ofertadas pelas operadoras. Há vários desafios de pesquisa envolvendo processamento de imagens, otimização e estratégias de testes, entre outros. ADR Lab O laboratório de Advanced Digital Radio, ADR Lab, tem como objetivo garantir que os produtos desenvolvidos pela Motorola atendam aos requisitos estabelecidos pelas normas e padrões de conformidade das redes móveis, nas diversas tecnologias de rede, como UMTS e LTE. Usando os equipamentos do ADR Lab é possível simular as mais diversas redes, em diferentes configurações, permitindo validar o funcionamento dos smartphones em diferentes condições de operação. Como no caso do laboratório acima descrito, há vários desafios de pesquisa envolvendo processamento otimização, data analytics, processamento de imagens, entre outros.. , Situação: Em andamento; Natureza: Pesquisa. , Integrantes: Augusto Cezar Alves Sampaio - Coordenador.
2013 - 2018

Modelagem, Verificação e Teste Composicional de Sistemas com Aplicações na Indústria Aeronáutica, Descrição: Neste projeto, propomos a sistematização de vários aspectos do projeto de grandes sistemas, particularmente, com ênfase em Sistemas de Sistemas (SoS, Systems of Sytems). O escopo inclui modelagem (semiformal e formal), verificação (análise formal de propriedades) e teste de tais sistemas. Utilizamos a linguagem SysML para descrever requisitos e os modelos de análise e projeto (design) de um SoS. SysML é uma linguagem semiformal, amplamente utilizada na indústria, com uma semântica definida em linguagem natural e através do uso de meta-modelos, também semiformais. Portanto, ambiguidades nos modelos SysML podem induzir a erros de implementação. No processo proposto, o modelo em SysML é traduzido (automaticamente) para um modelo descrito na linguagem formal Circus, que integra a álgebra de processos CSP, para expressar os aspectos reativos, a linguagem baseada em modelos Z, para expressar os aspectos de dados e a linguagem de comandos guardados de Dijkstra, fazendo de Circus não apenas uma linguagem de especificação, mas também de programação. Como segunda etapa do processo proposto, o modelo Circus será verificado com o objetivo de se garantir a preservação de propriedades de interesse. Isto permitirá, inicialmente, verificar a consistência, tanto individual, como integrada, dos diagramas SysML do sistema. Um outro aspecto da análise é o desenvolvimento de uma estratégia que garanta, por construção, a ausência de problemas clássicos como deadlock no SoS, a partir da verificação da ausência de deadlock em seus componentes. O desafio desta análise é escalabilidade. Como terceira e última etapa do processo, complementar à verificação, será desenvolvida uma estratégia automática de geração de vetores de teste a partir da especificação em Circus. Finalmente, o escopo do projeto inclui uma avaliação, em um ambiente industrial, com o apoio da Embraer, da eficácia dos métodos de modelagem, análise e teste propostos, através da aplicação na área de aviação e na arquitetura IMA (Integrated Modular Avionics) em particular. Este projeto inclui um breve relato das metas atingidas no período anterior. Alguns resultados, restritos a aspectos de controle em CSP e testados em exemplos pequenos, serão estendidos para um formalismo multiparadigma (Circus) e validados em aplicações reais de IMA.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Mestrado acadêmico: (1) Doutorado: (3) . , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / Marcio Cornelio - Integrante / Lucas Lima - Integrante / Iyoda, Juliano - Integrante / Gustavo Carvalho - Integrante / Marcel Oliveira - Integrante / José Oliveira - Integrante / Pedro Antonino - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Bolsa.
2012 - 2015

Modelagem e Análise Composicional de Sistemas de Sistemas com Aplicações na Indústria Aeronáutica, Descrição: Propomos um processo para modelagem e análise formal de propriedades de Sistemas de Sistemas (SoS, Systems of Sytems), com ênfase em aplicações na área de aviação e na arquitetura IMA (Integrated Modular Avionics) em particular. Utilizamos a linguagem SysML para descrever requisitos e os modelos de análise e projeto (design) de um SoS. SysML é uma linguagem semiformal cuja semântica é definida em linguagem natural e através do uso de meta-modelos, também semiformais. Por um lado, uma notação semiformal (e gráfica) conquista uma adoção ampla e rápida pela indústria devido a sua simplicidade e facilidade de aprendizado. Por outro lado, ambiguidades nos modelos podem induzir a erros de implementação. Por sua vez, usualmente há resistência, no ambiente industrial, com relação à adoção de uma notação formal, mesmo com a promessa de especificações formais serem livres de ambiguidades e poderem ser analisadas de forma rigorosa com auxílio de ferramentas. No processo proposto, o modelo em SysML é traduzido (automaticamente) para um modelo descrito na linguagem formal Circus, que integra a álgebra de processos CSP, para expressar os aspectos reativos, a linguagem baseada em modelos Z, para expressar os aspectos de dados e a linguagem de comandos guardados de Dijkstra, fazendo de Circus não apenas uma linguagem de especificação, mas também de programação. Desta forma, esperamos produzir uma solução em que a notação gráfica continua disponível, porém com os benefícios adicionais oferecidos pela notação formal Circus. Como segunda etapa do processo proposto, o modelo Circus será analisado com o objetivo de se garantir a preservação de propriedades de interesse. Isto permitirá, inicialmente, verificar a consistência, tanto individual, como integrada, dos diagramas SysML do sistema. Um outro aspecto da análise é o desenvolvimento de uma estratégia que garanta, por construção, a ausência de deadlock no SoS, a partir da verificação da ausência de deadlock em seus componentes. O desafio desta análise é escalabilidade. Finalmente, o escopo do projeto inclui uma avaliação, em um ambiente industrial, com o apoio da Embraer, da eficácia dos métodos de modelagem e análise propostos, através da aplicação da abordagem proposta em um estudo de caso real relacionado a sistemas IMA.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Mestrado acadêmico: (1) Doutorado: (4) . , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / Marcio Cornelio - Integrante / Alexandre Cabral Mota - Integrante / Sidney Nogueira - Integrante / Cavalcanti, Ana - Integrante / Lucas Lima - Integrante / Iyoda, Juliano - Integrante / Joabe Jesus - Integrante / Gustavo Carvalho - Integrante / Marcel Oliveira - Integrante / José Oliveira - Integrante / Pedro Antonino - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro.
2011 - 2014

COMPASS - Comprehensive Modelling for Advanced Systems of Systems, Descrição: COMPASS will augment existing industry tools and practice with an underlying modelling language in which Systems of Systems (SoS) architectures and contracts can be expressed. A formal semantic foundation ? the first to be developed specifically for SoS engineering ? will enable this language to support analysis of global SoS properties. The language and methods will be supported by an open, extendible tools platform with integrated prototype plug-ins for model construction, dynamic analysis by simulation and test automation, static analysis by model-checking and proof, and links to an established architectural modelling language (SysML). These strengthened foundations and tools will support enhanced methods guidelines that help users embed this new technology in industrial SoS practice. Technical advances in COMPASS are focussed on industry needs evaluated through substantial industry-led case studies in three diverse and complementary areas. These will be augmented by challenge problems solicited from a range of SoS stakeholders and developer organisations through a special interest group. The open platform, tools plug-ins, semantics, development guidelines, industry case study experience and challenge problems will ensure that COMPASS‟s outputs can be readily exploited by SoS developers and stakeholders as well as in future research and development.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) / Mestrado acadêmico: (2) / Doutorado: (2) . , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / Marcio Cornelio - Integrante / Alexandre Cabral Mota - Integrante / Cavalcanti, Ana - Integrante / Lucas Lima - Integrante / WOODCOCK, J - Integrante / Iyoda, Juliano - Integrante / Gustavo Carvalho - Integrante / Cristiano Bertolini - Integrante / André Didier - Integrante., Financiador(es): Comunidade Européia - Auxílio financeiro.
2010 - 2014

Confiabilidade e Segurança em Software Crítico Embarcado, Descrição: Sistemas Embarcados têm se tornado cada vez mais comuns no suporte à execução de atividades críticas, tais como controle, monitoração e tomada de decisões, onde falhas podem resultar em perdas ou injúrias a pessoas, ao meio ambiente ou a negocios. Tais sistemas se enquadram no quinto grande desafio da SBC que tem como enfoque o desenvolvimento tecnológico de qualidade de sistemas. O objetivo deste projeto é prover fundamentação teórica e tecnologia para o desenvolvimento de software crítico embarcado, correto e seguro, com base na aplicação de técnicas de modelagem formal, transformação, geração automática, vericação de modelos e validação através de teste de software. Serão considerados aspectos e conceitos tais como abstração, tradução de linguagens, independência de plataforma, verificação de propriedades temporais e análise probabilística. As soluções serão aplicadas, prioritariamente, ao domínio aeronáutico, através de cooperação com a empresa Embraer, e de material de transporte metro-ferroviário, através de uma colaboração com a empresa AeS.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (2) / Mestrado acadêmico: (2) / Doutorado: (2) . , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / Paulo Borba - Integrante / David Deharbe - Integrante / Patrícia Machado - Integrante / Alexandre Cabral Mota - Integrante / Iyoda, Juliano - Integrante / Gustavo Carvalho - Integrante / Marcel Oliveira - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro.
2010 - 2012

Refatoração sincronizada de programas anotados com especificações formais, Descrição: A assimilação de evolução em projetos de software que fazem uso de especificação e modelagem ainda é difícil e custosa na prática. No caso de refatoração de programas, por exemplo, modelos abstratos em conformidade com os programas tornam-se inconsistentes; técnicas como engenharia round-trip e MDA (Model-Driven Architecture) lidam parcialmente com o problema, já que estabelecem perda da abstração desejável em especicações. Este projeto tem como objetivo propor, formalizar, implementar e avaliar uma abordagem prática de refatoração de especicações que geram refatorações automáticas de programas, mantendo sua conformidade. Especicações e código-fonte serão localizados em um único artefato, utilizando Java e a linguagem de especicação JML (Java Modeling Language), facilitando sua adoção da abordagem. Como complemento, iremos definir um catálogo de refatorações de programas que permanecem corretos mesmo com especicações JML presentes, formando assim uma metodologia de refatoração completa.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) / Mestrado acadêmico: (2) / Doutorado: (2) . , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / Paulo Borba - Integrante / T. Massoni - Integrante / Marcio Cornelio - Integrante / Rohit Gheyi - Integrante / Silva, Leila - Integrante / Naumann, David A. - Integrante / Gary Leavens - Integrante.
2007 - 2010

Combinando Técnicas de Métodos Formais e Teste na Construção de Sistemas Embarcados de Tempo Real, Descrição: Este projeto tem como enfoque o uso combinado de métodos formais e técnicas de teste baseado em modelos para sistemas embarcados de tempo real. O principal objetivo é compartilhar conhecimentos e experiências para promover avanços conjuntos nesta área de pesquisa. Em particular, procuramos com este projeto promover o desenvolvimento tecnológico de qualidade de sistemas corretos e seguros. O projeto considera as seguintes direções de pesquisa: (1) investigação de modelos de sistemas de software heterogêneos com características tais como não-determinismo, tempo e interrupção; (2) desenvolvimento de padrões de modelagem para sistemas embarcados utilizando formalismos baseados em estados e processos; (3) proposta de padrões de desenvolvimento baseado em refinamento de modelos baseados em estados e processos; (4) geração automática de código para hardware e software; (5) testes a partir de modelos parciais, considerando sua geração a partir de casos de teste abstratos e comportamento observável; (6) aprimoramento de técnicas atuais para a geração de casos de teste considerando critérios semânticos de cobertura além dos critérios de cobertura estrutural, bem como relações de conformidade pertinentes e critérios de cobertura de verificação de modelos; (7) investigação das relações de conformidade com base em falha e divergência em álgebras de processo; (8) proposta de estratégias para a seleção automática de casos de teste com base em funções de similaridade.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (2) / Mestrado acadêmico: (2) / Doutorado: (2) . , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / Paulo Borba - Integrante / Patrícia Machado - Integrante / Alexandre Cabral Mota - Integrante / CORNELIO, M - Integrante / Iyoda, Juliano - Integrante / Joabe Jesus - Integrante / Gustavo Carvalho - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro.
2005 - 2008

FORMULA - Formal Methods and UML-RT Integration (Edital Universal), Descrição: O objetivo geral deste projeto é integrar métodos semi-formais, usados para especificação e modelagem, e que possuem grande apelo prático, com métodos formais, que oferecem uma base matemática sólida complementar. Em particular, a notação gráfica UML (e sua extensão para tempo real, UML-RT) será uma linguagem de referência para o projeto, devido a sua ampla aceitação prática. A integração de UML-RT com métodos formais visa contribuir com um processo de desenvolvimento de software que permita a geração de artefatos (documentos) com semântica bem definida, ou seja, não-ambíguos, consistentes e precisos. Por outro lado, a integração visa difundir o uso de métodos formais na Indústria, encapsulando-os através dos diagramas de UML. Um dos requisitos centrais do processo integrado é flexibilidade: o desenvolvedor pode optar pelo grau de formalismo usado em seu projeto, podendo variar desde uma descrição puramente em UML até uma especificação completamente formal, para descrever tanto os aspectos estáticos quanto os dinâmicos da modelagem. O passo inicial do projeto proposto é a definição de uma linguagem de especificação formal capaz de capturar todos os elementos conceituais disponíveis em UML-RT, pois, do nosso conhecimento, não há, na literatura, um formalismo que integre objetos, concorrência e tempo real (elementos de UML-RT). Entretanto, ao invés de criar uma tal linguagem por completo, o objetivo é, novamente, utilizar princípios de integração de teorias e ferramentas, com o propósito de definir uma linguagem de especificação formal através da combinação de outras já bem definidas e com comprovada aceitação pela Comunidade Científica.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) / Mestrado acadêmico: (3) / Doutorado: (1) . , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / A. MOTA - Integrante / Rodrigo Ramos - Integrante / Manoel Messias - Integrante / Patrícia Ferreira - Integrante / Carlos Andrade - Integrante., Financiador(es): Universidade Federal de Pernambuco - Cooperação / Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro., Número de produções C, T & A: 6
2005 - 2008

Testes de aplicações para disseminação, capacitação e manutenção de dispositivios celulares (CT-INFO), Descrição: O objetivo central desta proposta é investigar e propor processos e ferramentas para o teste de aplicações voltadas a disseminação e manipulação da informação em dispositivos celulares, com elevado padrão de qualidade, tornando as atividades de teste mais efetivas, com conseqüente aumento de produtividade e redução de custos. Os objetivos mais específicos são: 1. Definição de um padrão para a documentação sistemática de requisitos que possa servir como base para a geração de casos de teste; 2. Geração automática de casos de teste de unidade e de integração; 3. Seleção de pontos de teste para cada caso de teste; 4. Suporte à construção/geração automática de código de teste; 5. Análise de cobertura de casos de teste e resultados de sua execução; 6. Desenvolvimento de processos para aplicação integrada das soluções propostas. Neste contexto, teste de unidade tem como escopo serviços atômicos (features) disponibilizados nas aplicações, enquanto que o teste de integração está relacionado às interações entre estes serviços. Ao final do projeto, deverá ser apresentado um conjunto integrado de notações, processos e ferramentas de suporte ao teste de aplicações-chave de tecnologia da informação para dispositivos celulares dentro do escopo das metas definidas. Tais resultados serão refletidos na concretização de trabalhos acadêmicos como dissertações de mestrado e teses de doutorado, bem como publicações em eventos e periódicos especializados na área.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (2) / Mestrado acadêmico: (3) / Doutorado: (3) . , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / A. MOTA - Integrante / Paulo Borba - Integrante / Alexandre Vasconcelos - Integrante / Patrícia Machado - Integrante / Flávia Barros - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro / Universidade Federal de Campina Grande - Cooperação.
2004 - 2010

Processo Integrado de Avaliação, Seleção e Geração Automática de Casos de Teste (Projeto de Pesquisa CIn-Motorola), Descrição: No contexto de uma cooperação já existente entre a Motorola do Brasil e o Centro de Informática (CIn) da UFPE , o objetivo mais amplo deste projeto é contribuir com todo o processo de testes da Motorola, incluindo os seguintes objetivos mais específicos. 1. Documentação de requisitos. A documentação é feita usando linguagem natural, o que pode dificultar a geração/seleção efetiva de casos de teste; uma linguagem padronizada (mesmo que expressa na forma de uma linguagem natural) é fundamental para um processo sistematizado de geração/seleção de casos de testes. 2. Seleção de casos de teste. É feita a partir dos documentos de requisitos. Um dos problemas encontrados refere-se a casos de testes redundantes; o problema complementar é a ausência de casos de testes que cubram algumas funcionalidades ou caminhos do código. Outra dificuldade é avaliar a qualidade de um suíte de testes. Finalmente, não existe um procedimento bem definido para seleção de casos de teste, o que poderia tornar possível a identificação efetiva de testes com potencial para revelar erros importantes na aplicação e com cobertura adequada. 3. Requisitos documentados como teste. A documentação de requisitos é, muitas vezes, incompleta e embutida nos testes desenvolvidos, o que torna difícil uma visualização das funcionalidades gerais da aplicação. A geração/atualização de requisitos (já em uma linguagem padronizada) a partir de casos de testes é um outro importante objetivo desta iniciativa. 4. Avaliação de Suíte de Testes e Resultados. Técnicas e ferramentas que permitam analisar parâmetros como cobertura e confiabilidade são primordiais.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (2) / Mestrado acadêmico: (8) / Doutorado: (2) . , Integrantes: Augusto Cezar Alves Sampaio - Integrante / A. MOTA - Integrante / Paulo Borba - Coordenador / Alexandre Vasconcelos - Integrante / Patrícia Machado - Integrante / Flávia Barros - Integrante., Financiador(es): Motorola Industrial LTDA - Cooperação / Ministério da Ciência, Tecnologia e Inovações - Auxílio financeiro., Número de produções C, T & A: 2
2001 - 2005

DARE-COOP - Develoment and Applications of a Refinement Calculus for Object-Oriented Programming, Descrição: O projeto é uma continuação do CO-OP (ver entrada para o projeto CO-OP), concluído em 2001. O objetivo é consolidar um cálculo de refinamentos para linguagens orientadas a objetos no estilo de Java, a partir de trabalhos existentes (o cálculo de Morgan e outros para linguagens imperativas). O cálculo deve incluir regras algébricas básicas para a transformação de programas e regras de mais alto nível que sistematizem a prática usual de projetos orientados a objetos. As regras são provadas a partir de uma semântica (baseada em weakest precondition) pra a linguagem em questão. Alguns estudos de caso foram desenvolvidos e um compilador (baseado em regras de reescrita) para a linguagem foi construído como um exercício de aplicação das regras. Enquanto no projeto CO-OP a ênfase foi em uma linguagem com a semântica de cópia, no DARE-COOP a ênfase é em uma linguagem com semântica de referência, além de incluir construções mais elaboradas como classes abstratas, interfaces e pacotes.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Mestrado acadêmico: (1) Doutorado: (2) . , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / A. CAVALCANTI - Integrante / Paulo Borba - Integrante / Marcio Cornelio - Integrante / Adolfo Duran - Integrante / David Naumann - Integrante., Financiador(es): Stevens Institute of Technology - Cooperação / Universidade Federal de Pernambuco - Cooperação / Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro., Número de produções C, T & A: 2
2001 - 2002

Refinement Calculi for Sequential and Concurrent Programs, Descrição: This proposal is for two Visiting Fellowships, for one month each, to enable Dr Ana Cavalcanti and Dr Augusto Sampaio of the Federal University of Pernambucco (UFPE), Brazil, to work with Prof. Jim Woodcock at the University of Oxford; and for a travel grant to enable Prof. Woodcock to visit UFPE. Drs Cavalcanti and Sampaio are experts in the field of the formal refinement of computer programs from mathematical specifications. Recent collaboration between UFPE and Oxford has resulted in the development of a refinement calculus, in the spirit of Morgan's, specifically for Z notation. This work is now being extended and developed to allow the formal, stepwise refinement of impressive CSP programs. This concurrent refinement calculus is novel, finding its basis in the Unifying Theory of Hoare & He. The new calculus is formed from the semantic combination of Z and CSP: Z is used to give specifications in state-based and behavioural terms; operation schemas are first-class process citizens; refinement laws introduce the combinators of process algebra and the imperative mechanisms. The Principal Investigator and the proposed Visiting Fellows are currently working on a formal semantics that is sufficiently tractable to allow machine proofs of consistency and the derivation of refinement laws.. , Situação: Concluído; Natureza: Pesquisa. , Integrantes: Augusto Cezar Alves Sampaio - Integrante / A. CAVALCANTI - Integrante / J. WOODCOCK - Coordenador., Financiador(es): EPSRC - Auxílio financeiro / University of Oxford - Cooperação., Número de produções C, T & A: 1
1999 - 2001

CO-OP - Calculus of Object-Oriented Programming, Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) / Mestrado acadêmico: (1) / Doutorado: (1) . , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / A. CAVALCANTI - Integrante / Paulo Borba - Integrante / Marcio Cornelio - Integrante / Adolfo Duran - Integrante / David Naumann - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro / Stevens Institute of Technology - Cooperação / Universidade Federal de Pernambuco - Cooperação / The National Science Foundation - Auxílio financeiro., Número de produções C, T & A: 2
1995 - 2012

Álgebra de Refinamentos e Aplicações - Projeto de Produtividade em Pesquisa (PQ), Descrição: O objetivo fundamental do nosso projeto tem sido o desenvolvimento de um formalismo multiparadigma, com ênfase na integração de orientação a objetos, concorrência e aspectos temporais. A integração envolve a definição de sintaxe, semântica formal, noções de refinamento e regras de transformação algébricas. Um requisito importante é que a semântica seja extremamente modular, tanto para permitir a integração dos diversos paradigmas, como para facilitar as provas das regras de transformação. Temos explorado a integração de modelos teóricos de concorrência, especificamente a álgebra de processos CSP, com extensões orientadas a objetos da linguagem Z. A experiência já obtida com o tratamento algébrico de cada paradigma, separadamente, tem servido de base para a investigação de leis algébricas para a integração. Um resultado importante foi a proposta de um formalismo orientado a objetos e concorrente (OhCircus) e a proposição de leis algébricas e noções de refinamento para OhCircus. No contexto do projeto corrente, o escopo envolve a definição de uma semântica baseada na Unifying Theories of Programming (UTP) [HH98], a incorporação de construções temporais e a proposição e prova de regras que relacionem o modelo de processos concorrentes com objetos e tempo real. O projeto de um formalismo multiparadigma é a base para alcançar os demais objetivos deste projeto. Um outro objetivo importante do nosso projeto é a integração de métodos formais com linguagens de modelagem diagramáticas e semi-formais, como UML, particularmente UML-RT e UML2.0. A estratégia tem sido utilizar o formalismo mencionado acima como uma base semântica para UML, de forma que equivalência, refinamento e transformações de construções e diagramas de UML são definidos a partir de noções precisamente definidas no formalismo. Pretendemos definir um mapeamento entre este formalismo e a notação gráfica de UML. A motivação para este mapeamento é promover uma unificação entre uma notação de grande apelo práti. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (8) / Mestrado acadêmico: (12) / Doutorado: (4) . , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / A. MOTA - Integrante / Adnan Sherif - Integrante / Marcio Cornelio - Integrante / Adolfo Duran - Integrante / Adalberto Farias - Integrante / Rodrigo Ramos - Integrante / Walter Mesquita - Integrante / Thiago Santos - Integrante / Manuela Xavier - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro., Número de produções C, T & A: 35
1995 - 1997

Projeto Integrado de Software e Hardware (PISH), Descrição: O principal objetivo do projeto PISH consiste no desenvolvimento de um sistema de CAD que suporte o projeto de sistemas digitais complexos considerando arquiteturas heterogêneas compostas por componentes programáveis de propósito geral (denominados no projeto componentes de software) e componentes de aplicação específica (ou componentes de hardware). Tal objetivo será obtido através do desenvolvimento de seis subprojetos: Particionamento Hardware/Software; Verificacação Formal; Síntese do Hardware/Software; Geração do Protótipo e Implementação. Em todas as etapas será utilizado um exemplo comum, o qual foi definido numa fase inicial do projeto. Dos subprojetos mencionados anteriormente os dois primeiros objetivam o desenvolvimento de um mecanismo para particionamento de uma descrição em partes a serem implementadas diretamente em hardware e partes a serem implementadas por programas sendo executados em microprocessadores de propósito geral, isto é soluções implementadas por software. Além de considerar uma arquitetura mais genérica dos que os métodos em desenvolvimento consideram e ter a capacidade de analisar um espaço mais amplo de alternativas de projetos, os subprojetos em questão visam o desenvolvimento de um método que permita um particionamento correto por construção através do uso de técnicas de verificação formal, tais como transformações algébricas e técnicas de reescritura de termos. As tarefas realizadas dentros destes subprojetos são dadas por: definição de um formato intermediário para o algoritmo de particionamento ; definição de uma arquitetura genérica; incorporação do modelo genérico de arquitetura no algoritmo de particionamento; verificação da corretude do particionamento para CSP/occam; verificação da corretude da síntese de hardware para CSP/occam; verificação mecânica do particionamento para CSP/occam; verificação da corretude do particionamento para LOTOS; tradução LOTOS/occam; e implementação de um protótipo de verificação. Neste p. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (2) / Mestrado acadêmico: (2) / Doutorado: (1) . , Integrantes: Augusto Cezar Alves Sampaio - Integrante / L. SILVA - Integrante / E. BARROS - Coordenador / J. IYODA - Integrante / Ney Calazans - Integrante / Ricardo Jacob - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro / Pontifícia Universidade Católica do Rio Grande do Sul - Cooperação / Universidade Federal do Rio Grande do Sul - Cooperação., Número de produções C, T & A: 8
1994 - 1997

Provably Correct Systems (Keep-in-Touch Activity, funded by the European Comission), Descrição: UNIVERSITIES INVOLVED: Federal University of Pernambuco (Contact: Augusto Sampaio) Oxford University Computing Lab (Contact: Prof. C.A.R. Hoare ) Technical University of Denmark (Contact: Prof. Anders P. Ravn ) Carl von Ossietzky University of Oldenburg (Contact: Prof. Ernst-Rudiger Olderog ) Christian-Albrechts-University of Kiel (Contact: Prof. Hans Langmaack ) OBJECTIVES: The co-operation proposed here is in the context of the ESPRIT Basic Research PROCOS II project (no.7071) on Provably Correct Systems, dedicated to cover the entire development process for critical embedded systems, from the original capture of requirements to the computers and special purpose hardware on which the developed programs run. The emphasis is on a constructive approach to correctness, using proven algebraic transformations between adjacent phases of development: specifications, designs, programs, compilers and hardware. The purpose of this co-operation is to explore the development of embedded systems in such a way that the final implementation may include both software and hardware components. Rather than producing only machine code as the final implementation (as stated in the original objectives of PROCOS I), the aim is to design a partitioning algorithm which, based on some function of cost, determines what should be implemented in software and in hardware. The main concern is not the discovery of an original partitioning algorithm, but rather a correct design of (possibly an existing) one. RESULTS: A partitioning algorithm has been designed as a set of transformation rules which are provably correct from the semantics of the programming language. The result of the partitioning is still a program, but its structure reflects the software and hardware components, and how they interact to achieve the overall goal. We have implemented this strategy by coding the transformations in a term rewriting system. The software components generated by the process are then compil. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (3) / Mestrado acadêmico: (2) / Doutorado: (1) . , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / C. A. R. HOARE - Integrante / L. SILVA - Integrante / J. IYODA - Integrante / Adnan Sherif - Integrante / Ernst-Rudiger Olderog - Integrante / Anders P. Ravn - Integrante / Hans Langmaack - Integrante., Financiador(es): European Commission - Auxílio financeiro / University of Oxford - Cooperação / University of Oldenburgh - Cooperação / University of Kiel - Cooperação / Technical University of Denmark - Cooperação., Número de produções C, T & A: 8

Projetos de desenvolvimento

2002 - Atual

Projeto de Automação de Testes (cooperação de P&D CIn-Motorola), Descrição: Este projeto vem sendo desenvolvido em cooperação com a Motorola. O Projeto de Automação de Testes vem ampliar e referendar o sucesso do Projeto "Curso Seqüencial de Formação Complementar em Análise de Testes". O escopo envolve a melhoraria contínua do processo de especificação, projeto, geração e execução de testes de aplicações móveis, através da sistematização e automatização de procedimentos anteriormeente executados de forma manual. Além da automação de testes funcionais, o desenvolvimento de ferramentas de suporte à configuração de ambiente tem proporcionado uma redução significativa de esforço dos testadores para realização dos testes automáticos e manuais. No caso de testes automáticos, o escopo inclui também a implementação e operacionalização de laboratórios para testes de stress e de performance das aplicações móveis. . , Situação: Em andamento; Natureza: Desenvolvimento. , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / Paulo Borba - Integrante / Sergio Cavalcante - Integrante / Luis Figueiredo - Integrante / Hermano Moura - Integrante., Financiador(es): Ministério da Ciência e Tecnologia - Outra / Motorola Industrial LTDA - Cooperação.
2002 - Atual

Projeto de Automação de Testes (cooperação de P&D CIn-Motorola), Descrição: Este projeto vem sendo desenvolvido em cooperação com a Motorola. O Projeto de Automação de Testes vem ampliar e referendar o sucesso do Projeto "Curso Seqüencial de Formação Complementar em Análise de Testes". O escopo envolve a melhoraria contínua do processo de especificação, projeto, geração e execução de testes de aplicações móveis, através da sistematização e automatização de procedimentos anteriormeente executados de forma manual. Além da automação de testes funcionais, o desenvolvimento de ferramentas de suporte à configuração de ambiente tem proporcionado uma redução significativa de esforço dos testadores para realização dos testes automáticos e manuais. No caso de testes automáticos, o escopo inclui também a implementação e operacionalização de laboratórios para testes de stress e de performance das aplicações móveis. . , Situação: Em andamento; Natureza: Desenvolvimento. , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / Paulo Borba - Integrante / Sergio Cavalcante - Integrante / Luis Figueiredo - Integrante / Hermano Moura - Integrante., Financiador(es): Ministério da Ciência e Tecnologia - Outra / Motorola Industrial LTDA - Cooperação.
2002 - Atual

Projeto de Automação de Testes (cooperação de P&D CIn-Motorola), Descrição: Este projeto vem sendo desenvolvido em cooperação com a Motorola. O Projeto de Automação de Testes vem ampliar e referendar o sucesso do Projeto "Curso Seqüencial de Formação Complementar em Análise de Testes". O escopo envolve a melhoraria contínua do processo de especificação, projeto, geração e execução de testes de aplicações móveis, através da sistematização e automatização de procedimentos anteriormeente executados de forma manual. Além da automação de testes funcionais, o desenvolvimento de ferramentas de suporte à configuração de ambiente tem proporcionado uma redução significativa de esforço dos testadores para realização dos testes automáticos e manuais. No caso de testes automáticos, o escopo inclui também a implementação e operacionalização de laboratórios para testes de stress e de performance das aplicações móveis. . , Situação: Em andamento; Natureza: Desenvolvimento. , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / Paulo Borba - Integrante / Sergio Cavalcante - Integrante / Luis Figueiredo - Integrante / Hermano Moura - Integrante., Financiador(es): Ministério da Ciência e Tecnologia - Outra / Motorola Industrial LTDA - Cooperação.
2002 - Atual

Projeto de Automação de Testes (cooperação de P&D CIn-Motorola), Descrição: Este projeto vem sendo desenvolvido em cooperação com a Motorola. O Projeto de Automação de Testes vem ampliar e referendar o sucesso do Projeto "Curso Seqüencial de Formação Complementar em Análise de Testes". O escopo envolve a melhoraria contínua do processo de especificação, projeto, geração e execução de testes de aplicações móveis, através da sistematização e automatização de procedimentos anteriormeente executados de forma manual. Além da automação de testes funcionais, o desenvolvimento de ferramentas de suporte à configuração de ambiente tem proporcionado uma redução significativa de esforço dos testadores para realização dos testes automáticos e manuais. No caso de testes automáticos, o escopo inclui também a implementação e operacionalização de laboratórios para testes de stress e de performance das aplicações móveis.. , Situação: Em andamento; Natureza: Desenvolvimento. , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / Paulo Borba - Integrante / Sergio Cavalcante - Integrante / Luis Figueiredo - Integrante / Hermano Moura - Integrante., Financiador(es): Motorola Industrial LTDA - Cooperação / Ministério da Ciência, Tecnologia e Inovação - Outra.
2002 - Atual

Projeto de Automação de Testes (cooperação de P&D CIn-Motorola), Descrição: Este projeto vem sendo desenvolvido em cooperação com a Motorola. O Projeto de Automação de Testes vem ampliar e referendar o sucesso do Projeto "Curso Seqüencial de Formação Complementar em Análise de Testes". O escopo envolve a melhoraria contínua do processo de especificação, projeto, geração e execução de testes de aplicações móveis, através da sistematização e automatização de procedimentos anteriormeente executados de forma manual. Além da automação de testes funcionais, o desenvolvimento de ferramentas de suporte à configuração de ambiente tem proporcionado uma redução significativa de esforço dos testadores para realização dos testes automáticos e manuais. No caso de testes automáticos, o escopo inclui também a implementação e operacionalização de laboratórios para testes de stress e de performance das aplicações móveis.. , Situação: Em andamento; Natureza: Desenvolvimento. , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / Paulo Borba - Integrante / Sergio Cavalcante - Integrante / Luis Figueiredo - Integrante / Hermano Moura - Integrante., Financiador(es): Ministério da Ciência, Tecnologia e Inovação - Outra / Motorola Industrial LTDA - Cooperação.
2002 - Atual

Projeto de Automação de Testes (cooperação de P&D CIn-Motorola), Descrição: Este projeto vem sendo desenvolvido em cooperação com a Motorola. O Projeto de Automação de Testes vem ampliar e referendar o sucesso do Projeto "Curso Seqüencial de Formação Complementar em Análise de Testes". O escopo envolve a melhoraria contínua do processo de especificação, projeto, geração e execução de testes de aplicações móveis, através da sistematização e automatização de procedimentos anteriormeente executados de forma manual. Além da automação de testes funcionais, o desenvolvimento de ferramentas de suporte à configuração de ambiente tem proporcionado uma redução significativa de esforço dos testadores para realização dos testes automáticos e manuais. No caso de testes automáticos, o escopo inclui também a implementação e operacionalização de laboratórios para testes de stress e de performance das aplicações móveis.. , Situação: Em andamento; Natureza: Desenvolvimento. , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / Paulo Borba - Integrante / Sergio Cavalcante - Integrante / Luis Figueiredo - Integrante / Hermano Moura - Integrante., Financiador(es): Motorola Industrial LTDA - Cooperação / Ministério da Ciência, Tecnologia e Inovação - Outra.
2002 - Atual

Projeto de Automação de Testes (cooperação de P&D CIn-Motorola), Descrição: Este projeto vem sendo desenvolvido em cooperação com a Motorola. O Projeto de Automação de Testes vem ampliar e referendar o sucesso do Projeto "Curso Seqüencial de Formação Complementar em Análise de Testes". O escopo envolve a melhoraria contínua do processo de especificação, projeto, geração e execução de testes de aplicações móveis, através da sistematização e automatização de procedimentos anteriormeente executados de forma manual. Além da automação de testes funcionais, o desenvolvimento de ferramentas de suporte à configuração de ambiente tem proporcionado uma redução significativa de esforço dos testadores para realização dos testes automáticos e manuais. No caso de testes automáticos, o escopo inclui também a implementação e operacionalização de laboratórios para testes de stress e de performance das aplicações móveis.. , Situação: Em andamento; Natureza: Desenvolvimento. , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / Paulo Borba - Integrante / Sergio Cavalcante - Integrante / Luis Figueiredo - Integrante / Hermano Moura - Integrante., Financiador(es): Motorola Industrial LTDA - Cooperação / Ministério da Ciência, Tecnologia, Inovações e Comunicações - Outra.
2002 - Atual

Projeto de Automação de Testes (cooperação de P&D CIn-Motorola), Descrição: Este projeto vem sendo desenvolvido em cooperação com a Motorola. O Projeto de Automação de Testes vem ampliar e referendar o sucesso do Projeto "Curso Seqüencial de Formação Complementar em Análise de Testes". O escopo envolve a melhoraria contínua do processo de especificação, projeto, geração e execução de testes de aplicações móveis, através da sistematização e automatização de procedimentos anteriormeente executados de forma manual. Além da automação de testes funcionais, o desenvolvimento de ferramentas de suporte à configuração de ambiente tem proporcionado uma redução significativa de esforço dos testadores para realização dos testes automáticos e manuais. No caso de testes automáticos, o escopo inclui também a implementação e operacionalização de laboratórios para testes de stress e de performance das aplicações móveis.. , Situação: Em andamento; Natureza: Desenvolvimento. , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / Paulo Borba - Integrante / Sergio Cavalcante - Integrante / Luis Figueiredo - Integrante / Hermano Moura - Integrante., Financiador(es): Motorola Industrial LTDA - Cooperação / Ministério da Ciência, Tecnologia, Inovações e Comunicações - Outra.
2002 - Atual

Projeto de Automação de Testes (cooperação de P&D CIn-Motorola), Descrição: Este projeto vem sendo desenvolvido em cooperação com a Motorola. O Projeto de Automação de Testes vem ampliar e referendar o sucesso do Projeto "Curso Seqüencial de Formação Complementar em Análise de Testes". O escopo envolve a melhoraria contínua do processo de especificação, projeto, geração e execução de testes de aplicações móveis, através da sistematização e automatização de procedimentos anteriormeente executados de forma manual. Além da automação de testes funcionais, o desenvolvimento de ferramentas de suporte à configuração de ambiente tem proporcionado uma redução significativa de esforço dos testadores para realização dos testes automáticos e manuais. No caso de testes automáticos, o escopo inclui também a implementação e operacionalização de laboratórios para testes de stress e de performance das aplicações móveis.. , Situação: Em andamento; Natureza: Desenvolvimento. , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / Paulo Borba - Integrante / Sergio Cavalcante - Integrante / Luis Figueiredo - Integrante / Hermano Moura - Integrante., Financiador(es): Ministério da Ciência, Tecnologia, Inovações e Comunicações - Outra / Motorola Industrial LTDA - Cooperação.
2002 - Atual

Projeto de Automação de Testes (cooperação de P&D CIn-Motorola), Descrição: Este projeto vem sendo desenvolvido em cooperação com a Motorola. O Projeto de Automação de Testes vem ampliar e referendar o sucesso do Projeto "Curso Seqüencial de Formação Complementar em Análise de Testes". O escopo envolve a melhoraria contínua do processo de especificação, projeto, geração e execução de testes de aplicações móveis, através da sistematização e automatização de procedimentos anteriormeente executados de forma manual. Além da automação de testes funcionais, o desenvolvimento de ferramentas de suporte à configuração de ambiente tem proporcionado uma redução significativa de esforço dos testadores para realização dos testes automáticos e manuais. No caso de testes automáticos, o escopo inclui também a implementação e operacionalização de laboratórios para testes de stress e de performance das aplicações móveis.. , Situação: Em andamento; Natureza: Desenvolvimento. , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / Paulo Borba - Integrante / Sergio Cavalcante - Integrante / Luis Figueiredo - Integrante / Hermano Moura - Integrante., Financiador(es): Ministério da Ciência, Tecnologia, Inovações e Comunicações - Outra / Motorola Industrial LTDA - Cooperação.
2002 - Atual

Projeto de Automação de Testes (cooperação de P&D CIn-Motorola), Descrição: Este projeto vem sendo desenvolvido em cooperação com a Motorola. O Projeto de Automação de Testes vem ampliar e referendar o sucesso do Projeto "Curso Seqüencial de Formação Complementar em Análise de Testes". O escopo envolve a melhoraria contínua do processo de especificação, projeto, geração e execução de testes de aplicações móveis, através da sistematização e automatização de procedimentos anteriormeente executados de forma manual. Além da automação de testes funcionais, o desenvolvimento de ferramentas de suporte à configuração de ambiente tem proporcionado uma redução significativa de esforço dos testadores para realização dos testes automáticos e manuais. No caso de testes automáticos, o escopo inclui também a implementação e operacionalização de laboratórios para testes de stress e de performance das aplicações móveis.. , Situação: Em andamento; Natureza: Desenvolvimento.
2002 - Atual

Projeto de Automação de Testes (cooperação de P&D CIn-Motorola), Descrição: Este projeto vem sendo desenvolvido em cooperação com a Motorola. O Projeto de Automação de Testes vem ampliar e referendar o sucesso do Projeto "Curso Seqüencial de Formação Complementar em Análise de Testes". O escopo envolve a melhoraria contínua do processo de especificação, projeto, geração e execução de testes de aplicações móveis, através da sistematização e automatização de procedimentos anteriormeente executados de forma manual. Além da automação de testes funcionais, o desenvolvimento de ferramentas de suporte à configuração de ambiente tem proporcionado uma redução significativa de esforço dos testadores para realização dos testes automáticos e manuais. No caso de testes automáticos, o escopo inclui também a implementação e operacionalização de laboratórios para testes de stress e de performance das aplicações móveis.. , Situação: Em andamento; Natureza: Desenvolvimento. , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / Paulo Borba - Integrante / Sergio Cavalcante - Integrante / Luis Figueiredo - Integrante / Hermano Moura - Integrante., Financiador(es): Motorola Industrial LTDA - Cooperação / Ministério da Ciência, Tecnologia, Inovações e Comunicações - Outra.
2002 - Atual

Projeto de Automação de Testes (cooperação de P&D CIn-Motorola), Descrição: Este projeto vem sendo desenvolvido em cooperação com a Motorola. O Projeto de Automação de Testes vem ampliar e referendar o sucesso do Projeto "Curso Seqüencial de Formação Complementar em Análise de Testes". O escopo envolve a melhoraria contínua do processo de especificação, projeto, geração e execução de testes de aplicações móveis, através da sistematização e automatização de procedimentos anteriormeente executados de forma manual. Além da automação de testes funcionais, o desenvolvimento de ferramentas de suporte à configuração de ambiente tem proporcionado uma redução significativa de esforço dos testadores para realização dos testes automáticos e manuais. No caso de testes automáticos, o escopo inclui também a implementação e operacionalização de laboratórios para testes de stress e de performance das aplicações móveis.. , Situação: Em andamento; Natureza: Desenvolvimento. , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / Paulo Borba - Integrante / Sergio Cavalcante - Integrante / Luis Figueiredo - Integrante / Hermano Moura - Integrante., Financiador(es): Motorola Industrial LTDA - Cooperação / Ministério da Ciência, Tecnologia, Inovações e Comunicações - Outra.
2002 - Atual

Projeto de Automação de Testes (cooperação de P&D CIn-Motorola), Descrição: Este projeto vem sendo desenvolvido em cooperação com a Motorola. O Projeto de Automação de Testes vem ampliar e referendar o sucesso do Projeto "Curso Seqüencial de Formação Complementar em Análise de Testes". O escopo envolve a melhoraria contínua do processo de especificação, projeto, geração e execução de testes de aplicações móveis, através da sistematização e automatização de procedimentos anteriormeente executados de forma manual. Além da automação de testes funcionais, o desenvolvimento de ferramentas de suporte à configuração de ambiente tem proporcionado uma redução significativa de esforço dos testadores para realização dos testes automáticos e manuais. No caso de testes automáticos, o escopo inclui também a implementação e operacionalização de laboratórios para testes de stress e de performance das aplicações móveis.. , Situação: Em andamento; Natureza: Desenvolvimento. , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / Paulo Borba - Integrante / Sergio Cavalcante - Integrante / Luis Figueiredo - Integrante / Hermano Moura - Integrante., Financiador(es): Ministério da Ciência, Tecnologia, Inovações e Comunicações - Outra / Motorola Industrial LTDA - Cooperação.
2002 - Atual

Projeto de Automação de Testes (cooperação de P&D CIn-Motorola), Descrição: Este projeto vem sendo desenvolvido em cooperação com a Motorola. O Projeto de Automação de Testes vem ampliar e referendar o sucesso do Projeto "Curso Seqüencial de Formação Complementar em Análise de Testes". O escopo envolve a melhoraria contínua do processo de especificação, projeto, geração e execução de testes de aplicações móveis, através da sistematização e automatização de procedimentos anteriormeente executados de forma manual. Além da automação de testes funcionais, o desenvolvimento de ferramentas de suporte à configuração de ambiente tem proporcionado uma redução significativa de esforço dos testadores para realização dos testes automáticos e manuais. No caso de testes automáticos, o escopo inclui também a implementação e operacionalização de laboratórios para testes de stress e de performance das aplicações móveis.. , Situação: Em andamento; Natureza: Desenvolvimento. , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / Paulo Borba - Integrante / Sergio Cavalcante - Integrante / Luis Figueiredo - Integrante / Hermano Moura - Integrante., Financiador(es): Ministério da Ciência, Tecnologia, Inovações e Comunicações - Outra / Motorola Industrial LTDA - Cooperação.
2002 - Atual

Projeto de Automação de Testes (cooperação de P&D CIn-Motorola), Descrição: Este projeto vem sendo desenvolvido em cooperação com a Motorola. O Projeto de Automação de Testes vem ampliar e referendar o sucesso do Projeto "Curso Seqüencial de Formação Complementar em Análise de Testes". O escopo envolve a melhoraria contínua do processo de especificação, projeto, geração e execução de testes de aplicações móveis, através da sistematização e automatização de procedimentos anteriormeente executados de forma manual. Além da automação de testes funcionais, o desenvolvimento de ferramentas de suporte à configuração de ambiente tem proporcionado uma redução significativa de esforço dos testadores para realização dos testes automáticos e manuais. No caso de testes automáticos, o escopo inclui também a implementação e operacionalização de laboratórios para testes de stress e de performance das aplicações móveis.. , Situação: Em andamento; Natureza: Desenvolvimento. , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / Paulo Borba - Integrante / Sergio Cavalcante - Integrante / Luis Figueiredo - Integrante / Hermano Moura - Integrante., Financiador(es): Motorola Industrial LTDA - Cooperação / Ministério da Ciência, Tecnologia e Inovações - Outra.
2002 - Atual

Projeto de Automação de Testes (cooperação de P&D CIn-Motorola), Descrição: Este projeto vem sendo desenvolvido em cooperação com a Motorola. O Projeto de Automação de Testes vem ampliar e referendar o sucesso do Projeto "Curso Seqüencial de Formação Complementar em Análise de Testes". O escopo envolve a melhoraria contínua do processo de especificação, projeto, geração e execução de testes de aplicações móveis, através da sistematização e automatização de procedimentos anteriormeente executados de forma manual. Além da automação de testes funcionais, o desenvolvimento de ferramentas de suporte à configuração de ambiente tem proporcionado uma redução significativa de esforço dos testadores para realização dos testes automáticos e manuais. No caso de testes automáticos, o escopo inclui também a implementação e operacionalização de laboratórios para testes de stress e de performance das aplicações móveis.. , Situação: Em andamento; Natureza: Desenvolvimento. , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / Paulo Borba - Integrante / Sergio Cavalcante - Integrante / Luis Figueiredo - Integrante / Hermano Moura - Integrante., Financiador(es): Motorola Industrial LTDA - Cooperação / Ministério da Ciência, Tecnologia e Inovações - Outra.
2002 - Atual

Projeto de Automação de Testes (cooperação de P&D CIn-Motorola), Descrição: Este projeto vem sendo desenvolvido em cooperação com a Motorola. O Projeto de Automação de Testes vem ampliar e referendar o sucesso do Projeto "Curso Seqüencial de Formação Complementar em Análise de Testes". O escopo envolve a melhoraria contínua do processo de especificação, projeto, geração e execução de testes de aplicações móveis, através da sistematização e automatização de procedimentos anteriormeente executados de forma manual. Além da automação de testes funcionais, o desenvolvimento de ferramentas de suporte à configuração de ambiente tem proporcionado uma redução significativa de esforço dos testadores para realização dos testes automáticos e manuais. No caso de testes automáticos, o escopo inclui também a implementação e operacionalização de laboratórios para testes de stress e de performance das aplicações móveis.. , Situação: Em andamento; Natureza: Desenvolvimento. , Integrantes: Augusto Cezar Alves Sampaio - Coordenador / Paulo Borba - Integrante / Sergio Cavalcante - Integrante / Luis Figueiredo - Integrante / Hermano Moura - Integrante., Financiador(es): Ministério da Ciência, Tecnologia e Inovações - Outra / Motorola Industrial LTDA - Cooperação.

Prêmios

2025

Membro da Academia Brasileira de Ciências, Academia Brasileira de Ciências (ABC).

2022

Best Paper Award - 2nd place: Compositional Verification of Simulink Block Diagrams Using tock-CSP and CSP-Prover, SBMF - SBC.

2021

Membro da Academia Pernambucana de Ciëncias, Academia Pernambucana de Ciëncias.

2018

Prêmio Mérito Científico, SBC - Sociedade Brasileira de Computação.

2017

Pesquisador Homenageado, SBES - Simpósio Brasileiro de Engenharia de Software.

2016

Doutor Honoris Causa, University of York, Reino Unido.

2010

Comendador da Ordem Nacional do Mérito Científico, Presidência da República do Brasil.

2007

Orientador do aluno de Iniciação Científica Joabe Bezerra Jesus Júnior, premiado em primeiro lugar na área Ciências Exatas e da Terra, no XIV Congresso de IC da UFPE, UFPE.

2006

Coordenador e um dos idealizadores do programa Residência em Software, premiado em primeiro lugar com o prêmio Dorgival Brandão Júnior da Qualidade e Produtividade em Software, referente ao ciclo 2005, MCT - SEPIN - PBQP (Programa Brasileiro de Qualidade e Produtividade) Software.

2006

Best Paper Award. Formal Specification Generation from Requirement Documents. Co-autoria com gustavo Cabral. Artigo apresenta resultados teóricos e práticos da cooperação CIn-Motorola., SBC - SBMF (Simpósio Brasileiro de Métodos Formais).

2006

Prêmio de Inovação FINEP (Região Sudeste) para o BTC (Brazil Test Center) que envolve Motorola, CIn, CESAR, Eldorado e UFSC. Coordeno o projeto pelo CIn-UFPE., FINEP.

2006

Prêmio Excelência em P&D da Revista Anuário Informática Hoje para o BTC (Brazil Test Center), cooperação entre a Motorola, o CIn-UFPE, O CESAR, o Eldorado e a UFSC. Coordeno o projeto pelo CIn-UFPE., Revista Anuário Informática Hoje.

2004

Orientador da Dissertação de Mestrado de Adalberto Cajueiro de Farias, premiada em 3o. lugar no Concurso de Teses e Dissertacoes (CTD), SBC - Sociedade Brasileira de Computação.

2002

Orientador da Tese de Doutorado de Alexandre Mota premiada em 1o. lugar no Concurso de Teses e Dissertacoes (CTD) da SBC, SBC - Sociedade Brasileira de Computacao.

2002

Coordenador do projeto CO-OP, CNPq, 1999-2001, merecedor de menção honrosa na avaliação final (http://www.cnpq.br/areas/sociedadeinformacao/protem-cc/avaliacao2001.htm#_Projeto_CO-OP), CNPq.

2002

Líder do grupo de pesquisa de Métodos Formais no CIn-UFPE, classificado entre os melhores do mundo em produção científica (http://floc02.diku.dk/misc/hats.html)., Federated Logic Conference (FloC).

2001

Orientador da Tese de Doutorado de Leila Silva premiada em 1o. lugar no Concurso de Teses e Dissertacoes (CTD) da SBC, SBC - Sociedade Brasileira de Computacao.

1988

DIssertação de Mestrado Aprovada com Distinção, Centro de Informática da UFPE.

1985

Aluno Laureado do Curso de Graduação em Ciência da Computação da UFPE, Turma 1985, Universidade Federal de Pernambuco.

1981

Auluno Laureado do Colégio Contato, Colégio Contato.

Histórico profissional

Endereço profissional

Universidade Federal de Pernambuco, Centro de Informática. , Avenida Jornalista Aníbal Fernandes, Cidade Universitária, 50740560 - Recife, PE - Brasil - Caixa-postal: 52071370, Telefone: (081) 21268430, Ramal: 4011, Fax: (081) 21268438

Experiência profissional

2020 - Atual

East China Normal University

Vínculo: , Enquadramento Funcional:

2011 - 2014

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior

Vínculo: , Enquadramento Funcional: Membro Comitê Assessor Ciência da Computação

2008 - 2011

Conselho Nacional de Desenvolvimento Científico e Tecnológico, CNPq

Vínculo: Servidor Público, Enquadramento Funcional: Membro Comitê Assesor Ciência da Computação

2007 - Atual

Universidade Federal de Pernambuco

Vínculo: Servidor Público, Enquadramento Funcional: Professor titular, Carga horária: 40, Regime: Dedicação exclusiva.

1995 - 2007

Universidade Federal de Pernambuco

Vínculo: Servidor Público, Enquadramento Funcional: Professor Adjunto, Carga horária: 40, Regime: Dedicação exclusiva.

1993 - 1995

Universidade Federal de Pernambuco

Vínculo: Bolsista recém-doutor, Enquadramento Funcional: Professor e Pesquisador, Carga horária: 40, Regime: Dedicação exclusiva.

1988 - 1989

Universidade Federal de Pernambuco

Vínculo: Colaborador, Enquadramento Funcional: ASSIST.ENSINO PESQ.DEPT.INFORMATICA, Carga horária: 40, Regime: Dedicação exclusiva.

Atividades

10/2013
Direção e administração, Centro de Informática.,Cargo ou função, Coordenador de Cooperação e Empreendedorismo.
05/2006
Direção e administração, Centro de Informática.,Cargo ou função, Chefe de Departamento.
03/2004
Conselhos, Comissões e Consultoria, Centro de Informática.,Cargo ou função, Consultor Ad Hoc da CAPES.
08/2003
Conselhos, Comissões e Consultoria, Centro de Informática.,Cargo ou função, Comissão de Avaliação de Seleção de Candidatos ao Doutorado do CIn-UFPE.
12/2002
Ensino, Curso Sequencial de Formação Complementar, Nível: Especialização,Disciplinas ministradas, Análise e Projeto de Software com UML
11/2002
Direção e administração, Centro de Informática.,Cargo ou função, Coordenador de Programa - Convênio CIn-Motorola.
09/1995
Conselhos, Comissões e Consultoria, Centro de Informática.,Cargo ou função, Membro do Colegiado da Pós-Graduação.
03/1994
Ensino, Ciencia da Computacao, Nível: Graduação,Disciplinas ministradas, Trabalho de Graduação, Iniciação Científica, Programação Concorrente e Distribuída, Engenharia de Software, Análise e Projeto de Sistemas, Métodos Formais, Teoria da Especificação
03/1994
Ensino, Ciências da Computação, Nível: Pós-Graduação,Disciplinas ministradas, Linguagens de Programação, Especificação de Sistemas Distribuídos, Especificação Formal, Paradigmas de Linguagens de Programação, Tópicos Avançados em Engenharia de Software 1, Tópicos Avançados em Engenharia de Software 2, Tópicos Avançados em Engenharia de Software 3, Trabalho Individual
11/1993
Conselhos, Comissões e Consultoria, Centro de Informática.,Cargo ou função, Consultor Ad hoc do CNPq.
05/2005 - 10/2013
Direção e administração, Centro de Informática.,Cargo ou função, Coordenador de Pesquisa do CIn-UFPE.
12/2005 - 09/2006
Conselhos, Comissões e Consultoria, Centro de Informática.,Cargo ou função, Presidente da Comisssão Especial de Métodos Formais (CEMF) - SBC.
07/2004 - 07/2004
Conselhos, Comissões e Consultoria, Centro de Informática.,Cargo ou função, Membro convidado para compor comissão de avaliação de cursos de pós-graduação (triênio 2001-2003).
08/2001 - 07/2003
Direção e administração, Centro de Informática.,Cargo ou função, Coordenador da Pós-Graduação.
09/1997 - 07/2002
Ensino, Especialização em Tecnologias da Informação, Nível: Especialização,Disciplinas ministradas, Programação orientada a objetos e Java, Fundamentos de Programação
10/1998 - 07/2001
Direção e administração, Centro de Informática.,Cargo ou função, Vice-Coordenador da Pós-Graduação.
10/1999 - 10/2000
Conselhos, Comissões e Consultoria, Centro de Informática.,Cargo ou função, Presidente da Comissão Especial de Engenharia de Software (CEES) - SBC.
03/1998 - 12/1998
Conselhos, Comissões e Consultoria, Centro de Informática.,Cargo ou função, Membro Comissão Verificadora do MEC para avaliar cursos de Graduação do MEC.
03/1996 - 08/1998
Direção e administração, Centro de Informática.,Cargo ou função, Vice-Coordenador da Graduação do CIn-UFPE.
03/1996 - 08/1998
Conselhos, Comissões e Consultoria, Centro de Informática.,Cargo ou função, Presidente da Comissão de Alocação Docente.
03/1996 - 08/1998
Conselhos, Comissões e Consultoria, Centro de Informática.,Cargo ou função, Coordenador de Monitoria.
02/1996 - 05/1997
Ensino, Especialização em Informática na Educação, Nível: Especialização,Disciplinas ministradas, Programação II, Programação I
03/1996 - 07/1996
Conselhos, Comissões e Consultoria, Pró-Reitoria de Pesquisa e Pós-Graduação.,Cargo ou função, Comissão de Seleção de Alunos de Iniciação Científica.

2000 - 2000

International Institute for Software Technology - United Nations University

Vínculo: Colaborador, Enquadramento Funcional: Professor visitante e colaborador em projetos

Outras informações:
Cooperação formalizada através de um Memorandum of Understanding entre o CIn-UFPE e o UNU/IIST. No contexto desta cooperação, já foram organizadas 2 Escolas de Computação em Recife e visita de professores e alunos nas duas direções.

Atividades

11/2006 - 11/2006
Ensino, ICTAC School 2006, Nível: Pós-Graduação,Disciplinas ministradas, Refinement in object-oriented Development
11/2004 - 12/2004
Direção e administração, UNU/IIST.,Cargo ou função, Coordenador de Escola de Computação - Refinement Techniques in Sofware Engineering.
11/2004 - 12/2004
Ensino, Pernambuco School on Software Engineering, Nível: Pós-Graduação,Disciplinas ministradas, Refinement in object-oriented development: sequential Java
12/2001 - 12/2001
Direção e administração, UNU/IIST.,Cargo ou função, Coordenador de Escola de Computação - Engenharia de Software.
11/2001 - 12/2001
Ensino, Summer School on Object-Oriented Technology, Nível: Pós-Graduação,Disciplinas ministradas, Object-oriented analysis and design
05/2001 - 06/2001
Ensino, Formação dos fellows, Nível: Pós-Graduação,Disciplinas ministradas, Programming Language Concepts and Paradigms

1994 - 2001

University of Oxford

Vínculo: Professor Visitante, Enquadramento Funcional: Professor visitante e colaborador em projetos

Outras informações:
De 1994 a 1997, obtive um finaciamento da Comunidade Européia, na linha Keep in Touch Activity, vinculado a Universidade de Oxford, que permitiu intensa cooperação com pesquisadores desta universidade, bem como com pesquisadores de outras 3 universidades européias que participaram do Projeto ProCoS. Em seguida, iniciamos uma outra cooperação: Refinement Calculi for Sequential and Concurrent Programas, que se estendeu até agosto/2001.

Atividades

04/1997 - 04/1997
Outras atividades técnico-científicas , Computing Laboratory, Computing Laboratory.,Atividade realizada, Participação no workshop do projeto ProCoS - em Reading-UK.
03/1996 - 03/1996
Outras atividades técnico-científicas , Computing Laboratory, Computing Laboratory.,Atividade realizada, Visita vientífica à Universitat Oldenburg (Projeto ProCoS).
01/1995 - 02/1995
Outras atividades técnico-científicas , Computing Laboratory, Computing Laboratory.,Atividade realizada, Professor visitante do Computing Lab no contexto do projeto ProCoS.

1984 - 1987

Centro de Prestação de Serviços Técnicos de Pernambuco

Vínculo: Celetista, Enquadramento Funcional: Programador Analista de Sistemas, Carga horária: 30

2007 - 2009

Sociedade Brasileira de Computação - Porto Alegre

Vínculo: Diretoria de Planejamento, Enquadramento Funcional: Diretor de Planejamento, Carga horária: 4