Augusto Cezar Alves Sampaio

Bolsista de Produtividade em Pesquisa do CNPq - Nível 1A

  • Endereço para acessar este CV: http://lattes.cnpq.br/3977760354511853
  • Última atualização do currículo em 16/09/2018


Professor Titular do Centro de Informática (CIn) da UFPE, possui graduação e mestrado em Ciência da Computação pela UFPE e doutorado pela Oxford University. Em 2018, recebeu o Prêmio Mérito Científico da SBC. Pesquisador Homenageado pelo SBES, em 2017. Em 2016, recebeu o título de Doutor Honoris Causa da University of York, Reino Unido. 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. É membro do Formal Methods Europe Fellowship Award Committee e 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 semi-formais (como UML e SysML); modelos de componentes; e na geração automática de testes a partir de modelos. 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, atualmente, como Coordenador de Cooperação com a Indústria e Chefia do Departamento de Ciência da Computação. (Texto informado pelo autor)


Identificação


Nome
Augusto Cezar Alves Sampaio
Nome em citações bibliográficas
SAMPAIO, A. C. A.;Sampaio, Augusto;Sampaio, Augusto C. A.;SAMPAIO, A;Sampaio, A.;Augusto Sampaio

Endereço


Endereço Profissional
Universidade Federal de Pernambuco, Centro de Informática.
Av. Jornalista Anibal Fernandes, s/n
Cidade universitária
50740560 - Recife, PE - Brasil
Telefone: (081) 21268430
Ramal: 4011
Fax: (081) 21268438


Formação acadêmica/titulação


1989 - 1993
Doutorado em Software Engineering.
University of Oxford, OX, Inglaterra.
Título: An Algebraic Approach to Compiler Design, Ano de obtenção: 1993.
Orientador: Charles A. R. Hoare.
Bolsista do(a): Conselho Nacional de Desenvolvimento Científico e Tecnológico, CNPq, Brasil.
1986 - 1988
Mestrado em Ciências da Computação.
Universidade Federal de Pernambuco, UFPE, Brasil.
Título: Zc: Uma Notação para Especificação de Sistemas Complexos,Ano de Obtenção: 1988.
Orientador: 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
1982 - 1985
Graduação em Ciencia da Computacao.
Universidade Federal de Pernambuco, UFPE, Brasil.




Atuação Profissional



Coordenação de Aperfeiçoamento de Pessoal de Nível Superior, CAPES, Brasil.
Vínculo institucional

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


Conselho Nacional de Desenvolvimento Científico e Tecnológico, CNPq, Brasil.
Vínculo institucional

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


Universidade Federal de Pernambuco, UFPE, Brasil.
Vínculo institucional

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

Vínculo institucional

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

Vínculo institucional

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

Vínculo institucional

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

Atividades

10/2013 - Atual
Direção e administração, Centro de Informática, .

Cargo ou função
Coordenador de Cooperação e Empreendedorismo.
05/2006 - Atual
Direção e administração, Centro de Informática, .

Cargo ou função
Chefe de Departamento.
03/2004 - Atual
Conselhos, Comissões e Consultoria, Centro de Informática, .

Cargo ou função
Consultor Ad Hoc da CAPES.
08/2003 - Atual
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 - Atual
Ensino, Curso Sequencial de Formação Complementar, Nível: Especialização

Disciplinas ministradas
Análise e Projeto de Software com UML
11/2002 - Atual
Direção e administração, Centro de Informática, .

Cargo ou função
Coordenador de Programa - Convênio CIn-Motorola.
09/1995 - Atual
Conselhos, Comissões e Consultoria, Centro de Informática, .

Cargo ou função
Membro do Colegiado da Pós-Graduação.
03/1994 - Atual
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 - Atual
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 - Atual
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.

International Institute for Software Technology - United Nations University, IIST-UNU, Macau.
Vínculo institucional

2000 - 2000
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

University of Oxford, OX, Inglaterra.
Vínculo institucional

1994 - 2001
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.

Centro de Prestação de Serviços Técnicos de Pernambuco, CETEPE, Brasil.
Vínculo institucional

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



Projetos de pesquisa


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 - 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.
2016 - Atual
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: Em andamento; Natureza: Pesquisa.
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.
2013 - Atual
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: Em andamento; 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 neg ocios. 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): Universidade Federal de Campina Grande - Cooperação / Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro.
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): Ministério da Ciência, Tecnologia, Inovações e Comunicações - Auxílio financeiro / Motorola Industrial LTDA - Cooperação.Número de orientações: 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.
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: 23 / Número de orientações: 12
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: 6 / Número de orientações: 2
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 / Technical University of Denmark - Cooperação / University of Oldenburgh - Cooperação / University of Kiel - Cooperação / University of Oxford - Cooperação.
Número de produções C, T & A: 6 / Número de orientações: 2


Projetos de extensão


2002 - Atual
Curso Seqüencial de Formação Complementar em Análise de Testes
Descrição: Este projeto vem sendo desenvolvido no contexto de uma cooperação entre o CIn/UFPE e a Motorola, envolvendo três ações principais, sendo uma delas o projeto denominado Curso Seqüencial de Formação Complementar em Análise de Testes. Este projeto tem permitido a implantação de um modelo inovador de formação. O programa segue a filosofia da tão consolidada Residência Médica: na Residência em Software, o papel dos hospitais é desempenhado pelas fábricas de software e uma instituição de ensino (tipicamente uma universidade) oferece a formação teórica. O programa já formou mais de 350 profissionais de diversos estrados do Brasil. O programa está inserido no contexto da Política de Software do Ministério da Ciência e Tecnologia (MCT), a qual estabelece as seguintes premissas básicas: · Parceria com universidades e empresas locais e internacionais; · Melhoria da qualidade em processo e produto; · Redução do custo operacional O modedo de Residencia em Software foi premiado pelo Ministério de Ciência e Tecnologia (Prêmio Dorgival Brandão Júnior de Qualidade e Produtividade em Software MCT ? SEPIN ? PBQP Software), tendo influenciado editais do CNPq para escalar o programa para todo o Brasil..
Situação: Em andamento; Natureza: Extensão.


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.


Membro de corpo editorial


2015 - Atual
Periódico: Formal Aspects of Computing (Internet)
2015 - Atual
Periódico: Journal of the Brazilian Computer Society (Impresso)


Membro de comitê de assessoramento


2015 - Atual
Agência de fomento: Formal Methods Europe
2014 - Atual
Agência de fomento: International Federation for Information Processing
2011 - 2014
Agência de fomento: Coordenação de Aperfeiçoamento de Pessoal de Nível Superior
2008 - 2011
Agência de fomento: Conselho Nacional de Desenvolvimento Científico e Tecnológico


Revisor de periódico


1992 - 1992
Periódico: Journal of Functional Programming
2002 - Atual
Periódico: Electronic Notes in Theoretical Computer Science
1998 - Atual
Periódico: Journal of the Brazilian Computer Society
1994 - 1994
Periódico: Nordic Journal of Computing
2001 - 2001
Periódico: Theoretical Computer Science
1994 - 1995
Periódico: Bulletin of the IGPL
2004 - 2004
Periódico: Software and Systems Modeling (1619-1366)
2011 - Atual
Periódico: Formal Aspects of Computing
2010 - Atual
Periódico: Science of Computer Programming (Print)


Revisor de projeto de fomento


1995 - Atual
Agência de fomento: Coordenação de Aperfeiçoamento de Pessoal de Nível Superior
1995 - Atual
Agência de fomento: Conselho Nacional de Desenvolvimento Científico e Tecnológico
1997 - 2001
Agência de fomento: Fundação de Amparo à Pesquisa do Estado de São Paulo


Áreas de atuação


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


Idiomas


Inglês
Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.
Espanhol
Compreende Razoavelmente, Fala Pouco, Lê Razoavelmente, Escreve Pouco.
Francês
Lê Pouco.


Prêmios e títulos


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.


Produções



Produção bibliográfica
Citações

SCOPUS
Total de trabalhos:91
Total de citações:639

Artigos completos publicados em periódicos

1.
CONSERVA FILHO, M.S.2018CONSERVA 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.

2.
GHEYI, ROHIT2017GHEYI, 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.

3.
Lima, Lucas2017Lima, 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.

4.
ARAUJO, HUGO2017ARAUJO, 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.

5.
FALASCHI, MORENO2017FALASCHI, MORENO ; Sampaio, Augusto . Editorial. FORMAL ASPECTS OF COMPUTING, v. 29, p. 381-382, 2017.

6.
OLIVEIRA, M. V. M.2016OLIVEIRA, 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.

7.
CARVALHO, GUSTAVO2016CARVALHO, GUSTAVO ; Cavalcanti, Ana ; Sampaio, Augusto . Modelling timed reactive systems from natural-language requirements. Formal Aspects of Computing (Internet), v. 1, p. 1-41, 2016.

8.
Nogueira, Sidney2014Nogueira, Sidney ; Sampaio, Augusto ; Mota, Alexandre . Test generation from state based use case models. Formal Aspects of Computing (Internet), v. 26, p. 441-490, 2014.

9.
CARVALHO, GUSTAVO2014CARVALHO, 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.

10.
Sampaio, Augusto2014Sampaio, 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.

11.
Naumann, David A.2012 Naumann, David A. ; Sampaio, Augusto ; Silva, Leila . Refactoring and representation independence for class hierarchies. Theoretical Computer Science, v. 433, p. 60-97, 2012.

12.
Gomes, Adriano2012Gomes, 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.

13.
Duarte, Rafael2011Duarte, Rafael ; Mota, Alexandre ; Sampaio, Augusto . Introducing concurrency in sequential Java via laws. Information Processing Letters (Print), v. 111, p. 129-134, 2011.

14.
Perna, Juan2011Perna, Juan ; Woodcock, Jim ; Sampaio, Augusto ; Iyoda, Juliano . Correct hardware synthesis. Acta Informatica, v. 48, p. 363-396, 2011.

15.
Ramos, Rodrigo2010Ramos, Rodrigo ; Sampaio, Augusto ; Mota, Alexandre . Conformance notions for the coordination of interaction components. Science of Computer Programming (Print), v. 75, p. 350-373, 2010.

16.
M. Cornelio2010M. Cornelio ; Cavalcanti, Ana ; Sampaio, Augusto . Sound Refactorings. Science of Computer Programming (Print), v. 75, p. 106-133, 2010.

17.
Sherif, Adnan2010Sherif, 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.

18.
Duran, Adolfo2010Duran, 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.

19.
Falcão, Flávia2009Falcã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.

20.
Cabral, Gustavo2008Cabral, 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.

21.
FERREIRA, P2008FERREIRA, P ; SAMPAIO, A ; Mota, A . Viewing CSP Specifications with UML-RT Diagrams?. Electronic Notes in Theoretical Computer Science, v. 195, p. 57-74, 2008.

22.
XAVIER, M2008XAVIER, M ; Cavalcanti, A ; SAMPAIO, A . Type Checking Circus Specifications. Electronic Notes in Theoretical Computer Science, v. 195, p. 75-93, 2008.

23.
Farias, Adalberto2008Farias, Adalberto ; Mota, Alexandre ; Sampaio, Augusto . Compositional abstraction of CSP Z processes. Journal of the Brazilian Computer Society (Impresso), v. 14, p. 23-44, 2008.

24.
Cavalcanti, Ana2005Cavalcanti, Ana ; Sampaio, Augusto ; Woodcock, Jim . Unifying classes and processes. Software and Systems Modeling (Print), Alemanha, v. 4, n.3, p. 277-296, 2005.

25.
CORNELIO, M2005CORNELIO, M ; Cavalcanti, A ; SAMPAIO, A . Refactoring Towards a Layered Architecture. Electronic Notes in Theoretical Computer Science, v. 130, p. 281-300, 2005.

26.
BORBA, P2004 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.

27.
SAMPAIO, A2004SAMPAIO, 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.

28.
Silva, Leila2004 Silva, Leila ; Sampaio, Augusto ; Barros, Edna . A Constructive Approach to Hardware/Software Partitioning. Formal Methods in System Design, v. 24, p. 45-90, 2004.

29.
Cavalcanti, Ana2003Cavalcanti, Ana ; Sampaio, Augusto ; Woodcock, Jim . A Refinement Strategy for Circus. Formal Aspects of Computing, Inglaterra, v. 15, n.2-3, p. 146-181, 2003.

30.
Cavalcanti, A2002Cavalcanti, A ; SAMPAIO, A ; WOODCOCK, J . Refinement of Actions in Circus,. Electronic Notes in Theoretical Computer Science, v. 70, p. 132-162, 2002.

31.
CORNELIO, M2002CORNELIO, M ; Cavalcanti, A ; SAMPAIO, A . Refactoring by Transformation. Electronic Notes in Theoretical Computer Science, v. 70, p. 311-330, 2002.

32.
Mota, A2001Mota, 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.

33.
P. Borba2000P. 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.

34.
Cavalcanti, A1999Cavalcanti, 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.

35.
Cavalcanti, Ana1998Cavalcanti, 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.

36.
Campos, Marcilia A.1996Campos, 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.

37.
HOARE, C. A. R.1993 HOARE, C. A. R. ; Jifeng, He ; Sampaio, A. . Normal form approach to compiler design. Acta Informatica, Estados Unidos, v. 30, p. 701-739, 1993.

Livros publicados/organizados ou edições
1.
Augusto Sampaio; Farn Wang. . Theoretical Aspects of Computing ? ICTAC 2016. 1. ed. Berlin: Springer - Lecture Notes in Computer Science, 2016. v. 1. 479p .

2.
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 .

3.
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 .

4.
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 .

5.
SAMPAIO, A. C. A.. Simpósio Brasileiro de Métodos Formais. 2. ed. SBC - Sociedade Brasileira de Computação, 2005. 200p .

6.
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 .

7.
SAMPAIO, A. C. A.. An Algebraic Approach To Compiler Design. 1. ed. Londres: World Scientific, 1997. v. 4. 200p .

Capítulos de livros publicados
1.
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.

2.
P. Machado ; Sampaio, Augusto . Automatic Test-Case Generation. Testing Techniques in Software Engineering. Berlin: Springer Berlin / Heidelberg, 2010, v. 6153, p. 59-103.

3.
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.

4.
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.

5.
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.

6.
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.

7.
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.

Textos em jornais de notícias/revistas
1.
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.

2.
Augusto Sampaio; Iyoda, Juliano . Engenharia de Sistemas de Sistemas. Computação Brasil, p. 40.

Trabalhos completos publicados em anais de congressos
1.
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.

2.
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.

3.
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.

4.
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.

5.
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.

6.
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.

7.
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.

8.
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.

9.
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.

10.
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.

11.
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.

12.
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.

13.
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.

14.
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.

15.
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.

16.
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.

17.
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.

18.
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.

19.
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.

20.
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.

21.
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.

22.
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.

23.
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.

24.
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.

25.
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.

26.
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.

27.
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.

28.
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.

29.
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.

30.
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.

31.
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.

32.
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.

33.
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.

34.
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.

35.
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.

36.
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.

37.
Silva, Leila ; Sampaio, Augusto ; Liu, Zhiming . Laws of Object-Orientation with Reference Semantics. In: , 2008, Cape Town. . p. 217-226.

38.
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.

39.
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.

40.
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.

41.
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.

42.
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.

43.
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.

44.
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.

45.
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.

46.
Mesquita, W. ; Sampaio, A. ; de Melo, A.C.V. . A strategy for the formal composition of frameworks. In: , 2005, Koblenz. . p. 404-413.

47.
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.

48.
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.

49.
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.

50.
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.

51.
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.

52.
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.

53.
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.

54.
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.

55.
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.

56.
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.

57.
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.

58.
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.

59.
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.

60.
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.

61.
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.

62.
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.

63.
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.

64.
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.

65.
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.

66.
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.

67.
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.

68.
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.

69.
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.

70.
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.

71.
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.

72.
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.

73.
SAMPAIO, A. C. A.. Reusing Algebraic Theories in Program Transformation. In: Program Transformation Workshop, 1996, Durham. Program Transformation Workshop, 1996.

74.
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.

75.
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.

76.
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.

77.
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.

78.
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.

79.
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.

80.
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.

81.
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.

82.
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.

83.
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.

84.
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.

85.
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.

86.
SAMPAIO, A. C. A.; MEIRA, S. . Especificação Funcional de um Interpretador. In: ERMAC - SBMAC, 1987, Fortaleza. IV ERMAC - SMBAC, 1987.

Resumos expandidos publicados em anais de congressos
1.
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.

Apresentações de Trabalho
1.
Augusto Sampaio. Testing from natural language in an industrial context. 2016. (Apresentação de Trabalho/Conferência ou palestra).

2.
Augusto Sampaio. Refinement Algebra and Applications. 2015. (Apresentação de Trabalho/Conferência ou palestra).

3.
Augusto Sampaio; Giovanny Lucero ; David Naumann . Refinement Algebra for an O-O Language with References. 2015. (Apresentação de Trabalho/Conferência ou palestra).

4.
Augusto Sampaio. Compositional Analysis for Systems of Systems. 2013. (Apresentação de Trabalho/Conferência ou palestra).

5.
Sampaio, Augusto C. A.. Invited Speaker (Workshop COMPASS): The object-oriented formalism OhCircus. 2012. (Apresentação de Trabalho/Conferência ou palestra).

6.
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).

7.
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).

8.
SAMPAIO, A. C. A.. Participação no Painel (SBMF-2008): Formal Methods in Industry. 2008. (Apresentação de Trabalho/Conferência ou palestra).

9.
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).

10.
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).

11.
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).

12.
SAMPAIO, A. C. A.. Invited speaker (IFIP WG2.3): Laws of Object-Oriented Programming. 2005. (Apresentação de Trabalho/Conferência ou palestra).

13.
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).

14.
SAMPAIO, A. C. A.. Invited speaker (Columbia University): An Algebraic Approach to Compiler Design. 1996. (Apresentação de Trabalho/Conferência ou palestra).


Demais tipos de produção técnica
1.
Sampaio, Augusto C. A.. Concurrency in CSP. 2011. (Curso de curta duração ministrado/Outra).

2.
Sampaio, Augusto C. A.. Conceitos e Paradigmas de Programação via Projeto de Interpretadores. 2008. (Curso de curta duração ministrado/Outra).

3.
SAMPAIO, A. C. A.. Transformation Laws for Sequential Object-Oriented Programming. 2006. (Curso de curta duração ministrado/Especialização).

4.
CAVALCANTI, A. ; SAMPAIO, A. C. A. ; WOODCOCK, J. . Refinement Techniques in Software Engineering. 2006. (Editoração/Livro).

5.
SAMPAIO, A. C. A.. Simpósio Brasileiro de Métodos Formais (SBMF) 2005. 2005. (Editoração/Anais).

6.
SAMPAIO, A. C. A.; P. Borba . Transformation Laws for Sequential Object-Oriented Programming. 2004. (Curso de curta duração ministrado/Especialização).

7.
SAMPAIO, A. C. A.. Object-oriented analysis and design. 2001. (Curso de curta duração ministrado/Especialização).

8.
SAMPAIO, A. C. A.. Programming language concepts and paradigms. 2001. (Curso de curta duração ministrado/Especialização).

9.
SAMPAIO, A. C. A.. Simpósio Brasileiro de Métodos Formais (SBES) 2000. 2000. (Editoração/Anais).



Bancas



Participação em bancas de trabalhos de conclusão
Mestrado
1.
Augusto Sampaio. Participação em banca de Sérgio Barza. Model Checking of Requirements Written in Controlled Natural Language. 2016. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.

2.
Augusto Sampaio. Participação em banca de Saulo Medeiros de Araújo. 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.

3.
Marcel Oliveira; Sampaio, Augusto C. A.; Anamaria Moureira. Participação em banca de Madiel de Sousa Conserva Filho. 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.

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

5.
Sampaio, Augusto C. A.; Alexandre Cabral Mota; M. Cornelio. Participação em banca de Adriana Carla Damasceno. 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.

6.
Ana Melo; Leliane Barros; SAMPAIO, A. C. A.. Participação em banca de David Paulo Pereira. 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.

7.
P. Machado; SAMPAIO, A. C. A.; Jorge César Abrantes Figueiredo. Participação em banca de Emanuela Gadelha Cartaxo. 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.

8.
SAMPAIO, A. C. A.; Paulo Masiero; Renata Fortes. Participação em banca de André Dantas Rocha. 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.

9.
SAMPAIO, A. C. A.. Participação em banca de Cristiano Bertolini. 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.

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

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

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

13.
SAMPAIO, A. C. A.; Daniel Schwabe; Alexandre Vasconcelos. Participação em banca de Ricardo André Cavalcante de Souza. 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.

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

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

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

17.
SAMPAIO, A. C. A.; Jair Leite; Alexandre Vasconcelos. Participação em banca de Alessandro Cruvinel Machado de Araújo. 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.

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

19.
SAMPAIO, A. C. A.; Angelo Perkusich; Jorge César Abrantes Figueiredo; Evandro de Barros Costa; José Reinaldo Silva. Participação em banca de Sandro Alex Damasceno Costa. 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.

20.
SAMPAIO, A. C. A.; Francisco Pinheiro; MEIRA, S.. Participação em banca de Denise de Oliveira Dias Neves. 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.

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

22.
SAMPAIO, A. C. A.. Participação em banca de Marum Simão Filho. 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.

23.
SAMPAIO, A. C. A.. Participação em banca de Valéria Cesário Times. 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.

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

Teses de doutorado
1.
Augusto Sampaio. Participação em banca de Henrique Emanuel Mostaert Rebêlo. Contract Modularity in Design By Contract Languages. 2014. Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco.

2.
Augusto Sampaio. Participação em banca de Rodrigo Fraxino de Araujo. 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.

3.
David Deharbe; Anamaria Moureira; Marcel Oliveira; Sampaio, Augusto C. A.; Rohit Gheyi. Participação em banca de Bruno Emerson Gurgel Gomes. Desenvolvimento Formal de Aplicações para Smart Cards. 2012. Tese (Doutorado em Matemática Aplicada e Estatistica) - Universidade Federal do Rio Grande do Norte.

4.
Ana Melo; Flavio Silva; Marie-Claude Gaudel; Sampaio, Augusto C. A.; Jean-pierre Briot. Participação em banca de Paulo Salem da Silva. 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.

5.
P. Machado; T. Massoni; Rohit Gheyi; Sampaio, Augusto C. A.; David Deharbe. Participação em banca de Wilkerson de Lucena Andrade. Symbolic model-based testing for real-time systems. 2011. Tese (Doutorado em Ciência da Computação) - Universidade Federal de Campina Grande.

6.
Sampaio, Augusto C. A.; P. Borba; Iyoda, Juliano; Cristiano Ferraz; Alvaro Moreira. Participação em banca de Cristiano Bertolini. 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.

7.
Sampaio, Augusto C. A.; Alexandre Cabral Mota; Iyoda, Juliano; Ana Melo; Marcel Oliveira. Participação em banca de Tiago Lima Massoni. 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.

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

9.
SAMPAIO, A. C. A.; Claudia Werner; Julio Leite. Participação em banca de Alexandre Luis Correa. 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.

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

11.
SAMPAIO, A. C. A.; Ana Maria de Alencar Price; Paulo Masiero. Participação em banca de Carla Alessandra Lima Reis. 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.

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

13.
SAMPAIO, A. C. A.; Carlos Ferraz; P. Borba; Claudia Werner. Participação em banca de Gledson Elias da Silveira. 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.

14.
SAMPAIO, A. C. A.. Participação em banca de Dalton Dario Serey Guerrero. 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.

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

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

Qualificações de Doutorado
1.
Augusto Sampaio. Participação em banca de André Luís Ribeiro Didier. An Algebra of Temporal Faults. 2016. Exame de qualificação (Doutorando em Ciências da Computação) - Universidade Federal de Pernambuco.

2.
Augusto Sampaio. Participação em banca de Adirana Carla Damasceno. 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.

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

4.
David Deharbe; Anamaria Moureira; Sampaio, Augusto C. A.. Participação em banca de Bruno Emerson Gurgel Gomes. 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.

5.
SAMPAIO, A. C. A.; Ana Melo; MOTA, A.. Participação em banca de Rohit Gheyi. 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.

6.
Sampaio, A.; Alexandre Cabral Mota. Participação em banca de Rohit Gheyi. 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.

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

8.
SAMPAIO, A. C. A.; Guilherme Travassos; Jaelson Castro. Participação em banca de Sérgio Castelo Branco Soares. An Aspect-oriented Implementation Method. 2003. Exame de qualificação (Doutorando em Ciências da Computação) - Universidade Federal de Pernambuco.

9.
Benemar Souza; Antonio Marcus Lima; TURNELL, M. F.; José Reinaldo Silva; SAMPAIO, A. C. A.; Carlos Lucena. Participação em banca de Dalton Dario Serey Guerrero. 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.

10.
SAMPAIO, A. C. A.. Participação em banca de Vanderlei Moraes Rodrigues. 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.

Trabalhos de conclusão de curso de graduação
1.
SAMPAIO, A. C. A.. Participação em banca de Rafael Oliveira Nóbrega.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.

2.
SAMPAIO, A. C. A.. Participação em banca de André Luís Ribeiro Didier.Automatic Z Data Refinement. 2006. Trabalho de Conclusão de Curso (Graduação em Ciencia da Computacao) - Universidade Federal de Pernambuco.

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

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

5.
SAMPAIO, A. C. A.. Participação em banca de Jairson Barbosa Rodrigues.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.

6.
SAMPAIO, A. C. A.. Participação em banca de Sandrelly Luiz Coutinho.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.

7.
SAMPAIO, A. C. A.. Participação em banca de Marcel Vinícius Medeiros Oliveira.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.

8.
SAMPAIO, A. C. A.. Participação em banca de Sérgio Castelo Branco Soares.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.



Participação em bancas de comissões julgadoras
Professor titular
1.
Augusto Sampaio. Comissão para Progressão para Professor Titular. 2015. Universidade Federal de Minas Gerais.

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

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

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

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

4.
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.

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

Avaliação de cursos
1.
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.

Outras participações
1.
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.

2.
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.

3.
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.

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

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



Eventos



Organização de eventos, congressos, exposições e feiras
1.
Augusto Sampaio. Membro do Comitê de Programa do FM2016 - Formal Methods. 2016. (Congresso).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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



Orientações



Orientações e supervisões em andamento
Dissertação de mestrado
1.
Rodrigo Benedito Otoni. Compositional Analysis of Classical Properties of Concurrency. Início: 2016. 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).

Tese de doutorado
1.
Flávia Mérylyn Carneiro Falcão. Compositional Analysis and Design of SysML Models. Início: 2016. Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco. (Orientador).

2.
Joabe Bezerra de Jesus Júnior. Functional Analysis of Systems of Systems. Início: 2012. Tese (Doutorado em Pós-Graduação em Ciência da Computação) - Centro de Informática. (Coorientador).


Orientações e supervisões concluídas
Dissertação de mestrado
1.
Filipe Marques Chaves de Arruda. Capture & Replay with Text-Based Reuse and Framework Agnosticism. 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.

2.
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.

3.
Bruno Cesar 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.

4.
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.

5.
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.

6.
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.

7.
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.

8.
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.

9.
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.

10.
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.

11.
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.

12.
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.

13.
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.

14.
Flavia Merylyn Carneiro Falcao. 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.

15.
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.

16.
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.

17.
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.

18.
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.

19.
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.

20.
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.

21.
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.

22.
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.

23.
Antônio 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.

24.
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.

25.
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.

26.
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.

27.
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.

28.
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.

29.
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.

30.
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.

31.
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.

32.
Erika 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.

33.
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.

34.
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.

35.
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.

Tese de doutorado
1.
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.

2.
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.

3.
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.

4.
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.

5.
Madiel de Sousa Conserva Filho. Local Livelock Analysis of Component-Based Models. 2016. Tese (Doutorado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte, . Coorientador: Augusto Cezar Alves Sampaio.

6.
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.

7.
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.

8.
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.

9.
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.

10.
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.

11.
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.

12.
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.

13.
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.

14.
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.

15.
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.

Supervisão de pós-doutorado
1.
Giovanny Lucero Palma. 2016. Universidade Federal de Pernambuco, . Augusto Cezar Alves Sampaio.

2.
Leila Maciel de Almeida e Silva. 2015. Universidade Federal de Pernambuco, . Augusto Cezar Alves Sampaio.

3.
Marcel Vinícius Medeiros Oliveira. 2012. Centro de Informática, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior. Augusto Cezar Alves Sampaio.

4.
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.

5.
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.

Monografia de conclusão de curso de aperfeiçoamento/especialização
1.
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.

2.
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.

3.
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.

4.
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.

5.
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.

6.
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.

7.
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.

8.
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.

9.
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.

10.
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.

11.
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.

12.
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.

13.
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.

14.
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.

15.
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.

16.
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.

17.
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.

18.
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.

Trabalho de conclusão de curso de graduação
1.
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.

2.
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.

3.
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.

4.
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.

5.
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.

6.
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.

7.
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.

8.
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.

9.
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.

10.
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.

11.
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.

12.
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.

13.
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.

14.
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.

15.
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.

16.
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.

17.
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.

18.
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.

19.
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.

20.
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.

21.
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.

22.
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.

23.
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.

24.
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.

Iniciação científica
1.
Hugo Leonardo da Silva Araújo. 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.

2.
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.

3.
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.

4.
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.

5.
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.

6.
Leonardo Freire de Andrade. Á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.

7.
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.

Orientações de outra natureza
1.
Juan Perna. Correct hardware synthesis. 2009. Orientação de outra natureza. (Ciencia da Computacao) - Universidade Federal de Pernambuco. Orientador: Augusto Cezar Alves Sampaio.



Inovação



Projetos de pesquisa


Educação e Popularização de C & T



Apresentações de Trabalho
1.
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).

2.
Sampaio, Augusto C. A.. Invited Speaker (Workshop COMPASS): The object-oriented formalism OhCircus. 2012. (Apresentação de Trabalho/Conferência ou palestra).


Cursos de curta duração ministrados
1.
Sampaio, Augusto C. A.. Concurrency in CSP. 2011. (Curso de curta duração ministrado/Outra).




Página gerada pelo Sistema Currículo Lattes em 14/12/2018 às 22:57:42