La génération de stratégies pour les solveurs en Satisfiabilité Modulo des Théories (SMT) nécessite des outils théoriques et pratiques qui permettent aux utilisateurs d’exercer un contrôle stratégique sur les aspects heuristiques fondamentaux des solveurs de SMT, tout en garantissant leur performance. Nous nous intéressons dans cette thèse au solveur Z3 , l’un des plus efficaces lors des compétitions SMT (SMT-COMP). Dans les solveurs SMT, la définition d’une stratégie repose sur un ensemble de composants et paramètres pouvant être agencés et configurés afin de guider la recherche d’une preuve de (in)satisfiabilité d’une instance donnée. Dans cette thèse, nous abordons ce défi en définissant un cadre pour la génération autonome de stratégies pour Z3, c’est-à-dire un algorithme qui permet de construire automatiquement des stratégies sans faire appel à des connaissances d’expertes. Ce cadre général utilise une approche évolutionnaire (programmation génétique), incluant un système à base de règles. Ces règles formalisent la modification de stratégies par des principes de réécriture, les algorithmes évolutionnaires servant de moteur pour les appliquer. Cette couche intermédiaire permettra d’appliquer n’importe quel algorithme ou opérateur sans qu’il soit nécessaire de modifier sa structure, afin d’introduire de nouvelles informations sur les stratégies. Des expérimentations sont menées sur les jeux classiques de la compétition SMT-COMP. / The Strategy Challenge in Satisfiability Modulo Theories (SMT) claims to build theoretical and practical tools allowing users to exert strategic control over core heuristic aspects of high-performance SMT solvers. In this work, we focus in Z3 Theorem Prover: one of the most efficient SMT solver according to the SMT Competition, SMT-COMP. In SMT solvers, the definition of a strategy relies on a set of tools that can be scheduled and configured in order to guide the search for a (un)satisfiability proof of a given instance. In this thesis, we address the Strategy Challenge in SMT defining a framework for the autonomous generation of strategies in Z3, i.e. a practical system to automatically generate SMT strategies without the use of expert knowledge. This framework is applied through an incremental evolutionary approach starting from basic algorithms to more complex genetic constructions. This framework formalise strategies modification as rewriting rules, where algorithms acts as enginess to apply them. This intermediate layer, will allow apply any algorithm or operator with no need to being structurally modified, in order to introduce new information in strategies. Validation is done through experiments on classic benchmarks of the SMT-COMP.

L’objectif principal de cette thèse est l’étude et la formalisation de nouvelles constructions permettant d’augmenter l’expressivité du filtrage et des langages à base de règles en général. Ceci est motivé par le développement de Tom, un système qui enrichit les langages impératifs comme Java et C avec des constructions de haut niveau comme le filtrage et les stratégies. Une première extension que l’on propose est la notion d’anti-patterns, i.e. des motifs qui peuvent contenir des symboles de complément. Nous définissons de manière formelle la sémantique des anti-patterns dans le cas syntaxique et modulo une théorie équationnelle arbitraire. Puis nous étendons la notion classique de filtrage entre les motifs et les termes clos au filtrage entre les anti-patterns et les termes clos (anti-filtrage). Ensuite, nous proposons plusieurs extensions aux constructions de filtrage fournies par Tom. La condition pour l’application d’une règle devient une conjonction ou disjonction de contraintes de filtrage et d’anti-filtrage ainsi que d’autres types de conditions. Les techniques classiques de compilation du filtrage ne sont pas bien adaptées à ces conditions complexes. On propose donc une nouvelle méthode de compilation basée sur des systèmes de réécriture contrôlés par des stratégies. Nous avons complètement réécrit le compilateur de Tom en utilisant cette technique. Tous ces éléments rassemblés constituent un environnement pour décrire et implémenter des transformations de manière élégante et concise. Pour promouvoir son utilisation dans des projets à grand échelle, on développe une technique pour extraire automatiquement des informations structurelles à partir d’une hiérarchie de classes Java. Cela permet l’intégration du filtrage offert par Tom dans n’importe quelle application Java / The main objective of this thesis is the study of new constructs and formalisms that increase the expressivity of pattern matching and rule based languages in general. This is motivated by the development of Tom, a system that adds high level constructs such as pattern matching and strategies to languages like Java and C. A first extension that we propose is the notion of anti-patterns, i.e. patterns that may contain complement symbols. We define formally the semantics of anti-patterns both in the syntactic case and modulo an arbitrary equational theory. We then extend the classical notion of matching between patterns and ground terms to matching between anti-patterns and ground terms. We further propose several extensions to the matching constructs provided by Tom. Consequently, the condition for the application of a rule becomes a combination of matching and anti-matching constraints together with other types of conditions. Classical compilation techniques for pattern matching are not very well suited for these complex conditions. Therefore we propose a new compilation method based on rewrite systems controlled by strategies, which provides a high level of modularity. Tom’s compiler has been rewritten from scratch using this technique. All this constitutes a software environment for expressing transformations in a clear and concise way. To promote its use in large scale applications, we propose an approach for extracting automatically structural information from arbitrary Java hierarchies. This allows a seamless integration of Tom’s pattern matching facilities in any application

L'objet de cette thèse est l'étude de certaines propriétés arithmétiques et combinatoires de la fonction somme des chiffres. Nous commençons par étudier les sommes d'exponentielles de la forme $dissum_{nleq x}expleft(2ipileft(frac{l}{m}S_q(n)+frac{k}{m'}S_{q}(n+1)+theta nright)right)$ en vue de montrer un résultat d'équirépartition modulo $1$ et un théorème probabiliste d'ErdH{o}s-Kac. Ensuite, on va généraliser un problème dû à Gelfond concernant l'étude de la répartition dans les progressions arithmétiques de la fonction somme des chiffres au cas des nombres ellipséphiques. En particulier, on donne un théorème analogue à celui d'Erdös, Mauduit et S'arközy sur l'uniforme répartition des entiers ellipséphiques dans les progressions arithmétiques sous une contrainte sur la somme des chiffres. Enfin, une étude de l'ordre moyen de certaines fonctions arithmétiques soumises à des contraintes digitales est faite en conséquence des travaux de Mkaouar et Wannès. / The aim of this thesis is the study of some arithmetic and combinatoric properties of the sum of digits function. We start by the study of exponential sums of the form $dissum_{nleq x}expleft(2ipileft(frac{l}{m}S_q(n)+frac{k}{m'}S_q(n+1)+theta nright)right)$ in order to establish a result of equidistribution modulo $1$ in addition to a probabilistic theorem of the kind ErdH{o}s-Kac. Then, we generalize a problem due to Gelfond concerning the distribution in residue classes of the sum of digits function in the case of integers with missing digits. Besides, we give a similar result to that of ErdH{o}s, Mauduit and S'ark"{o}zy on the uniform distribution of integers with missing digits in arithmetic progressions under a constraint on the sum of digits. Finally, a study of the order of magnitude of some arithmetical functions under digital constraints is done as a consequence of the works of Mkaouar and Wannès.

Doctor of Philosophy / Department of Mathematics / Todd E. Cochrane / Let $m$ be a positive integer, $p$ be an odd prime, and $\mathbb{Z}_{p^m } = \mathbb{Z}/(p^m )$ be the ring of integers modulo $p^m $. Let $$Q({\mathbf{x}}) = Q(x_1 ,x_2 ,...,x_n ) = \sum\limits_{1 \leqslant i \leqslant j \leqslant n} {a_{ij} x_i x_j } ,$$ be a quadratic form with integer coefficients. Suppose that $n$ is even and $\det A_Q \not \equiv 0\;(\bmod p)$. Set $\Delta = (( - 1)^{n/2} \det A_Q /p)$, where $( \cdot /p)$ is the Legendre symbol and $\left\| {\mathbf{x}} \right\| = \max \left| {x_i } \right|$. Let $V$ be the set of solutions the congruence $ $Q({\mathbf{x}})\, \equiv \;0\quad (\bmod p^m ) \quad(1)$$, contained in $\mathbb{Z}^n $ and let $B$ be any box of points in $\mathbb{Z}^n $of the type $$B = \left\{ {{\mathbf{x}} \in \mathbb{Z}^n \left| {\,a_i \leqslant x_i < a_i + m_i ,\;\,1 \leqslant i \leqslant n} \right.} \right\},$$ where $a_i ,m_i \in \mathbb{Z},\;1 \leqslant m_i \leqslant p^m $. In this dissertation we use the method of exponential sums to investigate how large the cardinality of the box $B$ must be in order to guarantee that there exists a solution ${\mathbf{x}}$of (1) in $ B$. In particular we will focus on cubes (all $m_i $equal) centered at the origin in order to obtain primitive solutions with $\left\| {\mathbf{x}} \right\|$ small. For $m = 2$ and $n \geqslant 4$ we obtain a primitive solution with $\left\| {\mathbf{x}} \right\| \leqslant \max \left\{ {2^5 p,2^{18} } \right\}$. For $m = 3$, $n \geqslant 6$, and $\Delta = + 1$, we get $\left\| {\mathbf{x}} \right\| \leqslant \max \left\{ {2^{2/n} p^{(3/2) + (3/n)} ,2^{(2n + 4)/(n - 2)} } \right\}$. Finally for any $m \geqslant 2$, $n \geqslant m,$ and any nonsingular quadratic form we obtain $\left\| {\mathbf{x}} \right\| \leqslant \max \{ 6^{1/n} p^{m[(1/2) + (1/n)]} ,2^{2(n + 1)/(n - 2)} 3^{2/(n - 2)} \} $. Others results are obtained for boxes $B$ with sides of arbitrary lengths.

Objetivando galgar um maior conhecimento das propriedades geotécnicas dos solos tropicais, a presente tese introduz um estudo de solos de textura fina, plintíticos e concrecionados coletados em obras aeroportuárias na Amazônia Legal, empregando-se as metodologias classificatórias MCT e Reliliente, além das de caracterização e de análise mineralógica da fração areia. Para os ensaios triaxiais dinâmicos, desenvolveu-se um novo equipamento inteiramente nacional e monitorado por microcomputador, o qual permite testar corpos de prova com 5, 10 ou 15 cm de diâmetro, de modo a tratar as amostras praticamente em sua granulometria real. Enfoques adicionais são efetuados sobre a transformação dos solos plintíticos submetidos a diferentes ciclos de secagem-molhagem, e sobre o caráter qualitativo da estrutura e estabilidade dos solos lateríticos concrecionados, através de curvas de Compactação Total e diagramas de Imersão em Água. Apresenta-se, também, a realidade aeroportuária e de materiais da região, executando-se um tratamento estatístico e apreciação de dados levantados em estudos referentes à implantação de aeroportos, conduzindo à discretização de materiais e à definição de macro-zonas com diferentes aptidões geotécnicas. Os resultados alcançados, além de propiciarem uma visão global das características e propriedades dos solos típicos da Amazônia, permitem o estabelecimento de novos padrões de comportamento geotécnico e critérios MCT/Resiliente adaptados para a seleção adequada desses materiais, com vistas a seu uso racional em camadas de pavimentos.

L'objet de cette thèse est l'étude des champs algébriques de revêtements galoisiens de courbes algébriques, avec un intérêt spécial pour la caractéristique positive. On établit tout d'abord des résultats concernant les actions de schémas en groupes sur les champs: existence et algébricité des champs de points fixes et champs quotients; lien avec le champ classifiant du groupe. Dans toute la suite on considère des groupes finis~$G,G'$ d'ordres~$n,n'$. Utilisant la théorie de Hurwitz des revêtements modérés de courbes, on exhibe tout d'abord un champ qui est une compactification lisse du champ~${\cal M}_g(G')$ des courbes de genre~$g$ avec structure de niveau~$G'$. C'est aussi une désingularisation, modulaire qui plus est, du champ propre donné par Deligne et Mumford en normalisant le champ des courbes stables de genre~$g$ dans~${\cal M}_g(G')$. Ensuite, grâce à l'action de certains groupes sur le champ produit ci-dessus, on propose une compactification du champ des courbes de genre~$g$ avec action de~$G$, la base comprenant cette fois-ci les caractéristiques qui divisent~$n$. Cette compactification est lisse a priori seulement au-dessus des caractéristiques premières à~$n$. Puis, on se penche sur l'aspect local de la ramification sauvage. Supposons que~$G$ agit sur un schéma~$X$ au-dessus d'un anneau de valuation discrète d'inégales caractéristiques (la caractéristique résiduelle divisant~$n$) et que l'action est fidèle sur la fibre générique. On souhaite trouver un modèle pour~$G$ qui agisse fidèlement y compris sur la fibre spéciale, avec une propriété d'unicité. Si~$X$ est propre cela est assez facile. Lorsque~$X$ est affine nous donnons une méthode, utilisant les éclatements de Néron, qui mène conjecturalement à une construction effective de ce modèle. Dans le cas du groupe cyclique d'ordre~$p$, cette méthode fournit la structure précise des revêtements de courbes lisses. Enfin nous concluons par un exemple qui illustre les questions traitées dans la thèse.

Soit p un nombre premier. Cette thèse est une contribution à la théorie des représentations modulo p des groupes réductifs p-adiques, jusque là essentiellement centrée sur le groupe linéaire général GL(n) défini sur un corps local non archimédien F complet pour une valuation discrète, de caractéristique résiduelle p et de corps résiduel fini. L'originalité de nos travaux réside notamment dans le fait qu'ils concernent d'autres groupes : nous nous intéressons en effet à la description des classes d'isomorphisme des représentations modulo p de groupes formés des F-points d'un groupe réductif connexe défini, quasi-déployé de rang semi-simple égal à 1 sur F. Une place particulière est accordée au groupe spécial linéaire SL(2) et au groupe unitaire quasi-déployé non ramifié en trois variables U(2,1). Dans ces deux cas, nous montrons que les classes d'isomorphisme des représentations lisses irréductibles admissibles à coefficients dans un corps algébriquement clos de caractéristique p se scindent en deux familles : les représentations non supersingulières et les représentations supersingulières. Nous décrivons complètement les représentations non supersingulières, et montrons que la notion de supersingularité est équivalence à la notion de supercuspidalité apparaissant dans la théorie complexe. Nous donnons aussi une description explicite des représentations supersingulières de SL(2,Q_{p}), ce qui nous permet de définir dans ce cas une correspondance de Langlands locale semi-simple modulo p compatible à celle construite par Breuil pour GL(2). Nous généralisons ensuite les méthodes utilisées jusqu'alors pour obtenir la description des représentations non supercuspidales de G(F) lorsque G est un groupe réductif connexe défini, quasi-déployé, et rang semi-simple égal à 1 sur F. Elle fait apparaître trois familles deux à deux disjointes de représentations : les caractères, les représentations de la série principale et celles de la série spéciale. Nous terminons par une classification des modules à droite simples sur la pro-p-algèbre de Hecke-Iwahori H de SL(2,F). On déduit en particulier que l'application qui envoie une représentation lisse modulo p de SL(2,F) sur son espace de vecteurs invariants sous l'action du pro-p-sous-groupe d'Iwahori induit une bijection entre l'ensemble des classes d'isomorphisme des représentations lisses irréductibles non supersingulières de SL(2,F) et l'ensemble des classes d'isomorphisme des H-modules à droite simples non supersinguliers. Cette bijection s'étend aux objets supersinguliers lorsque l'on suppose que F = Q_{p}, ce qui est de bon augure dans la recherche d'une équivalence de catégories analogue à celle obtenue par Ollivier dans le cadre de la théorie existant pour GL(2, Q_{p}).

<p>In this thesis we address the problem of integrated software pipelining for clustered VLIW architectures. The phases that are integrated and solved as one combined problem are: cluster assignment, instruction selection, scheduling, register allocation and spilling.</p><p>As a first step we describe two methods for integrated code generation of basic blocks. The first method is optimal and based on integer linear programming. The second method is a heuristic based on genetic algorithms.</p><p>We then extend the integer linear programming model to modulo scheduling. To the best of our knowledge this is the first time anybody has optimally solved the modulo scheduling problem for clustered architectures with instruction selection and cluster assignment integrated.</p><p>We also show that optimal spilling is closely related to optimal register allocation when the register files are clustered. In fact, optimal spilling is as simple as adding an additional virtual register file representing the memory and have transfer instructions to and from this register file corresponding to stores and loads.</p><p>Our algorithm for modulo scheduling iteratively considers schedules with increasing number of schedule slots. A problem with such an iterative method is that if the initiation interval is not equal to the lower bound there is no way to determine whether the found solution is optimal or not. We have proven that for a class of architectures that we call transfer free, we can set an upper bound on the schedule length. I.e., we can prove when a found modulo schedule with initiation interval larger than the lower bound is optimal.</p><p>Experiments have been conducted to show the usefulness and limitations of our optimal methods. For the basic block case we compare the optimal method to the heuristic based on genetic algorithms.<em></em></p><p><em>This work has been supported by The Swedish national graduate school in computer science (CUGS) and Vetenskapsrådet (VR).</em></p>

Submitted by Marcos Roberto Gomes (mrobertosg@gmail.com) on 2017-06-22T15:28:21Z No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertacao_Rodrigo_Farias_Araujo.pdf: 2432590 bytes, checksum: a0accf6a453257550a0ea9f75b50b687 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2017-06-23T14:38:14Z (GMT) No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertacao_Rodrigo_Farias_Araujo.pdf: 2432590 bytes, checksum: a0accf6a453257550a0ea9f75b50b687 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2017-06-23T14:44:39Z (GMT) No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertacao_Rodrigo_Farias_Araujo.pdf: 2432590 bytes, checksum: a0accf6a453257550a0ea9f75b50b687 (MD5) / Made available in DSpace on 2017-06-23T14:44:39Z (GMT). No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertacao_Rodrigo_Farias_Araujo.pdf: 2432590 bytes, checksum: a0accf6a453257550a0ea9f75b50b687 (MD5) Previous issue date: 2017-03-30 / This work presents a new method of optimization applied to different classes of problems, such as non-convex and convex. The methodology consists in the use the counterexample generated from the model checking technique based on Boolean satisfiability theory (SAT) and satisfiability modulo theory (SMT), to guide the optimization process. Three algorithms of optimization are developed: Generic Algorithm, applied to any class of optimization problem, it will be used in the optimization of non-convex functions, Simplified Algorithm, used in the optimization of functions in which there is some previous knowledge, e. g., semi-defined or defined positive functions and Fast Algorithm, used to optimize convex functions. In addition, convergence proofs are provided for the respective algorithms. The algorithms are implemented using two model verifiers, CBMC which uses the SAT-based MiniSAT solver as back-end, and the ESBMC, which supports SMT-based solvers, such as Z3, Boolector and MathSAT. For perfomance evaluation, the algorithms are applied to a set of thirty functions taken from the literature and used to test optimization algorithms, they are also compared with traditional optimization algorithms usually used in solving non-convex optimization problems, such as genetic algorithm, particle swarm, pattern search, simulated annealing and nonlinear programming. Through the analysis of the results it can be concluded that the developed algorithms are suitable the classes of functions for which they were developed and have a higher rate of success in the search for the optimal value in comparison with the other algorithms. Finally, the developed methodology is applied to solve optimization problems in the context of the two-dimensional path planning for autonomous mobile robots. / Este trabalho apresenta um novo método de otimização aplicado a diferentes classes de problemas, como não-convexos e convexos. A metodologia consiste na utilização do contraexemplo gerado a partir da técnica de verificação de modelos, baseada na teoria de satisfatibilidade booleana (SAT) ou na teoria do módulo de satisfatibilidade (SMT), para guiar o processo de otimização. São desenvolvidos três algoritmos de otimização, são eles: Algoritmo Genérico, aplicado a qualquer classe de problema de otimização, neste será utilizado na otimização de funções não-convexas, Algoritmo Simplificado, empregado na otimização de funções nas quais tem-se algum conhecimento prévio, por exemplo, funções semi-definidas ou definidas positivas e Algoritmo Rápido, utilizado para otimização de funções convexas. Adicionalmente, são fornecidas as provas de convergência para os respectivos algoritmos. Os algoritmos são implementados utilizando dois verificadores de modelos, o CBMC que utiliza como back-end o solucionador MiniSAT baseado em SAT, e o ESBMC, que tem suporte aos solucionadores baseados em SMT, como: Z3, Boolector e MathSAT. Para avaliação de desempenho, os algoritmos são aplicados a um conjunto de trinta funções retiradas da literatura e utilizadas para teste de algoritmos de otimização, os mesmos também são comparados com algoritmos de otimização tradicionais usualmente empregados na resolução de problemas de otimização não-convexa, como: algoritmo genético, enxame de partícula, busca de padrões, recozimento simulado e programação não-linear. Através da análise dos resultados pode-se concluir que os algoritmos desenvolvidos são adequados as classes de funções para os quais foram desenvolvidos e possuem maior taxa de acerto na busca pelo valor ótimo em comparação com os outros algoritmos. Finalmente a metodologia desenvolvida é aplicada para resolver problemas de otimização no contexto de planejamento de caminhos bidimensionais para robô móveis autônomos.

[pt] Esta dissertação tem como objetivo exibir uma fórmula para cálcular o anel de cohomologia de um fibrado flag homogêneo de um grupo de Lie G compacto e conexo. Para concluir o resultado é usado a cohomologia equivariante, em particular, sua abordagem mais algébrica. Isto implica introduzir G- módulos e sua teoria equivariante, o que passa também por introduzir a álgebra de Weil, o modelo de Cartan e o homomorfismo característico. A demonstração do resultado também está fortemente baseada nas propriedades algébricas dos toros maximais de G. / [en] The purpose of this dissertation is to present a formula for calculating the cohomology ring of a homogeneous flag bundles of a compact and connected Lie G group. To conclude the result, the equivalent cohomology is used, in particular, its more algebraic approach. This implies introducing G modules and their equivalent theory, which also involves introducing Weil algebra, Cartans model and characteristic homomorphism. The income statement is also strongly based on the algebraic properties of the maximal torus of G.