The prevalence, health risks, and consequences of asthma among adult residents in Texas

Based on asthma prevalence data collected from the 2000 BRFSS survey, approximately 14.7 million U.S. adults had current asthma, accounting for 7.2% of the total U.S. population. In Texas alone, state data extrapolated from the 1999-2003 Texas BRFSS suggested that approximately 1 million Texas adults were reporting current asthma and approximately 11% of the adult population has been diagnosed with the illness during their lifetime. From a public health perspective, the disease is manageable. Comprehensive state-specific asthma surveillance data are necessary to identify disparities in asthma prevalence and asthma-control characteristics among subpopulations and to develop targeted public health interventions. The purpose of this study was to determine the relative importance of various risk factors of asthma and to examine the impact of asthma on health-related quality of life among adult residents of Texas. ^ The study employed a cross-sectional study of respondents in Texas. The study extracted all the variables related to asthma along with their associated demographic, socioeconomic, and quality of life variables from the 2007 BRFSS data for 17,248 adult residents of Texas aged 18 and older. Chi-square test and logistic regression using SPSS were used in various data analyses on weighted data, adjusting for the complex sample design of the BRFSS data. All chi-square analyses were carried out using SPSS's CSTABULATE command. In addition, logistic regression models were fitted using SPSS's CSLOGISTIC command. ^ Risks factors significantly associated with reporting current asthma included BMI, race/ethnicity, gender, and income. Holding all other variables constant, obese adults were almost twice as likely to report current asthma as those adults who were normal weight (odds ratio [OR], 1.78; 95% confidence interval [CI], 1.25 to 2.53). Other non-Hispanic adults were significantly more likely to report current asthma than non-Hispanic Whites (OR, 2.43; 95% CI, 1.38 to 4.25), while Hispanics were significantly less likely to report current asthma than non-Hispanic Whites (OR, 0.38; 95% CI, 0.25 to 0.60), after controlling for all other variables. After adjusting for all other variables, adult females were almost twice as likely to report current asthma as males (OR, 1.97; 95% CI, 1.49 to 2.60). Adults with household income of less than $15,000 were almost twice as likely to report current asthma as those persons with an annual household income of $50,000 or more (OR, 1.98; 95% CI, 1.33 to 2.94). In regards to the association between asthma and health-related quality of life, after adjusting for age, race/ethnicity, gender, tobacco use, body mass index (BMI), exercise, education, and income, adults with current asthma compared to those without asthma were more likely to report having more than 15 days of unhealthy physical health (OR, 1.84; 95% CI, 1.29 to 2.60). ^ Overall, the findings of this study provide insight and valuable information into the populations in Texas most adversely affected by asthma and health-related consequences of the disease condition. Further research could build on the findings of this study by replicating this study as closely as possible in other asthma settings, and look at the relationship for hospitalization rates, asthma severity, and mortality.^

Revisiting health literacy and its impact on patient-physician communication

Objective. To review professional literature on health literacy and its impact on patient-physician communication, to describe significant literature on this issue, and to summarize implications of the findings from this literature. Design. Update of a review of literature. Data sources: MEDLINE. Review Methods. Articles dealing with the impact of health literacy on patient-physician communication were selected. The articles addressed at least one of four criteria on the subject: prevalence of the problem; effect of health literacy on patient-physician communication; association of health literacy to health outcomes; and interventions to enhance communication with patients exhibiting limited health literacy. Results. Approximately 623 articles were selected for review; 87 were fully reviewed and found to be relevant to the issue; and 25 articles were cited. Conclusion. Limited health literacy is extremely widespread throughout the U.S., particularly among specific populations. Providers must be aware that patients often process health care decision making differently from their own familiar procedures and that by taking the steps to make medical language and health information simpler and the time to confirm patient understanding, health outcomes of limited health literacy populations will improve. ^

The determinants of improvements in health outcomes and of cost reduction in hospital inpatient care

This study aims to address two research questions. First, ‘Can we identify factors that are determinants both of improved health outcomes and of reduced costs for hospitalized patients with one of six common diagnoses?’ Second, ‘Can we identify other factors that are determinants of improved health outcomes for such hospitalized patients but which are not associated with costs?’ The Healthcare Cost and Utilization Project (HCUP) Nationwide Inpatient Sample (NIS) database from 2003 to 2006 was employed in this study. The total study sample consisted of hospitals which had at least 30 patients each year for the given diagnosis: 954 hospitals for acute myocardial infarction (AMI), 1552 hospitals for congestive heart failure (CHF), 1120 hospitals for stroke (STR), 1283 hospitals for gastrointestinal hemorrhage (GIH), 979 hospitals for hip fracture (HIP), and 1716 hospitals for pneumonia (PNE). This study used simultaneous equations models to investigate the determinants of improvement in health outcomes and of cost reduction in hospital inpatient care for these six common diagnoses. In addition, the study used instrumental variables and two-stage least squares random effect model for unbalanced panel data estimation. The study concluded that a few factors were determinants of high quality and low cost. Specifically, high specialty was the determinant of high quality and low costs for CHF patients; small hospital size was the determinant of high quality and low costs for AMI patients. Furthermore, CHF patients who were treated in Midwest, South, and West region hospitals had better health outcomes and lower hospital costs than patients who were treated in Northeast region hospitals. Gastrointestinal hemorrhage and pneumonia patients who were treated in South region hospitals also had better health outcomes and lower hospital costs than patients who were treated in Northeast region hospitals. This study found that six non-cost factors were related to health outcomes for a few diagnoses: hospital volume, percentage emergency room admissions for a given diagnosis, hospital competition, specialty, bed size, and hospital region.^

Social support, health status and health services utilization among the noninstitutionalized elderly: An analysis of the Supplement on Aging to the 1984 national health interview survey

The association between Social Support, Health Status, and Health Services Utilization of the elderly, was explored based on the analysis of data from the Supplement on Aging to the National Health Interview Survey, 1984 (N = 11,497) using a modified framework of Aday and Andersen's Expanded Behavioral Model. The results suggested that Social Support as operationalized in this study was an independent determinant of the use of health services. The quantity of social activities and the use of community services were the two most consistent determinants across different types of health services use.^ The effects of social support on the use of health services were broken down into three components to facilitate explanations of the mechanisms through which social support operated. The Predisposing and Enabling component of Social Support had independent, although not uniform, effects on the use of health services. Only slight substitute effects of social support were detected. These included the substitution of the use of senior centers for longer stay in the hospital and the substitution of help with IADL problems for the use of formal home care services.^ The effect of financial support on the use of health services was found to be different for middle and low income populations. This differential effect was also found for the presence of intimate networks, the frequencies of interaction with children and the perceived availability of support among urban/rural, male/female and white/non-white subgroups.^ The study also suggested that the selection of appropriate Health Status measures should be based on the type of Health Services Utilization in which a researcher is interested. The level of physical function limitation and role activity limitation were the two most consistent predictors of the volume of physician visits, number of hospital days, and average length of stay in the hospital during the past year.^ Some alternative hypotheses were also raised and evaluated, when possible. The impacts of the complex sample design, the reliability and validity of the measures and other limitations of this analysis were also discussed. Finally, a revised framework was proposed and discussed based on the analysis. Some policy implications and suggestions for future study were also presented. ^

AN ASSESSMENT OF THE CURRENT STATUS OF MENTAL ILLNESS IN BENDEL STATE OF NIGERIA: IMPLICATIONS FOR PUBLIC MENTAL HEALTH POLICY AND EDUCATION

This descriptive study assesses the current status of mental illness in Bendel State of Nigeria to determine its implications for mental health policy and education. It is a study of the demographic characteristics of psychiatric patients in the only two modern western psychiatric facilities in Bendel State, the various treatment modalities utilized for mental illness, and the people's choice of therapeutic measures for mental illness in Bendel State.^ This study investigated ten aspects of mental illness in Bendel State (1) An increase of the prevalence of mental illness (psychiatric disorder) in Bendel State. (2) Unaided, unguided, and uncared for mentally ill people roaming about Bendel State. (3) Pluralistic Treatment Modalities for mentally ill patients in Bendel State. (4) Traditional Healers treating more mentally ill patients than the modern western psychiatric hospitals. (5) Inadequate modern western psychiatric facilities in Bendel State. (6) Controversy between Traditional Health and modern western trained doctors over the issue of possible cooperation between traditional and modern western medicine. (7) Evidence of mental illness in all ethnic groups in Bendel State. (8) More scientifically based and better organized modern western psychiatric hospitals than the traditional healing centers. (9) Traditional healers' level of approach with patients, and accessibility to patients' families compared with the modern western trained doctors. (10) An urgent need for an official action to institute a comprehensive mental health policy that will provide an optimum care for the mentally ill in Bendel State, and in Nigeria in general.^ Of the eight popular treatment modalities generally used in Bendel State for mental illness, 54% of the non-patient population sampled preferred the use of traditional healing, 26.5% preferred the use of modern western treatment, and 19.5% preferred religious healers.^ The investigator concluded at this time not to recommend the integration of Traditional Healing and modern western medicine in Nigeria. Rather, improvement of the existing modern western psychiatric facilities and a proposal to establish facilities to enable traditional healing and modern western medicine to exist side by side were highly recommended. ^

The response of Texas public health agencies and workers to the emergency preparedness initiatives after 9/11

The purpose of this research was to better understand the impact of the terrorist attacks in 2001 on public health, particularly for Texas public health. This study employed mixed methods to examine changes to public health culture within Texas local public health agencies, important attitudes of public health workers toward responding to a disaster, and the funding policies that might ensure our investment in public health emergency preparedness is protected. ^ A qualitative analysis of interviews conducted with a large sample of public health officials in Texas found that all the constituent parts of a peculiar culture for public health preparedness existed that spanned the state's local health departments regardless of size, or funding level. The new preparedness culture in Texas had the hallmarks necessary for a robust public health preparedness and emergency response system. ^ The willingness of public health workers, necessary to make these kinds of changes and mount a disaster response was examined in one of Texas' most experienced disaster response teams—the public health workers for the City of Houston. A hypothesized latent variable model showed that willingness mediated all other factors in the model (self-efficacy, knowledge, barriers, and risk perception) for self-reported likelihood of reporting to work for a disaster. The RMSEA for the final model was 0.042 with a confidence interval of 0.036—0.049 and the chi-squared difference test was P=0.08, indicating a well-fitted model that suggests willingness is an important factor for consideration by preparedness planners and researchers alike. ^ Finally, with disasters on the rise and federal funding for preparedness dwindling, a review of states' policies for the distribution of these funds and their advantages and disadvantages were examined through a review of current literature and public documents, and a survey of state-level public health officials, emergency management professionals and researchers. Although the base plus per-capita method is the most common, it is not necessarily perceived to be the most effective. No clear "optimal" method emerged from the study, but recommendations for a strategic combination of three methods were made that has the potential to maximize the benefits of each method, while minimizing the weaknesses.^

Relationships among epilepsy self-management, health outcomes, and socioeconomic status

The purpose of this study was to investigate the association between epilepsy self-management and disease control and socio-economic status. Study participants were adult patients at two epilepsy specialty clinics in Houston, Texas that serve demographically and socioeconomically diverse populations. Self-management behaviors- medication, information, safety, seizure, and lifestyle management were tested against emergency room visits, hospitalizations, and seizure occurrence. Overall self-management score was associated with a greater likelihood of hospitalizations over a prior twelve month time frame, but not for three months, and was not associated with seizure occurrence or emergency room visits, at all. Scores on specific self-management behaviors varied in their relationships to the different disease control indicators, over time. Contrary to expectations based on the findings of previous research, higher information management scores were associated with greater likelihood of emergency room visits and hospitalizations, over the study's twelve months. Higher lifestyle management scores were associated with lower likelihood of any emergency room visits, over the preceding twelve months and emergency room visits for the last three months. The positive associations between overall self-management scores and information management behaviors and disease control are contrary to published research. These findings may indicate that those with worse disease control in a prior period employ stronger self-management efforts to better control their epilepsy. Further research is needed to investigate this hypothesis.^

Patenting genes and gene sequences: Analysis of public health implications and the law

At issue is whether or not isolated DNA is patent eligible under the U.S. Patent Law and the implications of that determination on public health. The U.S. Patent and Trademark Office has issued patents on DNA since the 1980s, and scientists and researchers have proceeded under that milieu since that time. Today, genetic research and testing related to the human breast cancer genes BRCA1 and BRCA2 is conducted within the framework of seven patents that were issued to Myriad Genetics and the University of Utah Research Foundation between 1997 and 2000. In 2009, suit was filed on behalf of multiple researchers, professional associations and others to invalidate fifteen of the claims underlying those patents. The Court of Appeals for the Federal Circuit, which hears patent cases, has invalidated claims for analyzing and comparing isolated DNA but has upheld claims to isolated DNA. The specific issue of whether isolated DNA is patent eligible is now before the Supreme Court, which is expected to decide the case by year's end. In this work, a systematic review was performed to determine the effects of DNA patents on various stakeholders and, ultimately, on public health; and to provide a legal analysis of the patent eligibility of isolated DNA and the likely outcome of the Supreme Court's decision. ^ A literature review was conducted to: first, identify principle stakeholders with an interest in patent eligibility of the isolated DNA sequences BRCA1 and BRCA2; and second, determine the effect of the case on those stakeholders. Published reports that addressed gene patents, the Myriad litigation, and implications of gene patents on stakeholders were included. Next, an in-depth legal analysis of the patent eligibility of isolated DNA and methods for analyzing it was performed pursuant to accepted methods of legal research and analysis based on legal briefs, federal law and jurisprudence, scholarly works and standard practice legal analysis. ^ Biotechnology, biomedical and clinical research, access to health care, and personalized medicine were identified as the principle stakeholders and interests herein. Many experts believe that the patent eligibility of isolated DNA will not greatly affect the biotechnology industry insofar as genetic testing is concerned; unlike for therapeutics, genetic testing does not require tremendous resources or lead time. The actual impact on biomedical researchers is uncertain, with greater impact expected for researchers whose work is intended for commercial purposes (versus basic science). The impact on access to health care has been surprisingly difficult to assess; while invalidating gene patents might be expected to decrease the cost of genetic testing and improve access to more laboratories and physicians' offices that provide the test, a 2010 study on the actual impact was inconclusive. As for personalized medicine, many experts believe that the availability of personalized medicine is ultimately a public policy issue for Congress, not the courts. ^ Based on the legal analysis performed in this work, this writer believes the Supreme Court is likely to invalidate patents on isolated DNA whose sequences are found in nature, because these gene sequences are a basic tool of scientific and technologic work and patents on isolated DNA would unduly inhibit their future use. Patents on complementary DNA (cDNA) are expected to stand, however, based on the human intervention required to craft cDNA and the product's distinction from the DNA found in nature. ^ In the end, the solution as to how to address gene patents may lie not in jurisprudence but in a fundamental change in business practices to provide expanded licenses to better address the interests of the several stakeholders. ^

Social integration, health behaviors and health status among Mexican-American women in the *southwestern United States

Using the Hispanic Health and Nutrition Examination Survey (HHANES), this research examined several health behaviors and the health status of Mexican American women. This study focused on determining the relative impact of social contextual factors: age, socioeconomic status, quality of life indicators, and urban/rural residence on (a) health behaviors (smoking, obesity and alcohol use) and (b) health status (physician's assessment of health status, subject's assessment of health status and blood pressure levels). In addition, social integration was analyzed. The social integration indicators relate to an individual's degree of integration within his/her social group: marital status, level of acculturation (a continuum of traditional Mexican ways to dominant U.S. cultural ways), status congruency, and employment status. Lastly, the social contextual factors and social integration indicators were examined to identify those factors that contribute most to understanding health behaviors and health status among Mexican American women.^ The study found that the social contextual factors and social integration indicators proved to be important concepts in understanding the health behaviors. Social integration, however, did not predict health status except in the case of the subject's assessment of health status. Age and obesity were the strongest predictors of blood pressure. The social contextual factors and obesity were significant predictors of the physician's assessment of health status while acculturation, education, alcohol use and obesity were significant predictors of the subject's assessment of health status. ^

Precise set sharin analysis for java-style programs (and proofs).

Finding useful sharing information between instances in object- oriented programs has recently been the focus of much research. The applications of such static analysis are multiple: by knowing which variables definitely do not share in memory we can apply conventional compiler optimizations, find coarse-grained parallelism opportunities, or, more importantly, verify certain correctness aspects of programs even in the absence of annotations. In this paper we introduce a framework for deriving precise sharing information based on abstract interpretation for a Java-like language. Our analysis achieves precision in various ways, including supporting multivariance, which allows separating different contexts. We propose a combined Set Sharing + Nullity + Classes domain which captures which instances do not share and which ones are definitively null, and which uses the classes to refine the static information when inheritance is present. The use of a set sharing abstraction allows a more precise representation of the existing sharings and is crucial in achieving precision during interprocedural analysis. Carrying the domains in a combined way facilitates the interaction among them in the presence of multivariance in the analysis. We show through examples and experimentally that both the set sharing part of the domain as well as the combined domain provide more accurate information than previous work based on pair sharing domains, at reasonable cost.

Influence of liposoluble vitamin status on health parameter and physical fitness in European adolescents = Influencia del estado en vitaminas liposolubles en parámetros de salud y condición física en adolescentes europeos

La adolescencia es un período de crecimiento y desarrollo crítico e importante para la adquisición de hábitos saludables, en los que tanto la alimentación como la actividad física tienen un papel destacado. Junto con el primer año de vida, los requerimientos de energía y nutrientes son mayores que en cualquier otro periodo. Dentro de la nutrición, las vitaminas se ven involucradas en múltiples procesos celulares y tisulares, y sus deficiencias se vinculan a enfermedades crónicas degenerativas en la edad adulta como las cardiovasculares, cáncer, diabetes y osteoporosis, pero cuyos factores de riesgo se establecen a edades más tempranas. Las concentraciones sanguíneas de vitaminas están influenciadas en gran medida por la ingesta dietética, pero existen otros factores del individuo, entre los que cabe citar la composición corporal, la actividad física y condición física que, junto a la genética, podrían desempeñar un papel crucial. La presente memoria de Tesis Doctoral tiene como objetivo analizar el estado en vitaminas liposolubles y su relación con diversos factores de salud, entre los que destacan la composción corporal, hábitos dietéticos, actividad física y condición física en adolescentes Europeos. El trabajo está basado en los datos del estudio HELENA (“Healthy Lifestyle in Europe by Nutrition in Adolescence”). Se han analizado un total de 1089 adolescentes procedentes de diez ciudades en nueve paises europeos. Los principales resultados de este trabajo indican; a) La existencia de un estado deficiente en vitaminas liposolubles en adolescentes Europeos, especialmente de vitamina D, que alcanza valores del 80%. b) La estación del año, la latitud, el índice de masa corporal, la condición física, la ingesta de calcio dietético, los suplementos vitamínicos y la edad son las variables más relacionadas con el estado de vitamina D. c) A su vez, la capacidad cardiorrespiratoria puede predecir los niveles de vitamina D en los chicos, mientras que la fuerza muscular y masa magra parecen influir en los niveles de vitamina D en las chicas. La grasa corporal y el índice de masa corporal se correlaccionan negativamente con los niveles de vitamina D, especialmente en chicos. d) Un estado de vitamina D óptimo provoca una mejora de la masa ósea sólo cuando se tiene un nivel adecuado de actividad física. e) Se identifica la necesidad de establecer un consenso sobre los rangos aceptables y puntos de corte para las concentraciones sanguíneas de estas vitaminas en este grupo de población, ya que los actuales están extrapolados de la población adulta ABSTRACT Adolescence is a critical period of physiological growth and development as well as for the acquisition of healthy behaviors where both diet and physical activity play a major role. Apart from the first year of life, both energy and nutrient requirements are greatest during adolescence and the way to spend this energy by movement is also crucial. Vitamins are specifically involved in multiple cellular and tissue processes, and there is increasing evidence that deficiencies at these early ages could contribute to risk factors of chronic diseases like cardiovascular and cerebrovascular disease, cancer, diabetes and osteoporosis in adulthood, regardless data are scarce for younger ages. Vitamin concentrations are largely influenced by diet but other individual factors like body composition, physical activity or fitness together with genetics could play also an important role. The current thesis analyzes the liposoluble vitamin status in European adolescents and their relation with several health related factors, like body composción, dietary intake, physical activity and fitness. The work is based on data from the HELENA study ("Healthy Lifestyle in Europe by Nutrition in Adolescence"), for which a total of 1089 adolescents from ten different cities, in nine European countries were recruited. The main outcomes of this thesis are: a) There is a high liposoluble vitamin deficiency prevalence in European adolescents, specifically for vitamin D, which is presenting almost 80% of the adolescents. b) Season, latitude, BMI, fitness, dietary calcium intake, supplements intake and age are highly related to 25(OH)D concentrations found in European adolescents. c) Cardiorespiratory fitness may predict 25(OH)D concentrations in male adolescents, whereas upper limbs muscular strength and FFM may predict 25(OH)D concentrations in young females. Fat mass and BMI are inversely related to 25(OH)D concentrations, especially in males. d) The effect of 25(OH)D concentrations on bone mineral content in adolescents depends on physical activity levels. e) There is a need to establish a consensus on acceptable ranges and cut-offs of blood concentrations of these vitamins during adolescence, as currently they are extrapolated from adults.

A Tele-Health Communication and Information System for Underserved Children in Rural Areas of Nicaragua

Millennium Development Goals point out the necessity of actively promoting maternal-child health care status, especially in underserved areas. This article details the development actions carried out between 2008 and 2011 in some rural communities of Nicaragua with the aim to provide a low-cost tele-health communication service. The service is managed by the health care center of Cusmapa, which leads the program and maintains a communication link between its health staff and the health brigades of 26 distant communities. Local agents can use the system to report urgent maternal-child health care episodes to be assessed through WiMAX-WiFi voice and data communications attended by two physicians and six nurses located at the health care center. The health and nutritional status of the maternal-child population can be monitored to prevent diseases, subnutrition, and deaths. The action approach assumes the fundamentals of appropriate technology and looks for community- based, sustainable, replicable, and scalable solutions to ensure future deployments according to the strategies of the United Nations.

Effect of the health status and geographical origin on the cork production characteristics of Western Algeria cork oak stands

Results lead to the conclusion that the effect of health status on traumatic phellogen formation and activity is clear but not uniform. Further studies are necessary for a deeper understanding of the effect of stress situations on pore formation and characteristics

AFRICA BUILD Portal: developing a social network of African health researchers and educators

One of the main outputs of the project is a collaborative platform which integrates a myriad of research and learning resources. This article presents the first prototype of this platform: the AFRICA BUILD Portal (ABP 1.0). The ABP is a Web 2.0 platform which facilitates the access, in a collaborative manner, to these resources. Through a usable web interface, the ABP has been designed to avoid, as much as possible, the connectivity problems of African institutions. In this paper, we suggest that the access to complex systems does not imply slow response rates, and that their development model guides the project to a natural technological transfer, adaptation and user acceptance. Finally, this platform aims to motivate research attitudes during the learning process and stimulate user?s collaborations.

Formal Verification of Temporal Properties for Parametrized Concurrent Programs and Concurrent Data Structures

Los tipos de datos concurrentes son implementaciones concurrentes de las abstracciones de datos clásicas, con la diferencia de que han sido específicamente diseñados para aprovechar el gran paralelismo disponible en las modernas arquitecturas multiprocesador y multinúcleo. La correcta manipulación de los tipos de datos concurrentes resulta esencial para demostrar la completa corrección de los sistemas de software que los utilizan. Una de las mayores dificultades a la hora de diseñar y verificar tipos de datos concurrentes surge de la necesidad de tener que razonar acerca de un número arbitrario de procesos que invocan estos tipos de datos de manera concurrente. Esto requiere considerar sistemas parametrizados. En este trabajo estudiamos la verificación formal de propiedades temporales de sistemas concurrentes parametrizados, poniendo especial énfasis en programas que manipulan estructuras de datos concurrentes. La principal dificultad a la hora de razonar acerca de sistemas concurrentes parametrizados proviene de la interacción entre el gran nivel de concurrencia que éstos poseen y la necesidad de razonar al mismo tiempo acerca de la memoria dinámica. La verificación de sistemas parametrizados resulta en sí un problema desafiante debido a que requiere razonar acerca de estructuras de datos complejas que son accedidas y modificadas por un numero ilimitado de procesos que manipulan de manera simultánea el contenido de la memoria dinámica empleando métodos de sincronización poco estructurados. En este trabajo, presentamos un marco formal basado en métodos deductivos capaz de ocuparse de la verificación de propiedades de safety y liveness de sistemas concurrentes parametrizados que manejan estructuras de datos complejas. Nuestro marco formal incluye reglas de prueba y técnicas especialmente adaptadas para sistemas parametrizados, las cuales trabajan en colaboración con procedimientos de decisión especialmente diseñados para analizar complejas estructuras de datos concurrentes. Un aspecto novedoso de nuestro marco formal es que efectúa una clara diferenciación entre el análisis del flujo de control del programa y el análisis de los datos que se manejan. El flujo de control del programa se analiza utilizando reglas de prueba y técnicas de verificación deductivas especialmente diseñadas para lidiar con sistemas parametrizados. Comenzando a partir de un programa concurrente y la especificación de una propiedad temporal, nuestras técnicas deductivas son capaces de generar un conjunto finito de condiciones de verificación cuya validez implican la satisfacción de dicha especificación temporal por parte de cualquier sistema, sin importar el número de procesos que formen parte del sistema. Las condiciones de verificación generadas se corresponden con los datos manipulados. Estudiamos el diseño de procedimientos de decisión especializados capaces de lidiar con estas condiciones de verificación de manera completamente automática. Investigamos teorías decidibles capaces de describir propiedades de tipos de datos complejos que manipulan punteros, tales como implementaciones imperativas de pilas, colas, listas y skiplists. Para cada una de estas teorías presentamos un procedimiento de decisión y una implementación práctica construida sobre SMT solvers. Estos procedimientos de decisión son finalmente utilizados para verificar de manera automática las condiciones de verificación generadas por nuestras técnicas de verificación parametrizada. Para concluir, demostramos como utilizando nuestro marco formal es posible probar no solo propiedades de safety sino además de liveness en algunas versiones de protocolos de exclusión mutua y programas que manipulan estructuras de datos concurrentes. El enfoque que presentamos en este trabajo resulta ser muy general y puede ser aplicado para verificar un amplio rango de tipos de datos concurrentes similares. Abstract Concurrent data types are concurrent implementations of classical data abstractions, specifically designed to exploit the great deal of parallelism available in modern multiprocessor and multi-core architectures. The correct manipulation of concurrent data types is essential for the overall correctness of the software system built using them. A major difficulty in designing and verifying concurrent data types arises by the need to reason about any number of threads invoking the data type simultaneously, which requires considering parametrized systems. In this work we study the formal verification of temporal properties of parametrized concurrent systems, with a special focus on programs that manipulate concurrent data structures. The main difficulty to reason about concurrent parametrized systems comes from the combination of their inherently high concurrency and the manipulation of dynamic memory. This parametrized verification problem is very challenging, because it requires to reason about complex concurrent data structures being accessed and modified by threads which simultaneously manipulate the heap using unstructured synchronization methods. In this work, we present a formal framework based on deductive methods which is capable of dealing with the verification of safety and liveness properties of concurrent parametrized systems that manipulate complex data structures. Our framework includes special proof rules and techniques adapted for parametrized systems which work in collaboration with specialized decision procedures for complex data structures. A novel aspect of our framework is that it cleanly differentiates the analysis of the program control flow from the analysis of the data being manipulated. The program control flow is analyzed using deductive proof rules and verification techniques specifically designed for coping with parametrized systems. Starting from a concurrent program and a temporal specification, our techniques generate a finite collection of verification conditions whose validity entails the satisfaction of the temporal specification by any client system, in spite of the number of threads. The verification conditions correspond to the data manipulation. We study the design of specialized decision procedures to deal with these verification conditions fully automatically. We investigate decidable theories capable of describing rich properties of complex pointer based data types such as stacks, queues, lists and skiplists. For each of these theories we present a decision procedure, and its practical implementation on top of existing SMT solvers. These decision procedures are ultimately used for automatically verifying the verification conditions generated by our specialized parametrized verification techniques. Finally, we show how using our framework it is possible to prove not only safety but also liveness properties of concurrent versions of some mutual exclusion protocols and programs that manipulate concurrent data structures. The approach we present in this work is very general, and can be applied to verify a wide range of similar concurrent data types.