Safety and health in forest harvesting operations. Diagnosis and preventive actions. A review

Aim of study: to review the present state of the art in relation to the main labour risks and the most relevant results of recent studies evaluating the safety and health conditions of the forest harvesting work and better ways to reduce accidents. Area of study: It focuses mainly on developed Countries, where the general concern about work risks prevention, together with the complex idiosyncrasy of forest work in forest harvesting operations, has led to a growing interest from the forest scientific and technical community. Material and Methods: The main bibliographic and Internet references have been identified using common reference analysis tools. Their conclusions and recommendations have been comprehensively summarized. Main results: Collection of the principal references and their most important conclusions relating to the main accident risk factors, their causes and consequences, the means used towards their prevention, both instrumental as well as in the aspects of training and business management, besides the influence of the growing mechanization of logging operations on those risks. Research highlights: Accident risk is higher in forest harvesting than in most other work sectors, and the main risk factors such as experience, age, seasonality, training, protective equipment, mechanization degree, etc. have been identified and studied. The paper summarizes some relevant results, one of the principal being that the proper entrepreneurial risk management is a key factor leading to the success in minimizing labour risks..

Safety and operability of small fishing vessels: study of a series of stability-related accidents

The intact stability of five small Spanish fishing vessels with ages between 3 and 8 years old which sunk in stability related accidents between 2004 and 2007 is compared to the stability of the fishing vessels which were retired from service to build those. The seakeeping performance of both sets of vessels is also compared. The differences found between the results obtained by the two methods have been analyzed. The suitability of seakeeping methods to assess stability performance is discussed.

Fishing effort control regulations influence on stability, safety and operability of small fishing vessels: study of a series of stability related accidents occurred in Spain between 2004 and 2007

Entre los años 2004 y 2007 se hundieron por problemas de estabilidad cinco pesqueros españoles de pequeña eslora, de características parecidas, de relativamente poca edad, que habían sido construidos en un intervalo de pocos años. La mayoría de los tripulantes de esos pesqueros fallecieron o desaparecieron en esos accidentes. Este conjunto de accidentes tuvo bastante repercusión social y mediática. Entre ingenieros navales y marinos del sector de la pesca se relacionó estos accidentes con los condicionantes a los diseños de los pesqueros impuestos por la normativa de control de esfuerzo pesquero. Los accidentes fueron investigados y publicados sus correspondientes informes; en ellos no se exploró esta supuesta relación. Esta tesis pretende investigar la relación entre esos accidentes y los cambios de la normativa de esfuerzo pesquero. En la introducción se expone la normativa de control de esfuerzo pesquero analizada, se presentan datos sobre la estructura de la flota pesquera en España y su accidentalidad, y se detallan los criterios de estabilidad manejados durante el trabajo, explicando su relación con la seguridad de los pesqueros. Seguidamente se realiza un análisis estadístico de la siniestralidad en el sector de la pesca para establecer si el conjunto de accidentes estudiados supone una anomalía, o si por el contrario el conjunto de estos accidentes no es relevante desde el punto de vista estadístico. Se analiza la siniestralidad a partir de diversas bases de datos de buques pesqueros en España y se concluye que el conjunto de accidentes estudiados supone una anomalía estadística, ya que la probabilidad de ocurrencia de los cinco sucesos es muy baja considerando la frecuencia estimada de pérdidas de buques por estabilidad en el subsector de la flota pesquera en el que se encuadran los cinco buques perdidos. A continuación el trabajo se centra en la comparación de los buques accidentados con los buques pesqueros dados de baja para construir aquellos, según exige la normativa de control de esfuerzo pesquero; a estos últimos buques nos referiremos como “predecesores” de los buques accidentados. Se comparan las dimensiones principales de cada buque y de su predecesor, resultando que los buques accidentados comparten características de diseño comunes que son sensiblemente diferentes en los buques predecesores, y enlazando dichas características de diseño con los requisitos de la nueva normativa de control del esfuerzo pesquero bajo la que se construyeron estos barcos. Ello permite establecer una relación entre los accidentes y el mencionado cambio normativo. A continuación se compara el margen con que se cumplían los criterios reglamentarios de estabilidad entre los buques accidentados y los predecesores, encontrándose que en cuatro de los cinco casos los predecesores cumplían los criterios de estabilidad con mayor holgura que los buques accidentados. Los resultados obtenidos en este punto permiten establecer una relación entre el cambio de normativa de esfuerzo pesquero y la estabilidad de los buques. Los cinco buques accidentados cumplían con los criterios reglamentarios de estabilidad en vigor, lo que cuestiona la relación entre esos criterios y la seguridad. Por ello se extiende la comparativa entre pesqueros a dos nuevos campos relacionados con la estabilidad y la seguridad delos buques: • Movimientos a bordo (operatividad del buque), y • Criterios de estabilidad en condiciones meteorológicas adversas El estudio de la operatividad muestra que los buques accidentados tenían, en general, una mayor operatividad que sus predecesores, contrariamente a lo que sucedía con el cumplimiento de los criterios reglamentarios de estabilidad. Por último, se comprueba el desempeño de los diez buques en dos criterios específicos de estabilidad en caso de mal tiempo: el criterio IMO de viento y balance intenso, y un criterio de estabilidad de nueva generación, incluyendo la contribución original del autor de considerar agua en cubierta. Las tendencias observadas en estas dos comparativas son opuestas, lo que permite cuestionar la validez del último criterio sin un control exhaustivo de los parámetros de su formulación, poniendo de manifiesto la necesidad de más investigaciones sobre ese criterio antes de su adopción para uso regulatorio. El conjunto de estos resultados permite obtener una serie de conclusiones en la comparativa entre ambos conjuntos de buques pesqueros. Si bien los resultados de este trabajo no muestran que la aprobación de la nueva normativa de esfuerzo pesquero haya significado una merma general de seguridad en sectores enteros de la flota pesquera, sí se concluye que permitió que algunos diseños de buques pesqueros, posiblemente en busca de la mayor eficiencia compatible con dicha normativa, quedaran con una estabilidad precaria, poniendo de manifiesto que la relación entre seguridad y criterios de estabilidad no es unívoca, y la necesidad de que éstos evolucionen y se adapten a los nuevos diseños de buques pesqueros para continuar garantizando su seguridad. También se concluye que la estabilidad es un aspecto transversal del diseño de los buques, por lo que cualquier reforma normativa que afecte al diseño de los pesqueros o su forma de operar debería estar sujeta a evaluación por parte de las autoridades responsables de la seguridad marítima con carácter previo a su aprobación. ABSTRACT Between 2004 and 2007 five small Spanish fishing vessels sank in stability related accidents. These vessels had similar characteristics, had relatively short age, and had been built in a period of a few years. Most crewmembers of these five vessels died or disappeared in those accidents. This set of accidents had significant social and media impact. Among naval architects and seamen of the fishing sector these accidents were related to the design constraints imposed by the fishing control effort regulations. The accidents were investigated and the official reports issued; this alleged relationship was not explored. This thesis aims to investigate the relationship between those accidents and changes in fishing effort control regulations. In the introduction, the fishing effort control regulation is exposed, data of the Spanish fishing fleet structure and its accident rates are presented, and stability criteria dealt with in this work are explained, detailing its relationship with fishing vessel safety. A statistical analysis of the accident rates in the fishing sector in Spain is performed afterwards. The objective is determining whether the set of accidents studied constitute an anomaly or, on the contrary, they are not statistically relevant. Fishing vessels accident rates is analyzed from several fishing vessel databases in Spain. It is concluded that the set of studied accidents is statistically relevant, as the probability of occurrence of the five happenings is extremely low, considering the loss rates in the subsector of the Spanish fishing fleet where the studied vessels are fitted within. From this point the thesis focuses in comparing the vessels lost and the vessels that were decommissioned to build them as required by the fishing effort control regulation; these vessels will be referred to as “predecessors” of the sunk vessels. The main dimensions between each lost vessel and her predecessor are compared, leading to the conclusion that the lost vessels share design characteristics which are sensibly different from the predecessors, and linking these design characteristics with the requirements imposed by the new fishing control effort regulations. This allows establishing a relationship between the accidents and this regulation change. Then the margin in fulfilling the regulatory stability criteria among the vessels is compared, resulting, in four of the five cases, that predecessors meet the stability criteria with greater clearance than the sunk vessels. The results obtained at this point would establish a relationship between the change of fishing effort control regulation and the stability of vessels. The five lost vessels complied with the stability criteria in force, so the relation between these criteria and safety is put in question. Consequently, the comparison among vessels is extended to other fields related to safety and stability: • Motions onboard (operability), and • Specific stability criteria in rough weather The operability study shows that the lost vessels had in general greater operability than their predecessors, just the opposite as when comparing stability criteria. Finally, performance under specific rough weather stability criteria is checked. The criteria studied are the IMO Weather Criterion, and one of the 2nd generation stability criteria under development by IMO considering in this last case the presence of water on deck, which is an original contribution by the author. The observed trends in these two cases are opposite, allowing to put into question the last criterion validity without an exhaustive control of its formulation parameters; indicating that further research might be necessary before using it for regulatory purposes. The analysis of this set of results leads to some conclusions when comparing both groups of fishing vessels. While the results obtained are not conclusive in the sense that the entry into force of a new fishing effort control in 1998 caused a generalized safety reduction in whole sectors of the Spanish fishing fleet, it can be concluded that it opened the door for some vessel designs resulting with precarious stability. This evidences that the relation between safety and stability criteria is not univocal, so stability criteria needs to evolve for adapting to new fishing vessels designs so their safety is still guaranteed. It is also concluded that stability is a transversal aspect to ship design and operability, implying that any legislative reform affecting ship design or operating modes should be subjected to assessing by the authorities responsible for marine safety before being adopted.

Models for Lateral Dynamic Interaction of High-Speed Trains and Bridges

In this work a methodology for analysing the lateral coupled behavior of large viaducts and high-speed trains is proposed. The finite element method is used for the structure, multibody techniques are applied for vehicles and the interaction between them is established introducing wheel-rail nonlinear contact forces. This methodology is applied for the analysis of the railway viaduct of the R´ıo Barbantino, which is a very long and tall bridge in the north-west spanish high-speed line.

Safety-related issues for high-speed railway bridges

Railway bridges have specific requirements related to safety, which often are critical aspects of design. In this paper the main phenomena are reviewed, namely vertical dynamic effects for impact effect of moving loads and resonance in high-speed, service limit states which affect the safety of running traffic, and lateral dynamic effects.

Health and safety in the construction : subject pending to be included in the curriculum of architecture in Spain

The art of construction is a risky activity that directly affects the life and physical integrity of persons. Since the approval of Law 31/1995, of November 8, Prevention of Occupational Risks was the first legislation that established the current basis in all sectors and then transposed into Spanish law Directive 92/57/CEE called Royal Decree 1627/1997 of October 24, on minimum safety and health dispositions in construction works, measures have been proposed to develop a mixed body of scientific literature composed of researchers and professionals in the field of occupational safety and health, but even today there is still no clear and firm proposal, showing a lack of awareness in the occupational risk prevention and, therefore, a consolidation of the culture of prevention in society. Therefore, the technicians, who make up the building process, can incur in very high responsibilities, such as: Author of the project, Coordinator of Safety and Health during the preparation of the project and during the execution of works, Site Management: Site Manager. This involves the immediate creation of a general training in prevention for all architects starting when still studying, as well as specific training, appropriate and complementary to all the architects that will be devoted to the specialty of occupational safety and health in construction works. That is, first, we must make the responsible bodies aware of the urgent need to integrate risk prevention in the curricula of architecture and later in the continuing education of the profession. It is necessary that our teaching must conform to the laws on safety and health, due to the fact that the law recognizes our academic degrees and professional qualifications to perform functions in that area

Effectiveness of AFLPs and retrotransposon-based markers for the identification of portuguese grapevine cultivars and clones

Grapevine germplasm, including 38 of the main Portuguese cultivars and three foreign cultivars, Pinot Noir, Pinot Blanc and Chasselas, used as a reference, and 37 true-to-type clones from the Alvarinho, Arinto, Loureiro, Moscatel Galego Branco, Trajadura and Vinhão cultivars were studied using AFLP and three retrotransposon-based molecular techniques, IRAP, REMAP and SSAP. To study the retrotransposon-based polymorphisms, 18 primers based on the LTR sequences of Tvv1, Gret1 and Vine-1 were used. In the analysis of 41 cultivars, 517 IRAP, REMAP, AFLP and SSAP fragments were obtained, 83% of which were polymorphic. For IRAP, only the Tvv1Fa primer amplified DNA fragments. In the REMAP analysis, the Tvv1Fa-Ms14 primer combination only produced polymorphic bands, and the Vine-1 primers produced mainly ISSR fragments. The highest number of polymorphic fragments was found for AFLP. Both AFLP and SSAP showed a greater capacity for identifying clones, resulting in 15 and 9 clones identified, respectively. Together, all of the techniques allowed for the identification of 54% of the studied clones, which is an important step in solving one of the challenges that viticulture currently faces.

Core physics and safety analysis of Generation-IV Sodium Fast Reactors using existing and newly developed computational tools

El futuro de la energía nuclear de fisión dependerá, entre otros factores, de la capacidad que las nuevas tecnologías demuestren para solventar los principales retos a largo plazo que se plantean. Los principales retos se pueden resumir en los siguientes aspectos: la capacidad de proporcionar una solución final, segura y fiable a los residuos radiactivos; así como dar solución a la limitación de recursos naturales necesarios para alimentar los reactores nucleares; y por último, una mejora robusta en la seguridad de las centrales que en definitiva evite cualquier daño potencial tanto en la población como en el medio ambiente como consecuencia de cualquier escenario imaginable o más allá de lo imaginable. Siguiendo estas motivaciones, la Generación IV de reactores nucleares surge con el compromiso de proporcionar electricidad de forma sostenible, segura, económica y evitando la proliferación de material fisible. Entre los sistemas conceptuales que se consideran para la Gen IV, los reactores rápidos destacan por su capacidad potencial de transmutar actínidos a la vez que permiten una utilización óptima de los recursos naturales. Entre los refrigerantes que se plantean, el sodio parece una de las soluciones más prometedoras. Como consecuencia, esta tesis surgió dentro del marco del proyecto europeo CP-ESFR con el principal objetivo de evaluar la física de núcleo y seguridad de los reactores rápidos refrigerados por sodio, al tiempo que se desarrollaron herramientas apropiadas para dichos análisis. Efectivamente, en una primera parte de la tesis, se abarca el estudio de la física del núcleo de un reactor rápido representativo, incluyendo el análisis detallado de la capacidad de transmutar actínidos minoritarios. Como resultado de dichos análisis, se publicó un artículo en la revista Annals of Nuclear Energy [96]. Por otra parte, a través de un análisis de un hipotético escenario nuclear español, se evalúo la disponibilidad de recursos naturales necesarios en el caso particular de España para alimentar una flota específica de reactores rápidos, siguiendo varios escenarios de demanda, y teniendo en cuenta la capacidad de reproducción de plutonio que tienen estos sistemas. Como resultado de este trabajo también surgió una publicación en otra revista científica de prestigio internacional como es Energy Conversion and Management [97]. Con objeto de realizar esos y otros análisis, se desarrollaron diversos modelos del núcleo del ESFR siguiendo varias configuraciones, y para diferentes códigos. Por otro lado, con objeto de poder realizar análisis de seguridad de reactores rápidos, son necesarias herramientas multidimensionales de alta fidelidad específicas para reactores rápidos. Dichas herramientas deben integrar fenómenos relacionados con la neutrónica y con la termo-hidráulica, entre otros, mediante una aproximación multi-física. Siguiendo este objetivo, se evalúo el código de difusión neutrónica ANDES para su aplicación a reactores rápidos. ANDES es un código de resolución nodal que se encuentra implementado dentro del sistema COBAYA3 y está basado en el método ACMFD. Por lo tanto, el método ACMFD fue sometido a una revisión en profundidad para evaluar su aptitud para la aplicación a reactores rápidos. Durante ese proceso, se identificaron determinadas limitaciones que se discutirán a lo largo de este trabajo, junto con los desarrollos que se han elaborado e implementado para la resolución de dichas dificultades. Por otra parte, se desarrolló satisfactoriamente el acomplamiento del código neutrónico ANDES con un código termo-hidráulico de subcanales llamado SUBCHANFLOW, desarrollado recientemente en el KIT. Como conclusión de esta parte, todos los desarrollos implementados son evaluados y verificados. En paralelo con esos desarrollos, se calcularon para el núcleo del ESFR las secciones eficaces en multigrupos homogeneizadas a nivel nodal, así como otros parámetros neutrónicos, mediante los códigos ERANOS, primero, y SERPENT, después. Dichos parámetros se utilizaron más adelante para realizar cálculos estacionarios con ANDES. Además, como consecuencia de la contribución de la UPM al paquete de seguridad del proyecto CP-ESFR, se calcularon mediante el código SERPENT los parámetros de cinética puntual que se necesitan introducir en los típicos códigos termo-hidráulicos de planta, para estudios de seguridad. En concreto, dichos parámetros sirvieron para el análisis del impacto que tienen los actínidos minoritarios en el comportamiento de transitorios. Concluyendo, la tesis presenta una aproximación sistemática y multidisciplinar aplicada al análisis de seguridad y comportamiento neutrónico de los reactores rápidos de sodio de la Gen-IV, usando herramientas de cálculo existentes y recién desarrolladas ad' hoc para tal aplicación. Se ha empleado una cantidad importante de tiempo en identificar limitaciones de los métodos nodales analíticos en su aplicación en multigrupos a reactores rápidos, y se proponen interesantes soluciones para abordarlas. ABSTRACT The future of nuclear reactors will depend, among other aspects, on the capability to solve the long-term challenges linked to this technology. These are the capability to provide a definite, safe and reliable solution to the nuclear wastes; the limitation of natural resources, needed to fuel the reactors; and last but not least, the improved safety, which would avoid any potential damage on the public and or environment as a consequence of any imaginable and beyond imaginable circumstance. Following these motivations, the IV Generation of nuclear reactors arises, with the aim to provide sustainable, safe, economic and proliferationresistant electricity. Among the systems considered for the Gen IV, fast reactors have a representative role thanks to their potential capacity to transmute actinides together with the optimal usage of natural resources, being the sodium fast reactors the most promising concept. As a consequence, this thesis was born in the framework of the CP-ESFR project with the generic aim of evaluating the core physics and safety of sodium fast reactors, as well as the development of the approppriated tools to perform such analyses. Indeed, in a first part of this thesis work, the main core physics of the representative sodium fast reactor are assessed, including a detailed analysis of the capability to transmute minor actinides. A part of the results obtained have been published in Annals of Nuclear Energy [96]. Moreover, by means of the analysis of a hypothetical Spanish nuclear scenario, the availability of natural resources required to deploy an specific fleet of fast reactor is assessed, taking into account the breeding properties of such systems. This work also led to a publication in Energy Conversion and Management [97]. In order to perform those and other analyses, several models of the ESFR core were created for different codes. On the other hand, in order to perform safety studies of sodium fast reactors, high fidelity multidimensional analysis tools for sodium fast reactors are required. Such tools should integrate neutronic and thermal-hydraulic phenomena in a multi-physics approach. Following this motivation, the neutron diffusion code ANDES is assessed for sodium fast reactor applications. ANDES is the nodal solver implemented inside the multigroup pin-by-pin diffusion COBAYA3 code, and is based on the analytical method ACMFD. Thus, the ACMFD was verified for SFR applications and while doing so, some limitations were encountered, which are discussed through this work. In order to solve those, some new developments are proposed and implemented in ANDES. Moreover, the code was satisfactorily coupled with the thermal-hydraulic code SUBCHANFLOW, recently developed at KIT. Finally, the different implementations are verified. In addition to those developments, the node homogenized multigroup cross sections and other neutron parameters were obtained for the ESFR core using ERANOS and SERPENT codes, and employed afterwards by ANDES to perform steady state calculations. Moreover, as a result of the UPM contribution to the safety package of the CP-ESFR project, the point kinetic parameters required by the typical plant thermal-hydraulic codes were computed for the ESFR core using SERPENT, which final aim was the assessment of the impact of minor actinides in transient behaviour. All in all, the thesis provides a systematic and multi-purpose approach applied to the assessment of safety and performance parameters of Generation-IV SFR, using existing and newly developed analytical tools. An important amount of time was employed in identifying the limitations that the analytical nodal diffusion methods present when applied to fast reactors following a multigroup approach, and interesting solutions are proposed in order to overcome them.

Strategies and good practice for sustainable and liveable cities of tomorrow

This contribution deals with the question, what makes cities sustainable and integrative, and suggests an approach for "liveable cities of tomorrow" designed to sustain mobility. The liveable city of tomorrow needs to meet both ecological and social requirements in an integrative approach. To design urban patterns appropriate or “sustainable mobility” based on a concept of mobility defined as the number of accessible destinations (different to that for “fossil mobility” defined as the ability to cover distances) is a key element of such an approach. Considering the limited reserves of fossil fuels and the long lifetime of the built structure, mobility needs to rely on modes independent of fossil fuels (public transport and pedestrians) to make it sustainable and the urban pattern needs to be developed appropriately for these modes. Crucial for the success of public transport is the location of buildings within the catchment area of stops. An attractive urban environment for pedestrians is characterised by short distances in a compact settlement with appropriate/qualified urban density and mixed land use as well as by attractive public space. This, complemented by an integrative urban development on the quarter level including neighbourhood management with a broad spectrum of activity areas (social infrastructure, integration of diverse social and ethnic groups, health promotion, community living, etc.), results in increased liveability. The role of information technology in this context is to support a sustainable use of the built structures by organisational instruments. Sustainable and liveable communities offer many benefits for health, safety and well-being of their inhabitants.

State of the Art and Future Trends in Grid Codes Applicable to Isolated Electrical Systems

Electrical power systems are changing their traditional structure, which was based on a little number of large generating power plants placed at great distances from loads by new models that tend to split the big production nodes in many smaller ones. The set of small groups which are located close to consumers and provide safe and quality energy is called distributed generation (DG). The proximity of the sources to the loads reduces losses associated with transportation and increases overall system efficiency. DG also favors the inclusion of renewable energy sources in isolated electrical systems or remote microgrids, because they can be installed where the natural resource is located. In both cases, as weak grids unable to get help from other nearby networks, it is essential to ensure appropriate behavior of DG sources to guarantee power system safety and stability. The grid codes sets out the technical requirements to be fulfilled for the sources connected in these electrical networks. In technical literature it is rather easy to find and compare grid codes for interconnected electrical systems. However, the existing literature is incomplete and sparse regarding isolated electrical systems and this happens due to the difficulties inherent in the pursuit of codes. Some countries have developed their own legislation only for their island territory (as Spain or France), others apply the same set of rules as in mainland, another group of island countries have elaborated a complete grid code for all generating sources and some others lack specific regulation. This paper aims to make a complete review of the state of the art in grid codes applicable to isolated systems, setting the comparison between them and defining the guidelines predictably followed by the upcoming regulations in these particular systems.

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.