Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2012. / Submitted by Albânia Cézar de Melo (albania@bce.unb.br) on 2012-10-18T16:28:45Z No. of bitstreams: 1 2012_JoaoPauloCarvalhoColuQueiroz.pdf: 949010 bytes, checksum: 6c8c52f3b39f58d84a5780716ea83b12 (MD5) / Approved for entry into archive by Guimaraes Jacqueline(jacqueline.guimaraes@bce.unb.br) on 2012-10-24T11:08:41Z (GMT) No. of bitstreams: 1 2012_JoaoPauloCarvalhoColuQueiroz.pdf: 949010 bytes, checksum: 6c8c52f3b39f58d84a5780716ea83b12 (MD5) / Made available in DSpace on 2012-10-24T11:08:41Z (GMT). No. of bitstreams: 1 2012_JoaoPauloCarvalhoColuQueiroz.pdf: 949010 bytes, checksum: 6c8c52f3b39f58d84a5780716ea83b12 (MD5) / Este trabalho apresenta um estudo de metodologias para veri cação formal de aplicativos desenvolvidos em linguagens imperativas, em especial, na linguagem Java. Os formalismos teóricos mostrados incluem a Lógica de Hoare, usada para representar pro- priedades de aplicações imperativas, e construções da linguagem de especi cação JML (baseada na Lógica de Hoare), usada para especi car o comportamento esperado de apli- cações codi cadas em Java. As ferramentas mostradas são o sistema Krakatoa, usado para converter especi cações JML em obrigações de prova, e o ambiente interativo de provas Coq, usado para veri car obrigações de prova. Finalmente, exibe-se um estudo de caso que utiliza o ferramental teórico e prático proposto. ______________________________________________________________________________ ABSTRACT / This work presents a study of methodologies to formally verify applications developed with imperative languages, specially with the Java language. The theoretical formalisms shown include Hoare Logic, which is used to sketch properties on imperative languages, and JML constructions (based on Hoare Logic), which is a speci cation language used to specify the expected behavior from Java programs. The tools shown are the Krakatoa system, used to convert JML speci cations into proof obligations, and the Coq interactive proof environment, used to verify proof obligations. Finally, this paper presents a case study that employs the theoretical and practical proposed framework.

Orientador: Waldemar W. Setzer / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Matematica, Estatistica e Ciencia da Computação / Made available in DSpace on 2018-07-14T11:42:46Z (GMT). No. of bitstreams: 1 Badelucci_AntonioCarlos_M.pdf: 7319789 bytes, checksum: cffff5414360e0cb106bba181db8d264 (MD5) Previous issue date: 1974 / Resumo: Este trabalho visa ser um subsídio aqueles que se interessam, na ciência da computação, pela resolução de problemas referentes à manipulação simbólica estruturada. O sistema apresentado não pretente ser completo ou final, sua concepção prevê e espera complementos. Espero com ele abrir perspectivas de desenvolvimento na área das linguagens e na resolução de alguns problemas de lingüística computacional. O sistema apresentado vem precedido de uma crítica de outros sistemas em aspecto em que estes nos pareceram ineficientes ou mal concebidos, preocupamo-nos em fornecer ao usuário a máxima flexibilidade na utilização dos recursos do sistema, com um mínimo desgaste na introdução de novos conceitos e tendo sempre em conta uma facilitação do processo de aprendizagem. Essa preocupação vem acompanhada de outra: no desenvolvimento do sistema tivemos sempre presente uma ótima utilização de memória e a minimização dos tempos de execução. A concepção geral e acompanhada de listagens e explicações sobre cada peça particular do sistema. / Abstract: Not informed. / Mestrado / Mestre em Ciência da Computação

Estágio realizado na ALERT Life Sciences Computing, S. A. e orientado pelo Eng.º Rui Neves / Tese de mestrado integrado. Engenharia Informática e Computação. Faculdade de Engenharia. Universidade do Porto. 2009

MACIEL. D. L. Sherlock N-Overlap: normalização invasiva e coeficiente de sobreposição para análise de similaridade entre códigos-fonte em disciplinas de programação. 2014. 105 f. Dissertação (Mestrado em Engenharia de Teleinformática) - Centro de Tecnologia, Universidade Federal do Ceará, Fortaleza, 2014. / Submitted by Marlene Sousa (mmarlene@ufc.br) on 2015-02-27T18:39:59Z No. of bitstreams: 1 2014_dis_dlmaciel.pdf: 3409582 bytes, checksum: 8d85d508f02fe688e23c17dd70679cb4 (MD5) / Approved for entry into archive by Marlene Sousa(mmarlene@ufc.br) on 2015-03-04T16:07:48Z (GMT) No. of bitstreams: 1 2014_dis_dlmaciel.pdf: 3409582 bytes, checksum: 8d85d508f02fe688e23c17dd70679cb4 (MD5) / Made available in DSpace on 2015-03-04T16:07:48Z (GMT). No. of bitstreams: 1 2014_dis_dlmaciel.pdf: 3409582 bytes, checksum: 8d85d508f02fe688e23c17dd70679cb4 (MD5) Previous issue date: 2014-07-07 / This work is contextualized in the problem of plagiarism detection among source codes in programming classes. Despite the wide set of tools available for the detection of plagiarism, only few tools are able to effectively identify all lexical and semantic similarities between pairs of codes, because of the complexity inherent to this type of analysis. Therefore to the problem and the scenario in question, it was made a study about the main approaches discussed in the literature on detecting plagiarism in source code and as a main contribution, conceived to be a relevant tool in the field of laboratory practices. The tool is based on Sherlock algorithm, which has been enhanced as of two perspectives: firstly, with changes in the similarity coefficient used by the algorithm in order to improve its sensitivity for comparison of signatures; secondly, proposing intrusive techniques preprocessing that, besides eliminating irrelevant information, are also able to overemphasize structural aspects of the programming language, or gathering separating strings whose meaning is more significant for the comparison or even eliminating sequences less relevant to highlight other enabling better inference about the degree of similarity. The tool, called Sherlock N-Overlap was subjected to rigorous evaluation methodology, both in simulated scenarios as classes in programming, with results exceeding tools currently highlighted in the literature on plagiarism detection. / Este trabalho se contextualiza no problema da detecção de plágio entre códigos-fonte em turmas de programação. Apesar da ampla quantidade de ferramentas disponíveis para a detecção de plágio, poucas são capazes de identificar, de maneira eficaz, todas as semelhanças léxicas e semânticas entre pares de códigos, o que se deve à complexidade inerente a esse tipo de análise. Fez-se, portanto, para o problema e o cenário em questão, um estudo das principais abordagens discutidas na literatura sobre detecção de plágio em código-fonte e, como principal contribuição, concebeu-se uma ferramenta aplicável no domínio de práticas laboratoriais. A ferramenta tem por base o algoritmo Sherlock, que foi aprimorado sob duas perspectivas: a primeira, com modificações no coeficiente de similaridade usado pelo algoritmo, de maneira a melhorar a sua sensibilidade para comparação de assinaturas; a segunda, propondo técnicas de pré-processamento invasivas que, além de eliminar informação irrelevante, sejam também capazes de sobrevalorizar aspectos estruturais da linguagem de programação, reunindo ou separando sequências de caracteres cujo significado seja mais expressivo para a comparação ou, ainda, eliminando sequências menos relevantes para destacar outras que permitam melhor inferência sobre o grau de similaridade. A ferramenta, denominada Sherlock N-Overlap, foi submetida a rigorosa metodologia de avaliação, tanto em cenários simulados como em turmas de programação, apresentando resultados superiores a ferramentas atualmente em destaque na literatura sobre detecção de plágio.

Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnologico / Made available in DSpace on 2016-01-08T22:28:04Z (GMT). No. of bitstreams: 1 108878.pdf: 2304607 bytes, checksum: 9e7404e6e48b5ebbcb49740813a04ab7 (MD5) Previous issue date: 1997 / Esta dissertação descreve uma ferramenta de simulação para sistemas dependentes de tempo descritos com a técnica de descrição formal (TDF) RT-LOTOS. Discute-se a verificação e validação de especificações de sistemas dependentes de tempo, bem como os principais aspectos da TDF utilizada. A arquitetura da ferramenta é descrita e também são apresentados os algoritmos utilizados no processo de simulação. As funcionalidades da ferramenta são descritas, demonstrando a sua utilidade na validação de especificações RT-LOTOS. Ao final, são apresentados alguns estudos de caso para ilustrar o uso da ferramenta.

Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2010. / Submitted by Allan Wanick Motta (allan_wanick@hotmail.com) on 2011-01-21T18:14:44Z No. of bitstreams: 1 2010_FlavioJoseFerroBarros.pdf: 454810 bytes, checksum: 20b7e7f5115fdc9ff34396a6f5e6cc1f (MD5) / Approved for entry into archive by Daniel Ribeiro(daniel@bce.unb.br) on 2011-01-26T00:28:37Z (GMT) No. of bitstreams: 1 2010_FlavioJoseFerroBarros.pdf: 454810 bytes, checksum: 20b7e7f5115fdc9ff34396a6f5e6cc1f (MD5) / Made available in DSpace on 2011-01-26T00:28:37Z (GMT). No. of bitstreams: 1 2010_FlavioJoseFerroBarros.pdf: 454810 bytes, checksum: 20b7e7f5115fdc9ff34396a6f5e6cc1f (MD5) / Apresenta-se uma formalização das propriedades de composicionalidade do Cálculo lambda-ex em Coq. A abordagem utilizada baseia-se na lógica nominal de acordo com o trabalho desenvolvido por [3]. Mais especificamente estendemos a formalização do lambda-cálculo contida neste trabalho de forma a incluir a operação de substituição explícita do cálculo lambda-ex. Nessa abordagem, a alpha-equivalência coincide com a igualdade pré-construída de Coq, e os princípios de recursão e indução sobre classes de lambda-termos possuem tratamento específico. Escolhemos trabalhar com o cálculo lambda-ex por ser atualmente o único cálculo que satisfaz simultaneamente todas as propriedades desejáveis para um cálculo de substituições explícitas. Ele é uma extensão do lambda-x com uma regra de reescrita para composição de substituições dependentes e uma equação para comutação de substituições independentes. O cálculo lambda-ex usa um construtor unário para a substituição explicita, mas tem o mesmo poder de expressividade de cálculos com substituições simultâneas. _________________________________________________________________________________ ABSTRACT / We present a formalization of properties of compositionality of the ex-calculus in Coq. The approach is based in the nominal logic as presented in the paper [3]. More precisely, we extended a formalization of the -calculus in such a way that it now includes the explicit substitution operation of the ex-calculus. In this approach, -equivalence of -terms coincides with the Coqt’s built-in equality, and the principles of recursion and induction over classes of -terms are treated in a specific way. We chose to work with the ex-calculus because it is currently the only calculus that simultaneously satisfies all the desirable properties for a calculus of explicit substitutions. It is an extension of the x-calculus with a rewrite rule for composition of dependent substitutions and one equation for independent substitutions. The ex-calculus has a unary constructor for the explicit substitution operation, but have the same expressive power of calculi with simultaneous substitutions.

Orientador: Wagner C. Amaral / Dissertação (mestrado) - Universidade Estadual de Campinas, Faculdade de Engenharia Eletrica / Made available in DSpace on 2018-07-13T23:48:07Z (GMT). No. of bitstreams: 1 Nazzetta_RubenMario_M.pdf: 10450932 bytes, checksum: 00ecca7925c1cfde8dd3935e1d1de96a (MD5) Previous issue date: 1991 / Resumo: O presente trabalho detalha o desenvolvimento de um sistema baseado em conhecimento para o auxílio nas tarefas de configuração e supervisão de algoritmos de modelagem e controle de processos. O sistema consta dos seguintes módulos: Módulo de controle onde encontram-se os algoritmos de controle, de três termos (PID), de Variância Mínima Generalizada (GMV) e o Controlador Preditivo Generalizado (GPC); Módulo de identificação com o algoritmo de matriz estendida; Módulo de detecção de não estacionariedades do processo, baseado no algoritmo do erro previsto; Máquina de inferência com encadeamento reverso, utilizada junto com a Base de Conhecimento de Configuração; Máquina de inferência com encadeamento direto, utilizada com a Base de Conhecimento de supervisão; Base de Dados; e Interface Homem-Máquina. A Base de Dados, acessível a ambas as máquinas de inferência é composta de fatos escritos em linguagem natural. As bases de conhecimento possuem a estrutura de regras de produção do tipo SE <<condição>> então <<conclusão>>. A máquina de inferência de configuração obtém os valores dos objetos utilizados nos algoritmos de controle e identificação para satisfazer os requisitos de desempenho especificados ... Observação: O resumo, na íntegra, poderá ser visualizado no texto completo da tese digital / Abstract: Not informed. / Mestrado / Mestre em Engenharia Elétrica

Orientador: Douglas Eduardo Zampieri / Dissertação (mestrado) - Universidade Estadual de Campinas, Faculdade de Engenharia Mecanica / Made available in DSpace on 2018-07-13T23:58:10Z (GMT). No. of bitstreams: 1 Mendeleck_Andre_M.pdf: 5599564 bytes, checksum: ec23fed530a74495ffccc72362bbbffa (MD5) Previous issue date: 1991 / Resumo: Nesta dissertação é especificado e implementado o protótipo de uma linguagem de programação e um sistema de CAD-Simulação para um robô manipulador antropomórflco com 6 graus de liberdade. Trata-se de uma linguagem de alto nível destinada a programação de movimentos a nível de manlpulador e um sistema de CAD-Simulação que permite a visualização, em 'tempo real' , dos movimentos do robô em um terminal gráfico, sendo também, implementado um módulo de teach-in e um módulo de simulação apresentando informações sobre a evolução cinemátlca e dinâmica dos links e garra do robô / Abstract: This dissertation contains the specification and implementation of a prototype language program and a CAD-Simulation system for an antropomorphic manipulator with six degrees of freedom. The system has a high level language for motion program, a CAD-Simulator system to visualize robot motion in "real time", a teach-in and a simulation sub-system to visualize the kinematic and dynamic evolution of the links and the gras / Mestrado / Mecanica dos Sólidos e Projeto Mecanico / Mestre em Engenharia Mecânica

Orientador: Clesio Luiz Tozzi / Dissertação (mestrado) - Universidade Estadual de Campinas, Faculdade de Engenharia Eletrica / Made available in DSpace on 2018-07-14T00:27:48Z (GMT). No. of bitstreams: 1 Pizarro_DiegoA.Aracena_M.pdf: 8698005 bytes, checksum: fb4e06b4f9a8054cca126f06efe2c461 (MD5) Previous issue date: 1991 / Resumo: No presente trabalho realiza-se o estudo do comportamento da proposta para a implementarão paralela do algoritmo "Linhas e Superfícies Escondidas", utilizando a técnica do pintor, podendo ser inserido no contexto de computação gráfica e processamento paralelo. O trabalho foi dividido em três etapas principais: Na primeira etapa, apresenta-se o estudo do algoritmo e a proposta para a implementação paralela, realizando a análise dos módulos e fluxo dos dados entre os módulos. Na segunda etapa apresenta-se o desenvolvimento do sistema que executa a aplicação em máquinas HIHD fracamente acopladas, utilizando o mapeamento de várias topologias na placa lnmos IMS B008, com um número reduzido de processadores. Na terceira etapa apresenta-se o desenvolvimento do simulador do sistema multiprocessador, que permitiu realizar o estudo do comportamento do algoritmo, em um maior número de processadores, considerando diferentes particionamentos, para os quais apresentam-se os resultados experimentais obtidos / Abstract: Not informed. / Mestrado / Mestre em Engenharia Elétrica

Orientador: Arthur João Catto / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Matematica, Estatistica e Ciencia da Computação / Made available in DSpace on 2018-07-14T02:04:30Z (GMT). No. of bitstreams: 1 Rubira_CeciliaMaryFischer_M.pdf: 1743339 bytes, checksum: 48d2cb6de912c144c1721d797fa1fa45 (MD5) Previous issue date: 1989 / Resumo: Este trabalho apresenta um estudo detalhado da geração de código de uma linguagem de alto nível voltada para programação paralela denominada SISAL, implementada na Máquina de Fluxo de Dados de Manchester. Os pontos de deterioração de paralelismo obtidos na geração de código são identificados, apresentando sempre que possível otimizações que explorem o assincronismo e o poder computacional paralelo da máquina. O compilador SISAL gera código num formato intermediário gráfico chamado IFI, que é então traduzido para o código de máquina (grafos de fluxo de dados) através de um sistema de tradução. As otimizações aqui implementadas se concentram nos esquemas utilizados para a tradução do formato IF1 para código dependente de máquina. / Abstract: Not informed. / Mestrado / Mestre em Ciência da Computação