Programa de Pós Graduação em Ciência da Computação

Ana Cristina Vieira de Melo

Possui graduação em Bacharelado Em Ciência da Computação pela Universidade Federal de Pernambuco(1986), mestrado em Ciências da Computação pela Universidade Federal de Pernambuco(1989), doutorado em Phd In Computer Science pela The University Of Manchester(1995) e pós-doutorado pela University of Oxford(2009). Atualmente é Professor Associado da Universidade de São Paulo, Consultor Ad-hoc do Conselho Nacional de Desenvolvimento Científico e Tecnológico, Revisor de projeto de fomento do Conselho Nacional de Desenvolvimento Científico e Tecnológico, Consultor Ad-hoc do Coordenação de Aperfeiçoamento de Pessoal de Nível Superior, Revisor de projeto de fomento do Coordenação de Aperfeiçoamento de Pessoal de Nível Superior, Consultor Ad-hoc do Fundação de Amparo à Pesquisa do Estado de São Paulo, Revisor de projeto de fomento do Fundação de Amparo à Pesquisa do Estado de São Paulo, Revisor de periódico da Journal of the Brazilian Computer Society (0104-6500), Revisor de periódico da Formal Aspects of Computing, Revisor de periódico da International Journal of Software Engineering and Knowledge Engineering, Membro - Comissão Especial de Métodos Formais da Sociedade Brasileira de Computação, Revisor de periódico da Theoretical Computer Science, Revisor de periódico da Science of Computer Programming, Revisor de periódico da Information Sciences, Revisor de periódico da IET Software (Print), Revisor de periódico da The Journal of Systems and Software e Revisor de periódico da Computer Standards & Interfaces. Tem experiência na área de Ciência da Computação, com ênfase em Teoria da Computação. Atuando principalmente nos seguintes temas:reuse, Formal Methods, Process Algebras, Formal Verification, Bisimulation. (Texto gerado automaticamente pela aplicação CVLattes)

  • http://lattes.cnpq.br/1225623517319669 (22/08/2023)
  • Rótulo/Grupo:
  • Bolsa CNPq:
  • Período de análise:
  • Endereço: Universidade de São Paulo, Instituto de Matemática e Estatística, Departamento de Ciência da Computação. Rua do Matão, 1010 Cidade Universitária 05508090 - Sao Paulo, SP - Brasil Telefone: (11) 30919689 Fax: (11) 30916134
  • Grande área: Ciências Exatas e da Terra
  • Área: Ciência da Computação
  • Citações: Google Acadêmico

Produção bibliográfica

Produção técnica

Produção artística

Orientações em andamento

Supervisões e orientações concluídas

Projetos de pesquisa

Prêmios e títulos

Participação em eventos

Organização de eventos

Lista de colaborações

Produção bibliográfica

Produção técnica

Produção artística

Orientações em andamento

Supervisões e orientações concluídas

Projetos de pesquisa

  • Total de projetos de pesquisa (15)
    1. 2023-Atual. Centro de Pesquisa Aplicada em Inteligência Artificial para a Evolução das Indústrias para o Padrão 4.0
      Descrição: Processo Fapesp:20/09850-0Platafroma IASMIN (Inteligência Artificial Soluções para Manufatura Inteligente)Pesquisador Associado dentro da linha de pesquisa: Interoperabilidade e Integração da CadeiaInstituição SedeInstituto de Pesquisas Tecnológicas do Estado de São Paulo S/A (IPT) Empresas ParceirasSiemens LtdaSiemens Infraestrutura E Indústria LtdaRobert Bosch LimitadaKlabin S.AFCA Fiat Chrysler Automoveis Brasil LtdaBraskem S.A Instituições ParceirasAssociação Parque Tecnológico de São José dos Campos/APQTEC/APQTECCentro Universitário FACENS/UNIFACENS/ACRTSEscola Politécnica/EP/USPInstituto de Matemática e Estatística/IME/USPFundação Parque Tecnológico Itaipu - Brasil/FPTI-BR/FPTI-BRInstituto de Ciência e Tecnologia de Sorocaba/ICTS/UNESPInstituto Tecnológico de Aeronáutica/ITAUniversidade Técnica Federal do Paraná - UTFPRUniversidade Federal de São Paulo/UNIFESPUniversidade Federal do ABC/UFABCAgência Unesp de Inovação/AUIN/UNESPUniversidade Estadual de Campinas / UNICAMP. Situação: Em andamento; Natureza: Pesquisa. Integrantes: Ana Cristina Vieira de Melo - Coordenador / Flávio Soares Correa da Silva - Integrante / Jefferson de Oliveira Gomes - Integrante.
      Membro: Ana Cristina Vieira de Melo.
    2. 2020-Atual. Programming with Monoidal Profunctors and Semiarrows
      Descrição: Cooperação em projeto de pesquisa -Prof. Mauro Javier Jaskelioff e Alexandre Garcia de OliveiraUniversidad Nacional de Rosario- Argentina. Situação: Em andamento; Natureza: Pesquisa. Alunos envolvidos: Doutorado: (1) . Integrantes: Ana Cristina Vieira de Melo - Coordenador / Alexandre Garcia de Oliveira - Integrante / Mauro Javier Jaskelioff - Integrante.
      Membro: Ana Cristina Vieira de Melo.
    3. 2014-2015. Generation of Java PathFinder Properties from Test Purposes (FAPESP: 2013/22317-6)
      Descrição: This Research Internship Abroad (BEPE) project is part of the Ph.D work under the São Paulo Research Foundation (FAPESP) process: 2011/01928-1. The main objective of the Ph.D work is to help software developers in applying formal verification in practice. To do this, we propose an approach that generates the corresponding source code of the system properties that should be verified to assure the software quality. This code generation will be guided by the test purposes derived from the system specification. The main challenge of the Ph.D research is to synchronize the test purposes at implementation and specification levels in order to automate the properties code generation. To solve this problem, we have decided to make a theoretical work over this synchronization and then apply its results in practice using the Java PathFinder (JPF), a virtual machine that can be used as a model checker to verify Java programs. In this BEPE project, we will focus on the application of the theoretical results in practice: we are going to proceed to the implementation of general properties templates in JPF. These templates will be used to automate the generation of properties code that a system must satisfy to guarantee its quality. And the generated property code will be registered in JPF so that it will be able to check whether the system satisfies this property or not. To validate the implementation of those JPF general properties templates, a set of tests for each property template must be created and executed.. Situação: Concluído; Natureza: Pesquisa. Alunos envolvidos: Doutorado: (1) . Integrantes: Ana Cristina Vieira de Melo - Coordenador / Simone Hanazumi - Integrante / Corina Pasareanu - Integrante. Financiador(es): Fundação de Amparo à Pesquisa do Estado de São Paulo - Bolsa.
      Membro: Ana Cristina Vieira de Melo.
    4. 2013-Atual. VVTrans - um Método para Teste e Verificação Formal Transversal ao Desenvolvimento de Sistemas Críticos (FAPESP: 2012/23767-2)
      Descrição: Para que haja uma garantia de que o software desenvolvido é confiável, atividades de testes e verificação formal devem ser realizadas. Contudo, a viabilidade prática de execução dessas atividades depende de métodos de desenvolvimento que explorem o uso conjunto das técnicas, bem como de ferramentas que auxiliem sua realização, uma vez que a execução de ambas constitui um alto custo para o desenvolvimento do software. Tendo em vista a necessidade de facilitar a realização de testes e verificação formal nos sistemas de software de missão crítica, este projeto se propõe a desenvolver uma metodologia integrada, com apoio de ferramentas computacionais, para a verificação formal e testes desses sistemas, levando em conta a redução dos custos das atividades de Verificação & Validação (V&V). Os principais objetos de estudo que constituem um desafio científico ao projeto é a exploração da complementariedade das duas atividades de forma transversal ao desenvolvimento de sistemas críticos para possibilitar o uso conjunto dessas atividades e avaliar o custo de sua aplicação.. Situação: Em andamento; Natureza: Pesquisa. Alunos envolvidos: Graduação: (3) / Mestrado acadêmico: (3) / Doutorado: (3) . Integrantes: Ana Cristina Vieira de Melo - Coordenador / Nandamudi Lankalapalli Vijaykumar - Integrante / Valdivino Alexandre de Santiago Júnior - Integrante. Financiador(es): Fundação de Amparo à Pesquisa do Estado de São Paulo - Auxílio financeiro.
      Membro: Ana Cristina Vieira de Melo.
    5. 2011-2015. Geração de Propriedades sobre Programas Java a partir de Casos de Teste
      Descrição: Com a presença cada vez maior de sistemas computacionais e novas tecnologias no cotidiano das pessoas, garantir que eles não falhem e funcionem corretamente tornou-se algo de extrema importância. Além de indicar a qualidade do sistema, assegurar seu bom funcionamento é essencial para se evitar perdas, desde financeiras até de vidas. Uma das técnicas utilizadas para esta finalidade é a chamada verificação formal de programas. A partir da especificação do sistema, descrita numa linguagem formal, são definidas propriedades a serem satisfeitas e que certificariam a qualidade do software. Estas propriedades devem então ser implementadas para uso num verificador, que é a ferramenta responsável por executar a verificação e informar quais propriedades foram satisfeitas e quais não foram, indicando aos desenvolvedores os possíveis locais com código incorreto no sistema. A desvantagem do uso da verificação formal é, além do seu alto custo, a necessidade de haver pessoas com treinamento em linguagens e métodos formais. Ademais, a implementação de propriedades relativas a um sistema em particular para uso num verificador é uma tarefa bastante complexa e de alto custo. Para auxiliar os desenvolvedores na utilização da verificação formal em programas escritos em Java, este trabalho propõe a geração de código de propriedades para uso direto no verificador, a partir de casos de testes derivados dos requisitos formais de sistemas.. Situação: Concluído; Natureza: Pesquisa. Alunos envolvidos: Doutorado: (1) . Integrantes: Ana Cristina Vieira de Melo - Coordenador / Simone Hanazumi - Integrante. Financiador(es): Fundação de Amparo à Pesquisa do Estado de São Paulo - Bolsa.
      Membro: Ana Cristina Vieira de Melo.
    6. 2010-2015. Convênio Acadêmico Internacional - Engenharia de Software e Métodos Formais
      Descrição: Este convênio tem como objeto a cooperação acadêmica através do intercâmbio de docentes e pesquisadores, bem como de estudantes de pós-graduação entre o grupo de Engenharia de Software e Métodos Formais da USP (São Paulo) e o Laboratoire de Recherche en Informatique (LRI) da Université Paris-Sud 11. A colaboração proposta tem como objetivo principal o desenvolvimento conjunto de pesquisas científicas em tópicos relacionados ao desenvolvimento formal de sistemas de software, dentre os quais teste e verificação formal de sistemas. Dentro desta área de pesquisa, em particular, definimos como projeto inicial: ?Verificação de sistemas distribuídos e móveis orientado por informação de simulação e escolha estatística de testes?. No âmbito deste projeto, o grupo de Engenharia de Software e Métodos Formais da USP (São Paulo) tem desenvolvido técnicas de verificação e simulação de sistemas distribuídos e móveis, enquanto o Laboratoire de Recherche en Informatique (LRI) da Université Paris-Sud 11 tem aplicado métodos estatísticos para a escolha de conjuntos de testes relevantes. Desta forma, a colaboração propiciará o desenvolvimento de métodos estatísticos para a escolha de informação de simulação dos sistemas distribuídos e móveis que sejam relevantes à verificação de propriedades sobre tais sistemas. (Proc. 08.1.01153.45.4). Situação: Em andamento; Natureza: Pesquisa. Alunos envolvidos: Doutorado: (1) . Integrantes: Ana Cristina Vieira de Melo - Coordenador / Marie-Claude Gaudel - Integrante. Financiador(es): Université Paris-Sud XI - Cooperação / Universidade de São Paulo - Cooperação. Número de produções C, T & A: 3
      Membro: Ana Cristina Vieira de Melo.
    7. 2010-2011. Avaliação da Usabilidade de Sistemas Web
      Descrição: A cada dia a internet vem sendo mais utilizada pelas empresas para divulgar seus produtos, conhecer melhor ou conquistar mais clientes. Com o surgimento da WEB 2.0 bem como a facilidade de acesso a banda larga, cada vez mais usuários colaboram gerando conteúdo na web. O sucesso de um projeto web depende muito da aceitação dos usuários que o utilizam. Métodos de avaliação de usabilidade têm sido empregados para garantir uma boa qualidade desses produtos. Esse trabalho de pesquisa propõe um estudo e comparação dos métodos para avaliação de usabilidade para a WEB 2.0.. Situação: Concluído; Natureza: Pesquisa. Alunos envolvidos: Doutorado: (1) . Integrantes: Ana Cristina Vieira de Melo - Coordenador / Hamilton Fernandes de Moraes Junior - Integrante. Financiador(es): Serasa-Experian Fundação de Apoio à Pesquisa - Bolsa.
      Membro: Ana Cristina Vieira de Melo.
    8. 2009-2011. A methodology and related technology for multi-agent simulation
      Descrição: Multi-agent systems are useful to model complex systems in which the entities to be studied can be decomposed into several interacting pieces called agents. Human societies, computer networks, neural tissue and cell biology are examples of systems that can be seen from this perspective. There are a number of ways that such modelling can be done, ranging from purely formal approaches to entirely experimental ones. Our work, which is situated between these two extremes, focuses on employing simulation in order to study such multi-agent models. That is, we specify the agents as computer programs and run interesting scenarios in a simulator, hoping to learn something about the model after several simulations. As one would expect, simple simulation approaches of this kind are already in use nowadays. However, they are also rather naive with respect to automated analysis of simulation results. Typically, one merely runs the simulation several times and collect statistics about some variables. Clearly, though, as the simulation runs in a computer and is specified as a program, it must be possible to perform many kinds of automated analyses beyond such simple statistics compilation. Our work, thus, focuses on this issue: what kind of algorithms, theories and software infrastructure are required in order to have a simulator capable of helping an experimenter discover useful information about a simulation model. We believe that many ideas and techniques from the Formal Methods and Software Testing communities can be successfully adapted to this context. The crucial insight here is that simulations can be seen as incomplete explorations of state-spaces, and as such we can hope, for example, to apply approximate versions of Model Checking and other techniques of automated reasoning. To fulfill this vision, we intend to develop both the necessary theory and its implementation as a simulator. We expect, thus, to create a technology that can signific. Situação: Concluído; Natureza: Pesquisa. Alunos envolvidos: Doutorado: (1) . Integrantes: Ana Cristina Vieira de Melo - Coordenador / Paulo Salem da Silva - Integrante / Marie-Claude Gaudel - Integrante. Financiador(es): Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - Bolsa. Número de produções C, T & A: 1
      Membro: Ana Cristina Vieira de Melo.
    9. 2009-2010. Web Services confiáveis - Um estudo sobre os problemas atuais
      Descrição: Aplicativos Web Services oferecem serviços através de uma rede e são cada vez mais utilizados para integrarem sistemas e soluções das mais variadas complexidades. Os Web Services estão sendo cada vez mais usados em sistemas altamente complexos, principalmente com a chegada da web 2.0. Em alguns cenários com maior criticidade, a confiança no Web Service passa a ser um fator de fundamental importância. Atualmente, uma das suas principais características é o fato de que sua comunicação é feita em um ambiente com baixa confiabilidade, como a Internet, cujos protocolos de comunicação nem sempre provêm as garantias necessárias de funcionamento correto. De fato, isso é uma barreira que impede que empresas invistam em aplicativos críticos que dependam de integração com Web services. Com o objetivo de garantir um serviço de qualidade, a comunidade acadêmica e até mesmo a indústria têm despendido um grande esforço para definir modelos de Qualidade de Serviço especificamente para Web Services, e estudar alternativas para o problema de forma a aumentar a confiabilidade nos serviços oferecidos por eles. Estudar a fundo uma possível solução requer conhecimento sobre as diversas alternativas já pesquisadas e sobre as tendências tecnológicas que prometem ajudar a suprir as atuais necessidades. Assim, a proposta do presente estudo é analisar os principais problemas relacionados à confiabilidade de Web Services, com o objetivo de obter as informações necessárias para prover subsídios de como implementar soluções adequadas a situações específicas. Além disso, o estudo pode servir como referência para que sejam pesquisadas novas soluções.. Situação: Em andamento; Natureza: Pesquisa. Alunos envolvidos: Mestrado acadêmico: (1) . Integrantes: Ana Cristina Vieira de Melo - Coordenador / Paulo Roberto de Araújo França Nunes - Integrante. Financiador(es): Serasa-Experian Fundação de Apoio à Pesquisa - Bolsa. Número de produções C, T & A: 1
      Membro: Ana Cristina Vieira de Melo.
    10. 2008-2010. Ambiente Integrado para Verificação e Teste da Coordenação de Componentes Tolerantes a Falhas
      Descrição: Com o crescimento e popularização do mercado de componentes, muitos fornecedores de software têm se especializado no desenvolvimento e comercialização de componentes que atendam às necessidades específicas dos desenvolvedores de sistemas. Estes componentes são mais conhecidos como Commercial-Off-The-Shelf . Entretanto, a montagem de sistemas corporativos que sejam confiáveis e tolerantes a falhas, a partir da integração de componentes comerciais, tem-se mostrado uma atividade relativamente complexa. Garantir que esta integração não falhe passou a ser algo imprescindível. Com o objetivo de definir quais requisitos são necessários para estabelecer um bom teste do software, definem-se os critérios de teste. Mesmo considerando o direcionamento da escolha de conjuntos de testes a serem realizados a partir dos critérios, tais conjuntos são, na sua maioria, ainda muito complexos. Uma outra abordagem para garantir o funcionamento do software como inicialmente especificado, são as técnicas de verificação formal de programas, as quais garantem que os programas funcionam de acordo com a especificação ou atendem a um conjunto de propriedades relevantes. A viabilidade prática de testes de software depende de mecanismos e ferramentas que auxiliem esta atividade, de forma a automatizar a geração de casos e dados de testes a serem aplicados. Por outro lado, a aplicação prática de verificadores formais em linguagens de programação depende da predefinição de propriedades, já que os "desenvolvedores" de software, em geral, não possuem treinamento adequado para definir novas propriedades. Além disso, faz-se necessário o uso conjunto de ferramentas de ambas as atividades para que sejam exploradas suas complementariedades. Este projeto de Mestrado se propõe a desenvolver um ambiente integrado para a verificação e teste de protocolos para a coordenação do comportamento execepcional de componentes.. Situação: Em andamento; Natureza: Pesquisa. Alunos envolvidos: Mestrado acadêmico: (1) . Integrantes: Ana Cristina Vieira de Melo - Coordenador / Simone Hanazumi - Integrante. Financiador(es): Fundação de Amparo à Pesquisa do Estado de São Paulo - Bolsa. Número de produções C, T & A: 1
      Membro: Ana Cristina Vieira de Melo.
    11. 2008-2009. Construção de Componentes Concorrentes na Abordagem de Desenvolvimento Baseado em Modelos Formais
      Descrição: Component-based software is one of the reuse approaches successfully used. The task of developing software components can be seen from two different perspectives. One that would take care of building components useful in many different situations, and another that would develop the final software using these reusable components. Naturally, technology alone does not guarantee the creation of reusable components. Truly component-oriented approaches require methods that can define what kind of entities the components must represent, how they are composed and how such compositions are to be employed. Having all this together to end up with a set of components easily built and that can be reused in an appropriate way is not very straightforward. To make components construction more cost-effective and of a better quality, the model-driven development can be adopted. In this case, a design model language is required for components design, together with a code generation mechanism. Booster is a design language developed at the University of Oxford (UK) for components construction via code generation. It is an object-oriented language based on formal methods, namely B and Z, that is actually able to generate components under the contexts of sequential composition. In practice, however, component-based software naturally encompass contexts in which components are concurrently composed instead of purely sequential. This project is about a study on how to improve the model-driven components development with concurrent composition. From a theoretical point-of-view, a study on the abstraction level for specifying, through formal means, the required and provided interfaces of components must be carried on to end up with a model from which programs code can be generated. Also, mechanisms for components orchestration in the context of concurrent composition must be developed in order to provide an architecture and a corresponding protocol to coordi. Situação: Concluído; Natureza: Pesquisa. Integrantes: Ana Cristina Vieira de Melo - Coordenador / Jim Davies - Integrante. Financiador(es): Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - Bolsa.
      Membro: Ana Cristina Vieira de Melo.
    12. 2007-2009. Formalização da Orquestração de Componentes Tolerantes a Falhas
      Descrição: Com a popularização das redes de computadores e dos gerenciadores de banco de dados, os sistemas de informação tornaram-se elementos essenciais de suporte a processos de negócio de empresas fornecedoras de serviços indispensáveis à sociedade, tais como automação bancária e telefonia. Esses sistemas modernos são também considerados de missão crítica pois qualquer falha pode provocar, além de prejuízos financeiros, desgastes na imagem e reputação da empresa envolvida. A utilização de componentes na estruturação desses sistemas promove maior qualidade, confiabilidade e flexibilidade ao produto e agiliza o processo de desenvolvimento. Entretanto, para que estes benefícios sejam totalmente observados, é fundamental que os provedores de componentes projetem-nos com especificações precisas, completas e consistentes. Uma estratégia para a especificação de componentes tolerantes a falhas é informar a ocorrência de erros através de exceções e realizar a recuperação dos mesmos por rotinas de tratamento correspondentes. Contudo, o uso de notações precisas para representar os componentes tolerantes a falhas contribuem mas não são o suficiente para obtermos sistemas confiáveis. A falta de mecanismos adequados para a integração de componentes pode gerar comportamentos inesperados em sistemas construídos a partir da composição de componentes. Da mesma forma, a integração dos comportamentos referentes ao tratamento de falhas dos componentes também podem proporcionar comportamentos inesperados se não forem coordenados adequadamente. Este projeto tem como objetivo principal aprofundar os estudos e desenvolver mecanismos para a integração adequada (através de métodos formais) de componentes, tanto para o comportamento normal quanto para o associado ao tratamento de falhas. CNPq - Edital MCT/CNPq/CT-INFO no 07/2007 (Proc. 551038/2007-1). Situação: Em andamento; Natureza: Pesquisa. Alunos envolvidos: Mestrado acadêmico: (3) Doutorado: (3) . Integrantes: Ana Cristina Vieira de Melo - Coordenador. Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro.
      Membro: Ana Cristina Vieira de Melo.
    13. 2005-2007. Um Método de Desenvolvimento e Testes para Sistemas Baseados em Componentes com Tratamento de Exceções
      Descrição: A disseminação de sistemas computacionais em atividades críticas tornou a confiabilidade uma característica indispensável a esses sistemas. Essa confiabilidade é obtida através de técnicas de tolerância a falhas, que aumentam a complexidade do desenvolvimento. Para auxiliar a construção de sistemas tolerantes a falhas, esse projeto de pesquisa propõe um método de desenvolvimento baseado em componentes que guiará tanto as fases de desenvolvimento quanto os testes, paralelizando essas atividades. Número FAPESP: 04/10663-8. Situação: Concluído; Natureza: Pesquisa. Alunos envolvidos: Graduação: (0) / Especialização: (0) / Mestrado acadêmico: (0) / Mestrado profissional: (0) / Doutorado: (0) . Integrantes: Ana Cristina Vieira de Melo - Integrante / Eliane Martins - Integrante / Cecília M F Rubira - Coordenador. Financiador(es): Fundação de Amparo à Pesquisa do Estado de São Paulo - Auxílio financeiro.
      Membro: Ana Cristina Vieira de Melo.
    14. 2003-2005. CCC-AHIA Cooperação e Compartilhamento de Conhecimento entre Agentes Heterogêneos Inteligentes e Autônomos
      Descrição: Estudo sobre cooperação entre agentes autônomos híbridos.. Situação: Em andamento; Natureza: Pesquisa. Alunos envolvidos: Graduação: (0) / Especialização: (0) / Mestrado acadêmico: (0) / Mestrado profissional: (0) / Doutorado: (0) . Integrantes: Ana Cristina Vieira de Melo - Integrante / Flávio Soares Correa da Silva - Coordenador / Leliane Barros - Integrante / Renata Wasserman - Integrante / Marcelo Finger - Integrante. Financiador(es): Fundação de Amparo à Pesquisa do Estado de São Paulo - Auxílio financeiro.
      Membro: Ana Cristina Vieira de Melo.
    15. 2002-2006. CooPiTools - Cooperation among Pi-calculus Tools
      Descrição: Pi-calculus é uma das teorias pioneiras sobre agentes móveis. Além do esforço na construção das teorias, foram desenvolvidas também ferramentas de suporte ao uso das mesmas. Existem atualmente algumas ferramentas para verificação formal de processos concorrentes e agentes móveis, tanto para pi-calculus quanto para algumas outras teorias. Cada uma dessas ferramentas fornece serviços específicos para os quais elas foram concebidas. Algumas verificam se um dado modelo concorrente preserva algumas propriedades, enquanto outras verificam a equivalência entre modelos distintos. Apesar de todos os esforços, vários desafios ainda persistem na construção de ferramentas: o desenvolvimento de técnicas eficientes para a verificação de agentes móveis, construir ferramentas de suporte à especificação e verificação que sejam de fácil uso por usuários comuns, diminuição do esforço na construção de ferramentas e desenvolvimento de novas técnicas que abranjam classes de problemas não tratados atualmente. Considerando a diminuição do esforço de construção de novas ferramentas, um dos objetivos atuais na área de verificação formal é o compartilhamento de serviços entre ferramentas distintas através da sua integração. Este projeto de pesquisa tem como objetivo a integração das ferramentas de verificação para agentes móveis descritos em pi-calculus. Dessa forma, não há a necessidade de reimplementar todos os serviços requisitados em um único verificador, mas estabelecer comunicação entre verificadores capazes de fornecer os requisitos desejados.. Situação: Concluído; Natureza: Pesquisa. Alunos envolvidos: Graduação: (1) / Especialização: (0) / Mestrado acadêmico: (3) / Mestrado profissional: (0) / Doutorado: (0) . Integrantes: Ana Cristina Vieira de Melo - Coordenador. Número de produções C, T & A: 3
      Membro: Ana Cristina Vieira de Melo.

Prêmios e títulos

  • Total de prêmios e títulos (2)
    1. Jabuti 2007 - 1o. Lugar: Melhor Livro de Ciências Exatas, Tecnologia e Informática (Livro: Lógica para computação), CBL - Câmara Brasileira do Livro.. 2007.
      Membro: Ana Cristina Vieira de Melo.
    2. Jabuti 2004 - Indicado entre os 10 Melhores Livros de Ciências Exatas, Tecnologia e Informática (Livro: Princípios de Linguagens de Programação), CBL - Câmara Brasileira do Livro.. 2004.
      Membro: Ana Cristina Vieira de Melo.

Participação em eventos

  • Total de participação em eventos (31)
    1. SEFM. On the Testability of Properties Patterns. 2015. (Congresso).
    2. COMPSAC. Testing Java Exceptions: an instrumentation technique.. 2014. (Congresso).
    3. VVTransv Project Workshop.Overview of the VVTransv Project. 2014. (Oficina).
    4. SBMF 2013 - Brazilian Symposium on Formal Methods. 2013. (Simpósio).
    5. SBMF 2011 - Brazilian Symposium on Formal Methods.PiStache: Implementing π-Calculus in Scala. 2011. (Simpósio).
    6. 22nd IFIP International Conference on Testing Software and Systems. 2010. (Congresso).
    7. Microsoft Research - Latin American Faculty Summit. 2010. (Congresso).
    8. SBMF 2010 - Brazilian Symposium on Formal Methods.A Formal Environment Model for Multi-Agent Systems. 2010. (Simpósio).
    9. FMWeek - 21st IFIP Int. Conference on Testing of Communicating Systems. OConGraX - automatically generating data-flow test cases for fault-tolerant systems. 2009. (Congresso).
    10. 23rd Annual ACM Symposium on Applied Computing. A formal architectural model for exception handling coordination. 2008. (Congresso).
    11. SBMF 2008 - Brazilian Symposium on Formal Methods.SBMF 2008 - Brazilian Symposium on Formal Methods. 2008. (Simpósio).
    12. SEFM 2008 - Software Engineering and Formal Methods. Using Formal Verification to Reduce Test Space of Fault-Tolerant Programs. 2008. (Congresso).
    13. Latin American Faculty Summit.Latin American Faculty Summit. 2007. (Encontro).
    14. Microsoft Faculty Summit. 2007. (Encontro).
    15. Brazilian Symposium on Formal Methods.Ensino de Métodos Formais. 2006. (Simpósio).
    16. Brazilian Symposium on Formal Methods.A Simulation-Oriented Formalization for the Psychological Theory of B. F. Skinner. 2006. (Simpósio).
    17. ICGT 2006 International Conference on Graph Transformation. 2006. (Congresso).
    18. Brazilian Symposium on Formal Methods. 2005. (Simpósio).
    19. Microsoft Research Academic Summit. 2005. (Congresso).
    20. 4th annual Computing Curriculum Workshop 2004. 4th annual Computing Curriculum Workshop 2004. 2004. (Congresso).
    21. Brazilian Symposium on Formal Methods.Brazilian Symposium on Formal Methods. 2004. (Simpósio).
    22. Microsoft TechEd 2004. Microsoft TechEd 2004. 2004. (Congresso).
    23. School on Software Engineering.School on Software Engineering. 2004. (Outra).
    24. IDS 2003 - Jornadas Latinoamericanas de Ingeniería y Desarrollo de Software.IDS 2003 - Primeras Jornadas Latinoamericanas de Ingeniería y Desarrollo de Software: Teoría y Aplicaciones. 2003. (Simpósio).
    25. VI Workshop on Formal Methods.VI Workshop on Formal Methods. 2003. (Simpósio).
    26. IV Workshop de Métodos Formais.IV Workshop de Métodos Formais. 2001. (Simpósio).
    27. Workshop of DECAF-KB.Encontro de projeto - DECaFf-KB. 2001. (Encontro).
    28. XV SBES.XV SBES - Simpósio Brasileiro de Engenharia de Software. 2001. (Simpósio).
    29. III Workshop de Métodos Formais.III Workshop de Métodos Formais. 2000. (Simpósio).
    30. WorkSidam- Workkshop de Sistemas de Informação Distribuída de Agentes Móveis.WorkSidam- Workkshop de Sistemas de Informação Distribuída de Agentes Móveis. 2000. (Encontro).
    31. XIV SBES.XIV SBES - Simpósio Brasileiro de Engenharia de Software. 2000. (Simpósio).

Organização de eventos

  • Total de organização de eventos (6)
    1. de Melo, Ana C. V.; HANAZUMI, S. ; SILVA, L. K. ; Martins, Alexandre Locci. SBMF. 2019. Congresso
    2. MELO, Ana C. V. de; SANTIAGO JUNIOR, V. A.. VVTransv Project Workshop (FAPESP). 2014. Outro
    3. MELO, Ana C. V. de. SBMF 2011 - Brazilian Symposium on Formal Methods. 2011. (Congresso).. . 0.
    4. MELO, Ana C. V. de; Moreira, Alvaro ; Lucília Camarão ; Eliane Pimentel. SBMF 2007 - Brazilian Symposium on Formal Methods. 2007. Congresso
    5. MELO, Ana C. V. de; HAEUSLER, e H. IV Workshop de Métodos Formais. 2001. Congresso
    6. MELO, Ana C. V. de; OKUDA, Kunio ; ENDLER, Markus ; FINGER, Marcelo ; SONG, Siang. WorkSIDAM - I Workshop de Sistemas de Informação Distribuída de Agentes Móveis. 2000. Congresso

Lista de colaborações

  • Colaborações endôgenas (2)
    • Ana Cristina Vieira de Melo ⇔ Flavio Soares Correa da Silva (5.0)
      1. CORREA DA SILVA, F. S.; VASCONCELOS, W. W. ; ROBERTSON, D. S. ; BRILHANTE, V. ; MELO, Ana Cristina Vieira de ; FINGER, Marcelo ; AGUSTI, J.. On the insufficiency of ontologies: problems in knowledge sharing and alternative solutions. Knowledge-Based Systems. v. 15, n. 3, p. 147-167, 2002. Qualis: A1
      2. MELO, Ana Cristina Vieira de ; CORREA DA SILVA, F. S.. Princípios de Linguagens de Programação. 1 ed. São Paulo: Edgard Blucher, 2003. v. 1, p. 212.
      3. SILVA, Flávio Soares Corrêa da ; MENESES, Eudênia X ; MELO, Ana C. V. de. Capabilities in Formal Knowledge Coordination for Business Integration. Em: 17th Annual ACM Conference on Object-oriented Programming, 2002.Qualis: Não identificado (17th Annual ACM Conference on Object-oriented Programming)
      4. CORREA DA SILVA, F. S.; ROBERTSON, D. S. ; AGUSTI, J. ; VASCONCELOS, W. W. ; MELO, Ana Cristina Vieira de. A Lightweight Capability Communication Mechanism. Em: International Conference on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems, v. 1821, p. 660-670, 2000.Qualis: A1 (ENGINEERING APPLICATIONS OF ARTIFICIAL INTELLIGENCE)
      5. CORREA DA SILVA, F. S.; MELO, Ana Cristina Vieira de ; CARNEIRO, M. R. F.. Comunicação entre Computadores e Tecnologias de Redes. São Paulo: Thomson Pioneira. 2002. Tradução/Livro

    • Ana Cristina Vieira de Melo ⇔ Marcelo Finger (1.0)
      1. CORREA DA SILVA, F. S.; VASCONCELOS, W. W. ; ROBERTSON, D. S. ; BRILHANTE, V. ; MELO, Ana Cristina Vieira de ; FINGER, Marcelo ; AGUSTI, J.. On the insufficiency of ontologies: problems in knowledge sharing and alternative solutions. Knowledge-Based Systems. v. 15, n. 3, p. 147-167, 2002. Qualis: A1




(*) Relatório criado com produções desde 2000 até 2024
Data de processamento: 05/12/2024 01:15:21