Cette thèse s'intéresse à la démonstration automatique de la validité de formules mathématiques issues de la preuve de programmes. Elle se focalise tout particulièrement sur la Satisfiabilité Modulo Théories (SMT): un jeune domaine de recherche qui a connu de grands progrès durant la dernière décennie. Les démonstrateurs de cette famille ont des applications diverses dans la conception de microprocesseurs, la preuve de programmes, le model-checking, etc.Les démonstrateurs SMT offrent un bon compromis entre l'expressivité et l'efficacité. Ils reposent sur une coopération étroite d'un solveur SAT avec une combinaison de procédures de décision pour des théories spécifiques comme la théorie de l'égalité libre avec des symboles non interprétés, l'arithmétique linéaire sur les entiers et les rationnels, et la théorie des tableaux.L'objectif de cette thèse est d'améliorer l'efficacité et l'expressivité du démonstrateur SMT Alt-Ergo. Pour cela, nous proposons une nouvelle procédure de décision pour la théorie de l'arithmétique linéaire sur les entiers. Cette procédure est inspirée par la méthode de Fourier-Motzkin, mais elle utilise un simplexe sur les rationnels pour effectuer les calculs en pratique. Nous proposons également un nouveau mécanisme de combinaison, capable de raisonner dans l'union de la théorie de l'égalité libre, la théorie AC des symboles associatifs et commutatifs et une théorie arbitraire deShostak. Ce mécanisme est une extension modulaire et non intrusive de la procédure de completion close modulo AC avec la théorie de Shostak. Aussi, nous avons étendu Alt-Ergo avec des procédures de décision existantes pour y intégrer d'autres théories intéressantes comme la théorie de types de données énumérés et la théorie des tableaux. Enfin, nous avons exploré des techniques de simplification de formules en amont et l'amélioration de son solveur SAT. / This thesis tackles the problem of automatically proving the validity of mathematical formulas generated by program verification tools. In particular, it focuses on Satisfiability Modulo Theories (SMT): a young research topic that has seen great advances during the last decade. The solvers of this family have various applications in hardware design, program verification, model checking, etc.SMT solvers offer a good compromise between expressiveness and efficiency. They rely on a tight cooperation between a SAT solver and a combination of decision procedures for specific theories, such as the free theory of equality with uninterpreted symbols, linear arithmetic over integers and rationals, or the theory of arrays.This thesis aims at improving the efficiency and the expressiveness of the Alt-Ergo SMT solver. For that, we designed a new decision procedure for the theory of linear integer arithmetic. This procedure is inspired by Fourier-Motzkin's method, but it uses a rational simplex to perform computations in practice. We have also designed a new combination framework, capable of reasoning in the union of the free theory of equality, the AC theory of associative and commutativesymbols, and an arbitrary signature-disjoint Shostak theory. This framework is a modular and non-intrusive extension of the ground AC completion procedure with the given Shostak theory. In addition, we have extended Alt-Ergo with existing decision procedures to integrate additional interesting theories, such as the theory of enumerated data types and the theory of arrays. Finally, we have explored preprocessing techniques for formulas simplification as well as the enhancement of Alt-Ergo's SAT solver.

The thesis deals with speedup and accuracy of numerical computation, especially when differential equations are solved. Algorithms, which are fulling these conditions are named semi-analytical. One posibility how to accelerate computation of differential equation is paralelization. Presented paralelization is based on transformation numerical solution into residue number system, which is extended to floating point computation. A new algorithm for modulo multiplication is also proposed. As application applications in solution of differential calculus are the main goal it is discussed numeric integration with modified Euler, Runge - Kutta and Taylor series method in residue number system. Next possibilities and extension for implemented residue number system are mentioned at the end.

In dieser Arbeit wird das dynamische Auswertungsproblem über dynamische Datenbanken betrachtet, bei denen Tupel hinzugefügt oder gelöscht werden können. Die Aufgabe besteht darin einen dynamischen Algorithmus zu konstruieren, welcher unmittelbar nachdem die Datenbank aktualisiert wurde, die Datenstruktur, die das Resultat repräsentiert, aktualisiert. Die Datenstruktur soll in konstanter Zeit aktualisiert werden und das Folgende unterstützen: * Teste in konstanter Zeit ob ein Tupel zur Ausgabemenge gehört, * gebe die Anzahl der Tupel in der Ausgabemenge in konstanter Zeit aus, * zähle die Tupel aus der Ausgabemenge mit konstanter Taktung auf und * zähle den Unterschied zwischen der neuen und der alten Ausgabemenge mit konstanter Taktung auf. Im ersten Teil werden konjunktive Anfragen und Vereinigungen konjunktiver Anfragen auf relationalen Datenbanken betrachtet. Die Idee der q-hierarchischen Anfragen (und t-hierarchische Anfragen für das Testen) wird eingeführt und es wird gezeigt, dass das Resultat für jede q-hierarchische Anfrage auf dynamischen Datenbanken effizient in dem oben beschriebenen Szenario ausgewertet werden können. Konjunktive Anfragen mit Aggregaten werden weiterhin betrachtet. Es wird gezeigt, dass das Lernen von polynomiellen Regressionsfunktionen in konstanter Zeit vorbereitet werden kann, falls die Trainingsdaten aus dem Anfrageergebnis kommen. Mit logarithmischer Update-Zeit kann folgende Routine unterstützt werden: Bei Eingabe einer Zahl j, gebe das j-te Tupel aus der Aufzählung aus. Im zweiten Teil werden Anfragen, die Formeln der Logik erster Stufe (FO) und deren Erweiterung mit Modulo-Zähl Quantoren (FO+MOD) sind, betrachtet, und es wird gezeigt, dass diese effizient unter Aktualisierungen ausgewertet können, wobei die dynamische Datenbank die Gradschranke nicht überschreitet, und bei der Auswertung die Zähl-, Test-, Aufzähl- und die Unterschied-Routine unterstützt werden. / This thesis investigates the query evaluation problem for fixed queries over fully dynamic databases, where tuples can be inserted or deleted. The task is to design a dynamic algorithm that immediately reports the new result of a fixed query after every database update. In particular, the goal is to construct a data structure that allows to support the following scenario. After every database update, the data structure can be updated in constant time such that afterwards we are able * to test within constant time for a given tuple whether or not it belongs to the query result, * to output the number of tuples in the query result, * to enumerate all tuples in the new query result with constant delay and * to enumerate the difference between the old and the new query result with constant delay. In the first part, conjunctive queries and unions of conjunctive queries on arbitrary relational databases are considered. The notion of q-hierarchical conjunctive queries (and t-hierarchical conjunctive queries for testing) is introduced and it is shown that the result of each such query on a dynamic database can be maintained efficiently in the sense described above. Moreover, this notion is extended to aggregate queries. It is shown that the preparation of learning a polynomial regression function can be done in constant time if the training data are taken (and maintained under updates) from the query result of a q-hierarchical query. With logarithmic update time the following routine is supported: upon input of a natural number j, output the j-th tuple that will be enumerated. In the second part, queries in first-order logic (FO) and its extension with modulo-counting quantifiers (FO+MOD) are considered, and it is shown that they can be efficiently evaluated under updates, provided that the dynamic database does not exceed a certain degree bound, and the counting, testing, enumeration and difference routines is supported.

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}). / Let p be a prime number. This thesis is a contribution to the theory of mod p representations of p-adic reductive groups, which was until now mainly focused on the general linear group GL(n) defined over a non-archimedean local field F complete with respect to a discrete valuation and with finite residue class field of characteristic p. Our work is original as it deals with other groups : we indeed look for a classification of isomorphism classes of modulo p representations of groups formed by the F-points of a connected reductive group defined, quasi-split and of semi-simple rank 1 over F. A special place is devoted to the special linear group SL(2) and to the unramified quasi-split unitary group. In these two cases, we prove that the isomorphism classes of irreducible smooth representations over an algebraically closed field of characteristic p split into two families : supersingular and non-supersingular representations. We give a complete description of non-supersingular representations and prove that supersingularity is equivalent to the notion of supercuspidality that appears in the complex theory. We also make explicit the supersingular representations of SL(2,Q_{p}), what allows us to define a mod p semi-simple local Langlands correspondence that is compatible to the one built by Breuil for GL(2). We then generalize the methods used above to classify the isomorphism classes of non-supercuspidal representations of G(F) for G a connected reductive group which is defined, quasi-split and of semi-simple rank 1 over F. This classification is made up of three pairwise disjoint families : characters, representations of the principal series, and representations of the special series. We finally come back to SL(2) as we give an exhaustive classification of isomorphism classes of simple right modules on the pro-p-Iwahori-Hecke algebra H of SL(2,F). It implies that the map sending a smooth mod p representation of SL(2,F) on its vector space of invariants vectors under the action of the pro-p-Iwahori subgroup induces a bijection between non-supersingular irreducible smooth representations of SL(2,F) and non-supersingular simple right H-modules. This bijection extends to supersingular objects when F = Q_{p}, what is the first step in the search for an equivalence of categories similar to the one built by Ollivier in the setting of mod p representations of GL(2, Q_{p}).

This thesis tackles the problem of automatically proving the validity of mathematical formulas generated by program verification tools. In particular, it focuses on Satisfiability Modulo Theories (SMT): a young research topic that has seen great advances during the last decade. The solvers of this family have various applications in hardware design, program verification, model checking, etc.SMT solvers offer a good compromise between expressiveness and efficiency. They rely on a tight cooperation between a SAT solver and a combination of decision procedures for specific theories, such as the free theory of equality with uninterpreted symbols, linear arithmetic over integers and rationals, or the theory of arrays.This thesis aims at improving the efficiency and the expressiveness of the Alt-Ergo SMT solver. For that, we designed a new decision procedure for the theory of linear integer arithmetic. This procedure is inspired by Fourier-Motzkin's method, but it uses a rational simplex to perform computations in practice. We have also designed a new combination framework, capable of reasoning in the union of the free theory of equality, the AC theory of associative and commutativesymbols, and an arbitrary signature-disjoint Shostak theory. This framework is a modular and non-intrusive extension of the ground AC completion procedure with the given Shostak theory. In addition, we have extended Alt-Ergo with existing decision procedures to integrate additional interesting theories, such as the theory of enumerated data types and the theory of arrays. Finally, we have explored preprocessing techniques for formulas simplification as well as the enhancement of Alt-Ergo's SAT solver.

This paper proposes two new topological arrangements consisting in connecting the AC power supply in series with two DC converters, one operating during the positive half-cycle and the other during the negative half cycle. It is noteworthy that these DC converters in series in a case are Buck EIE converters and on the other a buck. The results obtained with both arrangements are analyzed and compared. The control strategy is developed with the goal of imposing an AC voltage output within the limits imposed by the rules in order to mitigate the problems associated with Sags and Swells from the AC power supply . The principles of operation as well as the experimental and simulation results obtained in both steady and transient state are presented and validated for a 1kVA experimental prototype. Finally, some works still on progress related to this dissertation are presented, like the multilevel compensation and the three phase compensation. / Este trabalho propõe dois novos arranjos topológicos que consistem em se conectar a alimentação CA em série com dois conversores CC, um para operar durante o semiciclo positivo e o outro durante o semiciclo negativo. Vale ressaltar que estes conversores CC em série, em um caso são conversores Buck EIE e no outro um conversor Buck. Os resultados obtidos com ambos os arranjos são analisados e comparados. A estratégia de controle é desenvolvida com o intuito de impor uma tensão de saída CA dentro dos limites impostos pelas normas de forma a mitigar os problemas associados com Sags e Swells da rede de alimentação CA. Os princípios de operação, os resultados experimentais e de simulação obtidos, tanto em regime permanente quanto em condições transitórias de operação, são apresentados e validados para um protótipo experimental de 1kVA. Por fim apresentam-se os trabalhos relacionados a esta dissertação que ainda estão em desenvolvimento, que são a compensação em multinível e a compensação trifásica. / Mestre em Ciências

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / This work deals with the analysis applied to the main methodologies found in literature for estimating the properties related to the physical phenomena in photovoltaic devices (parametrization), as well as the most important mathematical models used in the calculation of operating electrical characteristics of these devices (characterization). These devices are related to the mono and multi-junction technologies, when they are exposed to a condition where the temperature and solar radiation vary. Therefore, four parametrization methods were shown, including three analytical, and five models of electrical characterization, where two of them are specifically for multi-junction devices. Thus, several case studies were proposed which defined different situations for comparing the performance of the methods evaluated. In this way, the procedures that best fit to each type of photovoltaic technology were identified. Finally, according to the results obtained in the parameterization, the method based on the Generalized Reduced Gradient (GRG) nonlinear algorithm showed greater accuracy for all case studies and for all photovoltaic devices. As for the characterization, the main advantages and disadvantages of all models were determined, highlighting Domínguez, et al. (2010) model, due to the highest robustness and wide application range. / Esta dissertação apresenta uma análise aplicada às principais metodologias encontradas na literatura que permitem determinar as propriedades físicas relativas aos fenômenos que ocorrem nos dispositivos fotovoltaicos (etapa de parametrização), assim como dos modelos matemáticos de maior importância utilizados no cálculo das características elétricas operacionais destes dispositivos (etapa de caraterização). Tais dispositivos referem-se às tecnologias mono e multi junção quando submetidos à variações de temperatura e radiação solar. Portanto, foram apresentados quatro métodos de parametrização, entre eles três analíticos e cinco modelos de caracterização elétrica, sendo dois especificamente para dispositivos multi junção. Assim, estabeleceram-se vários estudos de caso para os quais foram definidas diferentes situações que permitiram comparar o desempenho de cada um dos métodos avaliados. Em consequência, foram identificados os procedimentos que melhor se ajustaram a cada tipo de tecnologia fotovoltaica. Dessa forma, de acordo com os resultados obtidos na parametrização, a metodologia baseada na aplicação do algoritmo de Gradiente Reduzido Generalizado (GRG) não linear, demonstrou maior exatidão para todos os estudos de caso e para todos os dispositivos fotovoltaicos. Já para a caraterização, foram determinadas as principais vantagens e desvantagens entre os modelos aplicados, destacando o modelo de Domínguez, et al. (2010), que apresentou maior robustez e ampla faixa de aplicação. / Mestre em Engenharia Mecânica

No description available.

Normalformen drücken semantische Eigenschaften einer Logik durch syntaktische Restriktionen aus. Sie ermöglichen es Algorithmen, Grenzen der Ausdrucksstärke einer Logik auszunutzen. Ein Beispiel ist die Lokalität der Logik erster Stufe (FO), die impliziert, dass Graph-Eigenschaften wie Erreichbarkeit oder Zusammenhang nicht FO-definierbar sind. Gaifman-Normalformen drücken die Bedeutung einer FO-Formel als Boolesche Kombination lokaler Eigenschaften aus. Sie haben eine wichtige Rolle in Model-Checking Algorithmen für Klassen dünn besetzter Graphen, deren Laufzeit durch die Größe der auszuwertenden Formel parametrisiert ist. Es ist jedoch bekannt, dass Gaifman-Normalformen im Allgemeinen nur mit nicht-elementarem Aufwand konstruiert werden können. Dies führt zu einer enormen Parameterabhängigkeit der genannten Algorithmen. Ähnliche nicht-elementare untere Schranken sind auch für Feferman-Vaught-Zerlegungen und für die Erhaltungssätze von Lyndon, Łoś und Tarski bekannt. Diese Arbeit untersucht die Komplexität der genannten Normalformen auf Klassen von Strukturen beschränkten Grades, für welche die nicht-elementaren unteren Schranken nicht gelten. Für diese Einschränkung werden Algorithmen mit elementarer Laufzeit für die Konstruktion von Gaifman-Normalformen, Feferman-Vaught-Zerlegungen, und für die Erhaltungssätze von Lyndon, Łoś und Tarski entwickelt, die in den ersten beiden Fällen worst-case optimal sind. Wichtig hierfür sind Hanf-Normalformen. Es wird gezeigt, dass eine Erweiterung von FO durch unäre Zählquantoren genau dann Hanf-Normalformen erlaubt, wenn alle Zählquantoren ultimativ periodisch sind, und wie Hanf-Normalformen in diesen Fällen in elementarer und worst-case optimaler Zeit konstruiert werden können. Dies führt zu Model-Checking Algorithmen für solche Erweiterungen von FO sowie zu Verallgemeinerungen der Algorithmen für Feferman-Vaught-Zerlegungen und die Erhaltungssätze von Lyndon, Łoś und Tarski. / Normal forms express semantic properties of logics by means of syntactical restrictions. They allow algorithms to benefit from restrictions of the expressive power of a logic. An example is the locality of first-order logic (FO), which implies that properties like reachability or connectivity cannot be defined in FO. Gaifman's local normal form expresses the satisfaction conditions of an FO-formula by a Boolean combination of local statements. Gaifman normal form serves as a first step in fixed-parameter model-checking algorithms, parameterised by the size of the formula, on sparse graph classes. However, it is known that in general, there are non-elementary lower bounds for the costs involved in transforming a formula into Gaifman normal form. This leads to an enormous parameter-dependency of the aforementioned algorithms. Similar non-elementary lower bounds also hold for Feferman-Vaught decompositions and for the preservation theorems by Lyndon, Łoś, and Tarski. This thesis investigates the complexity of these normal forms when restricting attention to classes of structures of bounded degree, for which the non-elementary lower bounds are known to fail. Under this restriction, the thesis provides algorithms with elementary and even worst-case optimal running time for the construction of Gaifman normal form and Feferman-Vaught decompositions. For the preservation theorems, algorithmic versions with elementary running time and non-matching lower bounds are provided. Crucial for these results is the notion of Hanf normal form. It is shown that an extension of FO by unary counting quantifiers allows Hanf normal forms if, and only if, all quantifiers are ultimately periodic, and furthermore, how Hanf normal form can be computed in elementary and worst-case optimal time in these cases. This leads to model-checking algorithms for such extensions of FO and also allows generalisations of the constructions for Feferman-Vaught decompositions and preservation theorems.

[pt] Ésteres de glicerol derivados de ácidos graxos são surfactantes não iônicos com aplicação como lubrificantes, agentes anti-estáticos, auxiliares de processamento, plastificantes, anti-espumas, agentes de dispersão e de outras aplicações que requerem atividade bifuncional. Os monoésteres de glicerol derivados de ácidos graxos naturais, tais como ácido octanóico (C menos 8), decanóico (C menos 10) e octadecanóico (C menos 18), foram sintetizados e caracterizados por técnicas de infravermelho e ressonância magnética nuclear de hidrogênio e carbono 13. Eles foram espalhados sobre uma subfase aquosa formando filmes de Langmuir em uma cuba de teflon. As propriedades interfaciais destes surfactantes foram investigadas na interface ar-água. Desta forma, foi também possível avaliar a isoterma de Langmuir Pi-A e as propriedades mecânicas das monocamadas através do módulo de compressão (Cs elevado a potencia negativa 1). As monocamadas mostraram um comportamento na fase de líquido expandido confirmado pelo módulo de compressão de 10 a 70 mN/m e na fase de líquido condensado confirmado pelo módulo de compressão de 70 a 175 mN/m. Por meio da espectroscopia de reflexão-absorção de infravermelho com fotomodulação (PM-IRRAS) e a microscopia no ângulo de Brewster (BAM) foi avaliada a organização dos filmes de Langmuir dos surfactantes. A elasticidade superficial dilatacional (E) dos filmes adsorvidos foram analisadas pelo método da gota pendente em um goniômetro. / [en] Fatty acid glycerol esters are non-ionic surfactants with application as lubricants, antistatic agents, processing aids, plasticizers, defoamers, dispersion aids and other applications requiring bifunctional activities. Monoesters of glycerol based on natural fatty acids such as octanoic acid (C less 8), decanoic acid (C less 10) and octadecanoic acid (C less 18), were synthesized and characterized by infrared and hydrogen nuclear magnetic resonance and carbon 13 nuclear magnetic resonance techniques. They were spread over the water subphase forming Langmuir films in a Teflon trough. The interfacial properties of these surfactants at the air/water interface have been investigated. Thus it was also possible to evaluate the Langmuir Pi-A isotherm and mechanical properties of the monolayers by calculating the compression modulus (Cs elevated to negative power 1). The monolayers showed a behavior in the expanded liquid phase, confirmed by the compression modulus between 10 and 70 mN/m and a behavior in the condensed liquid phase confirmed by the compression modulus between 70 and 175 mN/m. Through photomodulated-infrared reflection-absorption spectroscopy (PM-IRRAS) and Brewster angle microscopy (BAM) was evaluated organization of Langmuir films of surfactants. The surface dilatational elasticity (E) of the adsorbed films were analyzed by the pendant drop method with a goniometer apparatus.