Made available in DSpace on 2015-04-11T14:02:59Z (GMT). No. of bitstreams: 1 Pedro Antonio Gonzales Sanchez.pdf: 1313238 bytes, checksum: 234b86be8198c8c3e01948d1e566aa19 (MD5) Previous issue date: 2013-07-17 / CNPq - Conselho Nacional de Desenvolvimento Científico e Tecnológico / Today, the Internet is considered a powerful tool of communication and information. Its impact on society is increasing more and more, which means that it is becoming indispensable. In this context information searching systems are becoming increasingly important. In this paper, we propose a new search method capable of learning ranking functions that explore Web pages structure in blocks, using genetic programming. Different from previous works, our method allows combining traditional evidence in information retrieval with evidence derived from the structure of Web pages. To validate the proposed method, we use three real collections of pages (IG, CNN and BLOG). Experimental results show that our approach is able to overcome the results of a baseline of information which uses blocks information without learning machine, presenting precision benefits (MAP) of 9.38% in the IG collection, from 7.13% in CNN, and 25.87% in collection BLOG. Regarding our second baseline, which uses genetic programming out of traditional evidence in information retrieval, our method achieved benefits of 5.25% in the IG collection, 10.37% and 4.37% on CNN in collection BLOG. / Na atualidade, a Internet é considerada uma poderosa ferramenta de comunicação e informação. Seu impacto na sociedade está aumentando cada vez mais, o que significa que está se tornando indispensável. Neste contexto, sistemas de busca por informação tornam-se cada vez mais importantes. Neste trabalho, propomos um novo método de busca capaz de aprender funções de ranking que exploram a estrutura em bloco das páginas Web, usando programação genética. Diferentemente de trabalhos anteriores, nosso método permite combinar evidências tradicionais em recuperação de informação com evidências derivadas da estrutura das páginas. Para validar o método proposto, utilizamos três coleções reais de páginas (IG, CNN e BLOG). Os resultados experimentais mostram que nossa abordagem é capaz de superar os resultados de um baseline que usa informações de blocos sem aprendizagem de máquina, apresentando ganhos de precisão (MAP) de 9,38% na coleção IG, de 7,13% na CNN, e 25,87% na coleção de BLOG. Em relação a nosso segundo baseline, que usa programação genética a partir de evidências tradicionais de recuperação de informação, nosso método conseguiu ganhos de 5,25% na coleção IG, 10,37% na CNN e 4,37% na coleção de BLOG.

L’objectif général de cette thèse est le développement de méthodes mathématiques correctes et efficaces en pratique pour prouver automatiquement la correction de logiciels. Plus précisément, cette thèse est fondée sur la théorie de l’interprétation abstraite, un cadre mathématique puissant pour l’approximation du comportement des programmes. En particulier, cette thèse se concentre sur la preuve des propriétés de vivacité des programmes, qui représentent des conditions qui doivent être réalisés ultimement ou de manière répétée pendant l’exécution du programme. La terminaison des programmes est la propriété de vivacité la plus fréquemment considérée. Cette thèse conçoit des nouvelles approximations, afin de déduire automatiquement des conditions suffisantes pour la terminaison des programmes et synthétiser des fonctions de rang définies par morceaux, qui fournissent des bornes supérieures sur le temps d’attente avant la terminaison. Les approximations sont paramétriques dans le choix entre l’expressivité et le coût des approximations sous-jacentes, qui maintiennent des informations sur l’ensemble des valeurs possibles des variables du programme ainsi que les relations numériques possibles entre elles. Cette thèse développe également un cadre d’interprétation abstraite pour prouver des propriétés de vivacité, qui vient comme une généralisation du cadre proposé pour la terminaison. En particulier, le cadre est dédié à des propriétés de vivacité exprimées dans la logique temporelle, qui sont utilisées pour s’assurer qu’un événement souhaitable se produit une fois ou une infinité de fois au cours de l’exécution du programme. Comme pour la terminaison,des fonctions de rang définies par morceaux sont utilisées pour déduire des préconditions suffisantes pour ces propriétés, et fournir des bornes supérieures sur le temps d’attente avant un événement souhaitable. Les résultats présentés dans cette thèse ont été mis en œuvre dans un prototype d’analyseur. Les résultats expérimentaux montrent qu’il donne de bons résultats sur une grande variété de programmes, il est compétitif avec l’état de l’art, et il est capable d’analyser des programmes qui sont hors de la portée des méthodes existantes. / The overall aim of this thesis is the development of mathematically sound and practically efficient methods for automatically proving the correctness of computer software. More specifically, this thesis is grounded in the theory of abstract interpretation, a powerful mathematical framework for approximating the behavior of programs. In particular, this thesis focuses on provingprogram liveness properties, which represent requirements that must be eventually or repeatedly realized during program execution. Program termination is the most prominent liveness property. This thesis designs new program approximations, in order to automatically infer sufficient preconditions for program termination and synthesize so called piecewisedefined ranking functions, which provide upper bounds on the waiting time before termination. The approximations are parametric in the choice between the expressivity and the cost of the underlying approximations, which maintain information about the set of possible values of the program variables along with the possible numerical relationships between them. This thesis also contributes an abstract interpretation framework for proving liveness properties, which comes as a generalization of the framework proposedfor termination. In particular, the framework is dedicated to liveness properties expressed in temporal logic, which are used to ensure that some desirable event happens once or infinitely many times during program execution. As for program termination, piecewise-defined ranking functions are used to infer sufficient preconditions for these properties, and to provide upper boundson the waiting time before a desirable event. The results presented in this thesis have been implemented into a prototype analyzer. Experimental results show that it performs well on a wide variety of benchmarks, it is competitive with the state of the art, and is able to analyze programs that are out of the reach of existing methods.