Robust Learning Control for Manipulators with Uncertainty Disturbances Based on Internal Model

In this paper, a disturbance controller is designed for making robotic system behave as a decoupled linear system according to the concept of internal model. Based on the linear system, the paper presents an iterative learning control algorithm to robotic manipulators. A sufficient condition for convergence is provided. The selection of parameter values of the algorithm is simple and easy to meet the convergence condition. The simulation results demonstrate the effectiveness of the algorithm..

基于点集曲面投影算法的自由曲面匹配

测量数据的精确定位是实现复杂曲面加工检测的关键,针对测量点云数据与NURBS表示的CAD自由曲面模型匹配中求最近点计算方面存在的问题,提出了一种简单、有效的寻找最近点的方法。该方法与由测量点集评估给定曲面上的最近点的传统算法相反,采用点集曲面(point set surface,PSS)投影算法,对给定自由曲面模型上有限个点与不附加任何几何和拓扑信息的散乱点集之间进行粗匹配获得初始位置,进而以最近点迭代算法(ICP)完成测量数据定位的精确调整,达到全局及局部最优的目标。实验结果表明,采用PSS投影算法法寻找最近点不仅效率高,而且能得到全局匹配结果,可以为精匹配提供较好的计算初值,减少了ICP算法进行二次匹配时,迭代次数及执行时间并且精度得到了较大提高。

Optimisation du processus de développement du médicament grâce à la modélisation PK et les simulations d’études cliniques

Le développement d’un médicament est non seulement complexe mais les retours sur investissment ne sont pas toujours ceux voulus ou anticipés. Plusieurs médicaments échouent encore en Phase III même avec les progrès technologiques réalisés au niveau de plusieurs aspects du développement du médicament. Ceci se traduit en un nombre décroissant de médicaments qui sont commercialisés. Il faut donc améliorer le processus traditionnel de développement des médicaments afin de faciliter la disponibilité de nouveaux produits aux patients qui en ont besoin. Le but de cette recherche était d’explorer et de proposer des changements au processus de développement du médicament en utilisant les principes de la modélisation avancée et des simulations d’essais cliniques. Dans le premier volet de cette recherche, de nouveaux algorithmes disponibles dans le logiciel ADAPT 5® ont été comparés avec d’autres algorithmes déjà disponibles afin de déterminer leurs avantages et leurs faiblesses. Les deux nouveaux algorithmes vérifiés sont l’itératif à deux étapes (ITS) et le maximum de vraisemblance avec maximisation de l’espérance (MLEM). Les résultats de nos recherche ont démontré que MLEM était supérieur à ITS. La méthode MLEM était comparable à l’algorithme d’estimation conditionnelle de premier ordre (FOCE) disponible dans le logiciel NONMEM® avec moins de problèmes de rétrécissement pour les estimés de variances. Donc, ces nouveaux algorithmes ont été utilisés pour la recherche présentée dans cette thèse. Durant le processus de développement d’un médicament, afin que les paramètres pharmacocinétiques calculés de façon noncompartimentale soient adéquats, il faut que la demi-vie terminale soit bien établie. Des études pharmacocinétiques bien conçues et bien analysées sont essentielles durant le développement des médicaments surtout pour les soumissions de produits génériques et supergénériques (une formulation dont l'ingrédient actif est le même que celui du médicament de marque, mais dont le profil de libération du médicament est différent de celui-ci) car elles sont souvent les seules études essentielles nécessaires afin de décider si un produit peut être commercialisé ou non. Donc, le deuxième volet de la recherche visait à évaluer si les paramètres calculer d’une demi-vie obtenue à partir d'une durée d'échantillonnage réputée trop courte pour un individu pouvaient avoir une incidence sur les conclusions d’une étude de bioéquivalence et s’ils devaient être soustraits d’analyses statistiques. Les résultats ont démontré que les paramètres calculer d’une demi-vie obtenue à partir d'une durée d'échantillonnage réputée trop courte influençaient de façon négative les résultats si ceux-ci étaient maintenus dans l’analyse de variance. Donc, le paramètre de surface sous la courbe à l’infini pour ces sujets devrait être enlevé de l’analyse statistique et des directives à cet effet sont nécessaires a priori. Les études finales de pharmacocinétique nécessaires dans le cadre du développement d’un médicament devraient donc suivre cette recommandation afin que les bonnes décisions soient prises sur un produit. Ces informations ont été utilisées dans le cadre des simulations d’essais cliniques qui ont été réalisées durant la recherche présentée dans cette thèse afin de s’assurer d’obtenir les conclusions les plus probables. Dans le dernier volet de cette thèse, des simulations d’essais cliniques ont amélioré le processus du développement clinique d’un médicament. Les résultats d’une étude clinique pilote pour un supergénérique en voie de développement semblaient très encourageants. Cependant, certaines questions ont été soulevées par rapport aux résultats et il fallait déterminer si le produit test et référence seraient équivalents lors des études finales entreprises à jeun et en mangeant, et ce, après une dose unique et des doses répétées. Des simulations d’essais cliniques ont été entreprises pour résoudre certaines questions soulevées par l’étude pilote et ces simulations suggéraient que la nouvelle formulation ne rencontrerait pas les critères d’équivalence lors des études finales. Ces simulations ont aussi aidé à déterminer quelles modifications à la nouvelle formulation étaient nécessaires afin d’améliorer les chances de rencontrer les critères d’équivalence. Cette recherche a apporté des solutions afin d’améliorer différents aspects du processus du développement d’un médicament. Particulièrement, les simulations d’essais cliniques ont réduit le nombre d’études nécessaires pour le développement du supergénérique, le nombre de sujets exposés inutilement au médicament, et les coûts de développement. Enfin, elles nous ont permis d’établir de nouveaux critères d’exclusion pour des analyses statistiques de bioéquivalence. La recherche présentée dans cette thèse est de suggérer des améliorations au processus du développement d’un médicament en évaluant de nouveaux algorithmes pour des analyses compartimentales, en établissant des critères d’exclusion de paramètres pharmacocinétiques (PK) pour certaines analyses et en démontrant comment les simulations d’essais cliniques sont utiles.

Attribute reduction and missing value imputing with ANN: prediction of learning disabilities

Learning disability (LD) is a neurological condition that affects a child’s brain and impairs his ability to carry out one or many specific tasks. LD affects about 10% of children enrolled in schools. There is no cure for learning disabilities and they are lifelong. The problems of children with specific learning disabilities have been a cause of concern to parents and teachers for some time. Just as there are many different types of LDs, there are a variety of tests that may be done to pinpoint the problem The information gained from an evaluation is crucial for finding out how the parents and the school authorities can provide the best possible learning environment for child. This paper proposes a new approach in artificial neural network (ANN) for identifying LD in children at early stages so as to solve the problems faced by them and to get the benefits to the students, their parents and school authorities. In this study, we propose a closest fit algorithm data preprocessing with ANN classification to handle missing attribute values. This algorithm imputes the missing values in the preprocessing stage. Ignoring of missing attribute values is a common trend in all classifying algorithms. But, in this paper, we use an algorithm in a systematic approach for classification, which gives a satisfactory result in the prediction of LD. It acts as a tool for predicting the LD accurately, and good information of the child is made available to the concerned

Learning disability prediction tool using ANN and ANFIS

Learning Disability (LD) is a neurological condition that affects a child’s brain and impairs his ability to carry out one or many specific tasks. LD affects about 15 % of children enrolled in schools. The prediction of LD is a vital and intricate job. The aim of this paper is to design an effective and powerful tool, using the two intelligent methods viz., Artificial Neural Network and Adaptive Neuro-Fuzzy Inference System, for measuring the percentage of LD that affected in school-age children. In this study, we are proposing some soft computing methods in data preprocessing for improving the accuracy of the tool as well as the classifier. The data preprocessing is performed through Principal Component Analysis for attribute reduction and closest fit algorithm is used for imputing missing values. The main idea in developing the LD prediction tool is not only to predict the LD present in children but also to measure its percentage along with its class like low or minor or major. The system is implemented in Mathworks Software MatLab 7.10. The results obtained from this study have illustrated that the designed prediction system or tool is capable of measuring the LD effectively

Estudi i implementació d’un mètode de reconstrucció 3D basat en SfM i registre de vistes 3D parcials

Aquest projecte es basarà en reconstruir una imatge 3D gran a partir d’una seqüència d’imatges 2D capturades per una càmera. Ens centrem en l’estudi de les bases matemàtiques de la visió per computador així com en diferents mètodes emprats en la reconstrucció 3D d’imatges. Per portar a terme aquest estudi s’utilitza la plataforma de desenvolupament MatLab ja que permet tractar operacions matemàtiques, imatges i matrius de gran tamany amb molta senzillesa, rapidesa i eficiència, per aquesta raó s’usa en moltes recerques sobre aquest tema. El projecte aprofundeix en el tema descrit anteriorment estudiant i implementant un mètode que consisteix en aplicar Structure From Motion (SFM) a pocs frames seguits obtinguts d’una seqüència d’imatges 2D per crear una reconstrucció 3D. Quan s’han creat dues reconstruccions 3D consecutives i fent servir un frame com a mínim en comú entre elles, s’aplica un mètode de registre d’estructures 3D, l’Iterative Closest Point (ICP), per crear una reconstrucció 3D més gran a través d’unir les diferents reconstruccions obtingudes a partir de SfM. El mètode consisteix en anar repetint aquestes operacions fins al final dels frames per poder aconseguir una reconstrucció 3D més gran que les petites imatges que s’aconsegueixen a través de SfM. A la Figura 1 es pot veure un esquema del procés que es segueix. Per avaluar el comportament del mètode, utilitzem un conjunt de seqüències sintètiques i un conjunt de seqüències reals obtingudes a partir d’una càmera. L’objectiu final d’aquest projecte és construir una nova toolbox de MatLab amb tots els mètodes per crear reconstruccions 3D grans per tal que sigui possible tractar amb facilitat aquest problema i seguir-lo desenvolupant en un futur

Proximal methods for nonlinear programming: double regularization and inexact subproblems

This paper describes the first phase of a project attempting to construct an efficient general-purpose nonlinear optimizer using an augmented Lagrangian outer loop with a relative error criterion, and an inner loop employing a state-of-the art conjugate gradient solver. The outer loop can also employ double regularized proximal kernels, a fairly recent theoretical development that leads to fully smooth subproblems. We first enhance the existing theory to show that our approach is globally convergent in both the primal and dual spaces when applied to convex problems. We then present an extensive computational evaluation using the CUTE test set, showing that some aspects of our approach are promising, but some are not. These conclusions in turn lead to additional computational experiments suggesting where to next focus our theoretical and computational efforts.

A Robust, Fully Adaptive Hybrid Level-Set/Front-Tracking Method for Two-Phase Flows with an Accurate Surface Tension Computation

We present a variable time step, fully adaptive in space, hybrid method for the accurate simulation of incompressible two-phase flows in the presence of surface tension in two dimensions. The method is based on the hybrid level set/front-tracking approach proposed in [H. D. Ceniceros and A. M. Roma, J. Comput. Phys., 205, 391400, 2005]. Geometric, interfacial quantities are computed from front-tracking via the immersed-boundary setting while the signed distance (level set) function, which is evaluated fast and to machine precision, is used as a fluid indicator. The surface tension force is obtained by employing the mixed Eulerian/Lagrangian representation introduced in [S. Shin, S. I. Abdel-Khalik, V. Daru and D. Juric, J. Comput. Phys., 203, 493-516, 2005] whose success for greatly reducing parasitic currents has been demonstrated. The use of our accurate fluid indicator together with effective Lagrangian marker control enhance this parasitic current reduction by several orders of magnitude. To resolve accurately and efficiently sharp gradients and salient flow features we employ dynamic, adaptive mesh refinements. This spatial adaption is used in concert with a dynamic control of the distribution of the Lagrangian nodes along the fluid interface and a variable time step, linearly implicit time integration scheme. We present numerical examples designed to test the capabilities and performance of the proposed approach as well as three applications: the long-time evolution of a fluid interface undergoing Rayleigh-Taylor instability, an example of bubble ascending dynamics, and a drop impacting on a free interface whose dynamics we compare with both existing numerical and experimental data.

Multi-areas optimal reactive power flow

This paper describes a method for the decentralized solution of the optimal reactive power flow (ORPF) problem in interconnected power systems. The ORPF model is solved in a decentralized framework, consisting of regions, where the transmission system operator in each area operates its system independently of the other areas, obtaining an optimal coordinated but decentralized solution. The proposed scheme is based on an augmented Lagrangian approach using the auxiliary problem principle (APP). An implementation of an interior point method is described to solve the decoupled problem in each area. The described method is successfully implemented and tested using the IEEE two area RTS 96 test system. Numerical results comparing the solutions obtained by the traditional and the proposed decentralized methods are presented for validation. ©2008 IEEE.

Dessecação com Glyphosate em pré-colheita e qualidade fisiológica de sementes de soja

Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq)

Uma investigação da influência do parâmetro de barreira na solução do problema de fluxo de potência ótimo

Pós-graduação em Engenharia Elétrica - FEB

Hybrid heuristic-waterfilling game theory approach in MC-CDMA resource allocation

This paper discusses the power allocation with fixed rate constraint problem in multi-carrier code division multiple access (MC-CDMA) networks, that has been solved through game theoretic perspective by the use of an iterative water-filling algorithm (IWFA). The problem is analyzed under various interference density configurations, and its reliability is studied in terms of solution existence and uniqueness. Moreover, numerical results reveal the approach shortcoming, thus a new method combining swarm intelligence and IWFA is proposed to make practicable the use of game theoretic approaches in realistic MC-CDMA systems scenarios. The contribution of this paper is twofold: (i) provide a complete analysis for the existence and uniqueness of the game solution, from simple to more realist and complex interference scenarios; (ii) propose a hybrid power allocation optimization method combining swarm intelligence, game theory and IWFA. To corroborate the effectiveness of the proposed method, an outage probability analysis in realistic interference scenarios, and a complexity comparison with the classical IWFA are presented. (C) 2011 Elsevier B.V. All rights reserved.

Soft-decision equalization techniques for frequency selective MIMO channels

Multi-input multi-output (MIMO) technology is an emerging solution for high data rate wireless communications. We develop soft-decision based equalization techniques for frequency selective MIMO channels in the quest for low-complexity equalizers with BER performance competitive to that of ML sequence detection. We first propose soft decision equalization (SDE), and demonstrate that decision feedback equalization (DFE) based on soft-decisions, expressed via the posterior probabilities associated with feedback symbols, is able to outperform hard-decision DFE, with a low computational cost that is polynomial in the number of symbols to be recovered, and linear in the signal constellation size. Building upon the probabilistic data association (PDA) multiuser detector, we present two new MIMO equalization solutions to handle the distinctive channel memory. With their low complexity, simple implementations, and impressive near-optimum performance offered by iterative soft-decision processing, the proposed SDE methods are attractive candidates to deliver efficient reception solutions to practical high-capacity MIMO systems. Motivated by the need for low-complexity receiver processing, we further present an alternative low-complexity soft-decision equalization approach for frequency selective MIMO communication systems. With the help of iterative processing, two detection and estimation schemes based on second-order statistics are harmoniously put together to yield a two-part receiver structure: local multiuser detection (MUD) using soft-decision Probabilistic Data Association (PDA) detection, and dynamic noise-interference tracking using Kalman filtering. The proposed Kalman-PDA detector performs local MUD within a sub-block of the received data instead of over the entire data set, to reduce the computational load. At the same time, all the inter-ference affecting the local sub-block, including both multiple access and inter-symbol interference, is properly modeled as the state vector of a linear system, and dynamically tracked by Kalman filtering. Two types of Kalman filters are designed, both of which are able to track an finite impulse response (FIR) MIMO channel of any memory length. The overall algorithms enjoy low complexity that is only polynomial in the number of information-bearing bits to be detected, regardless of the data block size. Furthermore, we introduce two optional performance-enhancing techniques: cross- layer automatic repeat request (ARQ) for uncoded systems and code-aided method for coded systems. We take Kalman-PDA as an example, and show via simulations that both techniques can render error performance that is better than Kalman-PDA alone and competitive to sphere decoding. At last, we consider the case that channel state information (CSI) is not perfectly known to the receiver, and present an iterative channel estimation algorithm. Simulations show that the performance of SDE with channel estimation approaches that of SDE with perfect CSI.

Proceedings of the Twenty-Sixth Annual Biochemical Engineering Symposium

This volume contains the Proceedings of the Twenty-Sixth Annual Biochemical Engineering Symposium held at Kansas State University on September 21, 1996. The program included 10 oral presentations and 14 posters. Some of the papers describe the progress of ongoing projects, and others contain the results of completed projects. Only brief summaries are given of some of the papers; many of the papers will be published in full elsewhere. A listing of those who attended is given below. ContentsForeign Protein Production from SV40 Early Promoter in Continuous Cultures of Recombinant CHO Cells - Gautam Banik, Paul Todd, and Dhinakar Kampala Enhanced Cell Recruitment Due to Cell-Cell Interactions - Brad Farlow and Matthias Nollert The Recirculation of Hybridoma Suspension Cultures: Effects on Cell Death, Metabolism and Mab Productivity - Peng Jin and Carole A. Heath The Importance of Enzyme Inactivation and Self-Recovery in Cometabolic Biodegradation of Chlorinated Solvents - Xi-Hui Zhang, Shanka Banerji, and Rakesh Bajpai Phytoremediation of VOC contaminated Groundwater using Poplar Trees - Melissa Miller, Jason Dana, L.C. Davis, Murlidharan Narayanan, and L.E. Erickson Biological Treatment of Off-Gases from Aluminum Can Production: Experimental Results and Mathematical Modeling - Adeyma Y. Arroyo, Julio Zimbron, and Kenneth F. Reardon Inertial Migration Based Separation of Chlorella Microalgae in Branched Tubes - N.M. Poflee, A.L. Rakow, D.S. Dandy, M.L. Chappell, and M.N. Pons Contribution of Electrochemical Charge to Protein Partitioning in Aqueous Two-Phase Systems - Weiyu Fan and Charles C. Glatz Biodegradation of Some Commercial Surfactants Used in Bioremediation - Jun Gu, G.W. Preckshot, S.K. Banerji, and Rakesh Bajpai Modeling the Role of Biomass in Heavy Metal Transport Ln Vadose Zone - K.V. Nedunuri, L.E. Erickson, and R.S. Govindaraju Multivariable Statistical Methods for Monitoring Process Quality: Application to Bioinsecticide Production by 73 89 Bacillus Thuringiensis - c. Puente and M.N. Karim The Use of Polymeric Flocculants in Bacterial Lysate Streams - H. Graham, A.S. Cibulskas and E.H. Dunlop Effect of Water Content on transport of Trichloroethylene in a Chamber with Alfalfa Plants - Muralidharan Narayanan, Jiang Hu, Lawrence C. Davis, and Larry E. Erickson Detection of Specific Microorganisms using the Arbitrary Primed PCR in the Bacterial Community of Vegetated Soil - X. Wu and L.C. Davis Flux Enhancement Using Backpulsing - V.T. Kuberkar and R.H. Davis Chromatographic Purification of Oligonucleotides: Comparison with Electrophoresis - Stephen P. Cape, Ching-Yuan Lee, Kevin Petrini, Sean Foree, Micheal G. Sportiello and Paul Todd Determining Singular Arc Control Policies for Bioreactor Systems Using a Modified Iterative Dynamic Programming Algorithm - Arun Tholudur and W. Fred Ramirez Pressure Effect on Subtilisins Measured via FTIR, EPR and Activity Assays, and Its Impact on Crystallizations - J.N. Webb, R.Y. Waghmare, M.G. Bindewald, T.W. Randolph, J.F. Carpenter, C.E. Glatz Intercellular Calcium Changes in Endothelial Cells Exposed to Flow - Laura Worthen and Matthias Nollert Application of Liquid-Liquid Extraction in Propionic Acid Fermentation - Zhong Gu, Bonita A. Glatz, and Charles E. Glatz Purification of Recombinant T4 Lysozyme from E. Coli: Ion-Exchange Chromatography - Weiyu Fan, Matt L. Thatcher, and Charles E. Glatz Recovery and Purification of Recombinant Beta-Glucuronidase from Transgenic Corn - Ann R. Kusnadi, Roque Evangelista, Zivko L. Nikolov, and John Howard Effects of Auxins and cytokinins on Formation of Catharanthus Roseus G. Don Multiple Shoots - Ying-Jin Yuan, Yu-Min Yang, Tsung-Ting Hu, and Jiang Hu Fate and Effect of Trichloroethylene as Nonaqueous Phase Liquid in Chambers with Alfalfa - Qizhi Zhang, Brent Goplen, Sara Vanderhoof, Lawrence c. Davis, and Larry E. Erickson Oxygen Transport and Mixing Considerations for Microcarrier Culture of Mammalian Cells in an Airlift Reactor - Sridhar Sunderam, Frederick R. Souder, and Marylee Southard Effects of Cyclic Shear Stress on Mammalian Cells under Laminar Flow Conditions: Apparatus and Methods - M.L. Rigney, M.H. Liew, and M.Z. Southard

Advanced Topics in Resource Analysis: Certification, Incrementality, Concurrency and Array-Sensitivity

El Análisis de Consumo de Recursos o Análisis de Coste trata de aproximar el coste de ejecutar un programa como una función dependiente de sus datos de entrada. A pesar de que existen trabajos previos a esta tesis doctoral que desarrollan potentes marcos para el análisis de coste de programas orientados a objetos, algunos aspectos avanzados, como la eficiencia, la precisión y la fiabilidad de los resultados, todavía deben ser estudiados en profundidad. Esta tesis aborda estos aspectos desde cuatro perspectivas diferentes: (1) Las estructuras de datos compartidas en la memoria del programa son una pesadilla para el análisis estático de programas. Trabajos recientes proponen una serie de condiciones de localidad para poder mantener de forma consistente información sobre los atributos de los objetos almacenados en memoria compartida, reemplazando éstos por variables locales no almacenadas en la memoria compartida. En esta tesis presentamos dos extensiones a estos trabajos: la primera es considerar, no sólo los accesos a los atributos, sino también los accesos a los elementos almacenados en arrays; la segunda se centra en los casos en los que las condiciones de localidad no se cumplen de forma incondicional, para lo cual, proponemos una técnica para encontrar las precondiciones necesarias para garantizar la consistencia de la información acerca de los datos almacenados en memoria. (2) El objetivo del análisis incremental es, dado un programa, los resultados de su análisis y una serie de cambios sobre el programa, obtener los nuevos resultados del análisis de la forma más eficiente posible, evitando reanalizar aquellos fragmentos de código que no se hayan visto afectados por los cambios. Los analizadores actuales todavía leen y analizan el programa completo de forma no incremental. Esta tesis presenta un análisis de coste incremental, que, dado un cambio en el programa, reconstruye la información sobre el coste del programa de todos los métodos afectados por el cambio de forma incremental. Para esto, proponemos (i) un algoritmo multi-dominio y de punto fijo que puede ser utilizado en todos los análisis globales necesarios para inferir el coste, y (ii) una novedosa forma de almacenar las expresiones de coste que nos permite reconstruir de forma incremental únicamente las funciones de coste de aquellos componentes afectados por el cambio. (3) Las garantías de coste obtenidas de forma automática por herramientas de análisis estático no son consideradas totalmente fiables salvo que la implementación de la herramienta o los resultados obtenidos sean verificados formalmente. Llevar a cabo el análisis de estas herramientas es una tarea titánica, ya que se trata de herramientas de gran tamaño y complejidad. En esta tesis nos centramos en el desarrollo de un marco formal para la verificación de las garantías de coste obtenidas por los analizadores en lugar de analizar las herramientas. Hemos implementado esta idea mediante la herramienta COSTA, un analizador de coste para programas Java y KeY, una herramienta de verificación de programas Java. De esta forma, COSTA genera las garantías de coste, mientras que KeY prueba la validez formal de los resultados obtenidos, generando de esta forma garantías de coste verificadas. (4) Hoy en día la concurrencia y los programas distribuidos son clave en el desarrollo de software. Los objetos concurrentes son un modelo de concurrencia asentado para el desarrollo de sistemas concurrentes. En este modelo, los objetos son las unidades de concurrencia y se comunican entre ellos mediante llamadas asíncronas a sus métodos. La distribución de las tareas sugiere que el análisis de coste debe inferir el coste de los diferentes componentes distribuidos por separado. En esta tesis proponemos un análisis de coste sensible a objetos que, utilizando los resultados obtenidos mediante un análisis de apunta-a, mantiene el coste de los diferentes componentes de forma independiente. Abstract Resource Analysis (a.k.a. Cost Analysis) tries to approximate the cost of executing programs as functions on their input data sizes and without actually having to execute the programs. While a powerful resource analysis framework on object-oriented programs existed before this thesis, advanced aspects to improve the efficiency, the accuracy and the reliability of the results of the analysis still need to be further investigated. This thesis tackles this need from the following four different perspectives. (1) Shared mutable data structures are the bane of formal reasoning and static analysis. Analyses which keep track of heap-allocated data are referred to as heap-sensitive. Recent work proposes locality conditions for soundly tracking field accesses by means of ghost non-heap allocated variables. In this thesis we present two extensions to this approach: the first extension is to consider arrays accesses (in addition to object fields), while the second extension focuses on handling cases for which the locality conditions cannot be proven unconditionally by finding aliasing preconditions under which tracking such heap locations is feasible. (2) The aim of incremental analysis is, given a program, its analysis results and a series of changes to the program, to obtain the new analysis results as efficiently as possible and, ideally, without having to (re-)analyze fragments of code that are not affected by the changes. During software development, programs are permanently modified but most analyzers still read and analyze the entire program at once in a non-incremental way. This thesis presents an incremental resource usage analysis which, after a change in the program is made, is able to reconstruct the upper-bounds of all affected methods in an incremental way. To this purpose, we propose (i) a multi-domain incremental fixed-point algorithm which can be used by all global analyses required to infer the cost, and (ii) a novel form of cost summaries that allows us to incrementally reconstruct only those components of cost functions affected by the change. (3) Resource guarantees that are automatically inferred by static analysis tools are generally not considered completely trustworthy, unless the tool implementation or the results are formally verified. Performing full-blown verification of such tools is a daunting task, since they are large and complex. In this thesis we focus on the development of a formal framework for the verification of the resource guarantees obtained by the analyzers, instead of verifying the tools. We have implemented this idea using COSTA, a state-of-the-art cost analyzer for Java programs and KeY, a state-of-the-art verification tool for Java source code. COSTA is able to derive upper-bounds of Java programs while KeY proves the validity of these bounds and provides a certificate. The main contribution of our work is to show that the proposed tools cooperation can be used for automatically producing verified resource guarantees. (4) Distribution and concurrency are today mainstream. Concurrent objects form a well established model for distributed concurrent systems. In this model, objects are the concurrency units that communicate via asynchronous method calls. Distribution suggests that analysis must infer the cost of the diverse distributed components separately. In this thesis we propose a novel object-sensitive cost analysis which, by using the results gathered by a points-to analysis, can keep the cost of the diverse distributed components separate.