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.

Planning and projects: three visionaires Friedmann, J., Trueba, I. and Ramos, A.

It is impossible to talk about planning as a scientific meta-discipline without mentioning one of the most influential worldwide figures in the second half of the twentieth century: John Friedmann. His contribution to the planning concept on his "Planning as Social Learning" theory is still very relevant. This paper shows the intellectual connection between Friedmann and Angel Ramos and Ignacio Trueba, two of the Spanish intellectual drivers in the engineering project knowledge area, who contributed to founding the Engineering Projects Spanish Association. The three of them share a broad vision of the project and abandon the "blue print" planning model. They also see the project as a transformational tool that requires a different planning style to the one which prevailed in the 70s - both in public and private domains. They were pioneers in structuring Knowledge / Action in a different way, both in academic institutions where disciples helped to bring about change- and with direct action via projects.

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.

Health beliefs and folk models of diabetes in British Bangladeshis: a qualitative study

Objective: To explore the experience of diabetes in British Bangladeshis, since successful management of diabetes requires attention not just to observable behaviour but to the underlying attitudes and belief systems which drive that behaviour.