Deciding difference logic in a Nelson-Oppen combination framework

O método de combinação de Nelson-Oppen permite que vários procedimentos de decisão, cada um projetado para uma teoria específica, possam ser combinados para inferir sobre teorias mais abrangentes, através do princípio de propagação de igualdades. Provadores de teorema baseados neste modelo são beneficiados por sua característica modular e podem evoluir mais facilmente, incrementalmente. Difference logic é uma subteoria da aritmética linear. Ela é formada por constraints do tipo x − y ≤ c, onde x e y são variáveis e c é uma constante. Difference logic é muito comum em vários problemas, como circuitos digitais, agendamento, sistemas temporais, etc. e se apresenta predominante em vários outros casos. Difference logic ainda se caracteriza por ser modelada usando teoria dos grafos. Isto permite que vários algoritmos eficientes e conhecidos da teoria de grafos possam ser utilizados. Um procedimento de decisão para difference logic é capaz de induzir sobre milhares de constraints. Um procedimento de decisão para a teoria de difference logic tem como objetivo principal informar se um conjunto de constraints de difference logic é satisfatível (as variáveis podem assumir valores que tornam o conjunto consistente) ou não. Além disso, para funcionar em um modelo de combinação baseado em Nelson-Oppen, o procedimento de decisão precisa ter outras funcionalidades, como geração de igualdade de variáveis, prova de inconsistência, premissas, etc. Este trabalho apresenta um procedimento de decisão para a teoria de difference logic dentro de uma arquitetura baseada no método de combinação de Nelson-Oppen. O trabalho foi realizado integrando-se ao provador haRVey, de onde foi possível observar o seu funcionamento. Detalhes de implementação e testes experimentais são relatados

Innovation and technology policy (ITP) for catching up: a three phase life cycle framework for industrializing economies

Includes bibliography

Difusão do trabalho agrícola formal no Brasil e sua dinâmica multiescalar

This paper aims to analyze the geographical dynamics of work from the spread of formal employment in the agricultural sector in Northeast Brazil. In recent years the region has had highlighted a growing movement to produce fruit for export, resulting in the promotion of important sociospatial transformations arising from the formation of a capitalist labor market. Data about the increase in the number of formal jobs show the impact of fruit growing agribusiness in the establishment of a new social and territorial division of labor. However, our study draws attention to the existence of a framework dominated for the vulnerability of the labor market by the persistence of seasonality and precarious working conditions.

Product-portfolio management: A framework based on Methods, Organization, and Strategy

Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)

Searching and retrieving in content-based repositories of formal mathematical knowledge

In this thesis, the author presents a query language for an RDF (Resource Description Framework) database and discusses its applications in the context of the HELM project (the Hypertextual Electronic Library of Mathematics). This language aims at meeting the main requirements coming from the RDF community. in particular it includes: a human readable textual syntax and a machine-processable XML (Extensible Markup Language) syntax both for queries and for query results, a rigorously exposed formal semantics, a graph-oriented RDF data access model capable of exploring an entire RDF graph (including both RDF Models and RDF Schemata), a full set of Boolean operators to compose the query constraints, fully customizable and highly structured query results having a 4-dimensional geometry, some constructions taken from ordinary programming languages that simplify the formulation of complex queries. The HELM project aims at integrating the modern tools for the automation of formal reasoning with the most recent electronic publishing technologies, in order create and maintain a hypertextual, distributed virtual library of formal mathematical knowledge. In the spirit of the Semantic Web, the documents of this library include RDF metadata describing their structure and content in a machine-understandable form. Using the author's query engine, HELM exploits this information to implement some functionalities allowing the interactive and automatic retrieval of documents on the basis of content-aware requests that take into account the mathematical nature of these documents.

Recycling the city: a sustainable planning framework to reduce, reuse and recycle urban residual spaces

Cities are key locations where Sustainability needs to be addressed at all levels, as land is a finite resource. However, not all urban spaces are exploited at best, and land developers often evaluate unused, misused, or poorly-designed urban portions as impracticable constraints. Further, public authorities lose the challenge to enable and turn these urban spaces into valuable opportunities where Sustainable Urban Development may flourish. Arguing that these spatial elements are at the centre of SUD, the paper elaborates a prototype in the form of a conceptual strategic planning framework, committed to an effective recycling of the city spaces using a flexible and multidisciplinary approach. Firstly, the research focuses upon a broad review of Sustainability literature, highlighting established principles and guidelines, building a sound theoretical base for the new concept. Hence, it investigates origins, identifies and congruently suggests a definition, characterisation and classification for urban “R-Spaces”. Secondly, formal, informal and temporary fitting functions are analysed and inserted into a portfolio meant to enhance adaptability and enlarge the choices for the on-site interventions. Thirdly, the study outlines ideal quality requirements for a sustainable planning process. Then, findings are condensed in the proposal, which is articulated in the individuation of tools, actors, plans, processes and strategies. Afterwards, the prototype is tested upon case studies: Solar Community (Casalecchio di Reno, Bologna) and Hyllie Sustainable City Project, the latter developed via an international workshop (ACSI-Camp, Malmö, Sweden). Besides, the qualitative results suggest, inter alia, the need to right-size spatial interventions, separate structural and operative actors, involve synergies’ multipliers and intermediaries (e.g. entrepreneurial HUBs, innovation agencies, cluster organisations…), maintain stakeholders’ diversity and create a circular process open for new participants. Finally, the paper speculates upon a transfer of the Swedish case study to Italy, and then indicates desirable future researches to favour the prototype implementation.

The MIRELA framework: modeling and analyzing mixed reality applications using timed automata

Mixed Reality (MR) aims to link virtual entities with the real world and has many applications such as military and medical domains [JBL+00, NFB07]. In many MR systems and more precisely in augmented scenes, one needs the application to render the virtual part accurately at the right time. To achieve this, such systems acquire data related to the real world from a set of sensors before rendering virtual entities. A suitable system architecture should minimize the delays to keep the overall system delay (also called end-to-end latency) within the requirements for real-time performance. In this context, we propose a compositional modeling framework for MR software architectures in order to specify, simulate and validate formally the time constraints of such systems. Our approach is first based on a functional decomposition of such systems into generic components. The obtained elements as well as their typical interactions give rise to generic representations in terms of timed automata. A whole system is then obtained as a composition of such defined components. To write specifications, a textual language named MIRELA (MIxed REality LAnguage) is proposed along with the corresponding compilation tools. The generated output contains timed automata in UPPAAL format for simulation and verification of time constraints. These automata may also be used to generate source code skeletons for an implementation on a MR platform. The approach is illustrated first on a small example. A realistic case study is also developed. It is modeled by several timed automata synchronizing through channels and including a large number of time constraints. Both systems have been simulated in UPPAAL and checked against the required behavioral properties.

A stratigraphic framework for abrupt climatic changes during the Last Glacial period based on three synchronized Greenland ice-core records: refining and extending the INTIMATE event stratigraphy

Due to their outstanding resolution and well-constrained chronologies, Greenland ice-core records provide a master record of past climatic changes throughout the Last Interglacial–Glacial cycle in the North Atlantic region. As part of the INTIMATE (INTegration of Ice-core, MArine and TErrestrial records) project, protocols have been proposed to ensure consistent and robust correlation between different records of past climate. A key element of these protocols has been the formal definition and ordinal numbering of the sequence of Greenland Stadials (GS) and Greenland Interstadials (GI) within the most recent glacial period. The GS and GI periods are the Greenland expressions of the characteristic Dansgaard–Oeschger events that represent cold and warm phases of the North Atlantic region, respectively. We present here a more detailed and extended GS/GI template for the whole of the Last Glacial period. It is based on a synchronization of the NGRIP, GRIP, and GISP2 ice-core records that allows the parallel analysis of all three records on a common time scale. The boundaries of the GS and GI periods are defined based on a combination of stable-oxygen isotope ratios of the ice (δ18O, reflecting mainly local temperature) and calcium ion concentrations (reflecting mainly atmospheric dust loading) measured in the ice. The data not only resolve the well-known sequence of Dansgaard–Oeschger events that were first defined and numbered in the ice-core records more than two decades ago, but also better resolve a number of short-lived climatic oscillations, some defined here for the first time. Using this revised scheme, we propose a consistent approach for discriminating and naming all the significant abrupt climatic events of the Last Glacial period that are represented in the Greenland ice records. The final product constitutes an extended and better resolved Greenland stratotype sequence, against which other proxy records can be compared and correlated. It also provides a more secure basis for investigating the dynamics and fundamental causes of these climatic perturbations.

Comparability of Outcome Frameworks in Medical Education: Implications for framework development

Background: The demand for international harmonization in medical education increases with the growing mobility of students and health professionals. Many medical societies and governmental offices have issued outcome frameworks (OF), which describe aims and contents of medical education based on competencies. These national standards affect the development of curricula as well as assessment and licensing procedures. Comparing OF and identifying factors that limit their comparability may thus foster international harmonization of medical education. Summary of Work: We conducted a systematic search for national OF in MedLine, EmBase and the internet. We included all OF in German or English that resulted from a national consensus process and were published or endorsed by a national society or governmental body. We extracted information in five predetermined categories: history of origin, audience, formal structure, medical schooling system and key terms. Summary of Results: Out of 1816 results, 13 OF were included into further analyses. OF reference each other, often without addressing existing differences (e.g. in target audiences). The two most cited OF are “CanMEDs” and “Scottish Doctor”. OF differ especially in their level of detail as well as in the underlying educational system. Discussion and Conclusions: Based on our results we propose a two-step blueprint for OF, that may help to establish comparability for internationally aligned key features – so-called “core competencies” – while at the same time allowing for necessary regional adaptations in terms of “secondary competencies”. Take-home messages: Considerable differences in at least five categories of OF currently hinder the comparability of outcome frameworks.

Framework for risk assessment for maritime transportation systems

Maritime accidents involving ships carrying passengers may pose a high risk with respect to human casualties. For effective risk mitigation, an insight into the process of risk escalation is needed. This requires a proactive approach when it comes to risk modelling for maritime transportation systems. Most of the existing models are based on historical data on maritime accidents, and thus they can be considered reactive instead of proactive. This paper introduces a systematic, transferable and proactive framework estimating the risk for maritime transportation systems, meeting the requirements stemming from the adopted formal definition of risk. The framework focuses on ship-ship collisions in the open sea, with a RoRo/Passenger ship (RoPax) being considered as the struck ship. First, it covers an identification of the events that follow a collision between two ships in the open sea, and, second, it evaluates the probabilities of these events, concluding by determining the severity of a collision. The risk framework is developed with the use of Bayesian Belief Networks and utilizes a set of analytical methods for the estimation of the risk model parameters. The model can be run with the use of GeNIe software package. Finally, a case study is presented, in which the risk framework developed here is applied to a maritime transportation system operating in the Gulf of Finland (GoF). The results obtained are compared to the historical data and available models, in which a RoPax was involved in a collision, and good agreement with the available records is found.

Infrastructure and Workflow for the Formal Evaluation of Semantic Search Technologies

This paper describes an infrastructure for the automated evaluation of semantic technologies and, in particular, semantic search technologies. For this purpose, we present an evaluation framework which follows a service-oriented approach for evaluating semantic technologies and uses the Business Process Execution Language (BPEL) to define evaluation workflows that can be executed by process engines. This framework supports a variety of evaluations, from different semantic areas, including search, and is extendible to new evaluations. We show how BPEL addresses this diversity as well as how it is used to solve specific challenges such as heterogeneity, error handling and reuse

A generic, context sensitive analysis framework for object oriented programs

Abstract interpreters rely on the existence of a nxpoint algorithm that calculates a least upper bound approximation of the semantics of the program. Usually, that algorithm is described in terms of the particular language in study and therefore it is not directly applicable to programs written in a different source language. In this paper we introduce a generic, block-based, and uniform representation of the program control flow graph and a language-independent nxpoint algorithm that can be applied to a variety of languages and, in particular, Java. Two major characteristics of our approach are accuracy (obtained through a topdown, context sensitive approach) and reasonable efficiency (achieved by means of memoization and dependency tracking techniques). We have also implemented the proposed framework and show some initial experimental results for standard benchmarks, which further support the feasibility of the solution adopted.

Integration of cooperation for development in Survey Engineering curricula at the European Higher Education Area (EHEA) framework

Survey Engineering curricula involves the integration of many formal disciplines at a high level of proficiency. The Escuela de Ingenieros en Topografía, Cartografía y Geodesia at Universidad Politécnica de Madrid (Survey Engineering) has developed an intense and deep teaching on so-called Applied Land Sciences and Technologies or Land Engineering. However, new approaches are encouraged by the European Higher Education Area (EHEA). This fact requires a review of traditional teaching and methods. Furthermore, the new globalization and international approach gives new ways to this discipline to teach and learn about how to bridge gap between cultures and regions. This work is based in two main needs. On one hand, it is based on integration of basic knowledge and disciplines involved in typical Survey Engineering within Land Management. On the other, there is an urgent need to consider territory on a social and ethical basis, as far as a part of the society, culture, idiosyncrasy or economy. The integration of appropriate knowledge of the Land Management is typically dominated by civil engineers and urban planners. It would be very possible to integrate Survey Engineering and Cooperation for Development in the framework of Land Management disciplines. Cooperation for Development is a concept that has changed since beginning of its use until now. Development projects leave an impact on society in response to their beneficiaries and are directed towards self-sustainability. Furthermore, it is the true bridge to reduce gap between societies when differences are immeasurable. The concept of development has also been changing and nowadays it is not a purely economic concept. Education, science and technology are increasingly taking a larger role in what is meant by development. Moreover, it is commonly accepted that Universities should transfer knowledge to society, and the transfer of knowledge should be open to countries most in need for developing. If the importance of the country development is given by education, science and technology, knowledge transfer would be one of the most clear of ways of Cooperation for Development. Therefore, university cooperation is one of the most powerful tools to achieve it, placing universities as agents of development. In Spain, the role of universities as agents of development and cooperation has been largely strengthened. All about this work deals to how to implement both Cooperation for Development and Land Management within Survey Engineering at the EHEA framework.

Implementing a term rewriting engine for the EasyCrypt framework

La sociedad depende hoy más que nunca de la tecnología, pero la inversión en seguridad es escasa y los sistemas informáticos siguen estando muy lejos de ser seguros. La criptografía es una de las piedras angulares de la seguridad en este ámbito, por lo que recientemente se ha dedicado una cantidad considerable de recursos al desarrollo de herramientas que ayuden en la evaluación y mejora de los algoritmos criptográficos. EasyCrypt es uno de estos sistemas, desarrollado recientemente en el Instituto IMDEA Software en respuesta a la creciente necesidad de disponer de herramientas fiables de verificación formal de criptografía. En este trabajo se abordará la implementación de una mejora en el reductor de términos de EasyCrypt, sustituyéndolo por una máquina abstracta simbólica. Para ello se estudiarán e implementarán previamente dos máquinas abstractas muy conocidas, la Máquina de Krivine y la ZAM, introduciendo variaciones sobre ellas y estudiando sus diferencias desde un punto de vista práctico.---ABSTRACT---Today, society depends more than ever on technology, but the investment in security is still scarce and using computer systems are still far from safe to use. Cryptography is one of the cornerstones of security, so there has been a considerable amount of effort devoted recently to the development of tools oriented to the evaluation and improvement of cryptographic algorithms. One of these tools is EasyCrypt, developed recently at IMDEA Software Institute in response to the increasing need of reliable formal verification tools for cryptography. This work will focus on the improvement of the EasyCrypt’s term rewriting system, replacing it with a symbolic abstract machine. In order to do that, we will previously study and implement two widely known abstract machines, the Krivine Machine and the ZAM, introducing some variations and studying their differences from a practical point of view.

Configuración formal de los rosetones románicos de la ciudad de Zamora

La presente tesis estudia los rosetones románicos de la ciudad de Zamora. La elección del tema tiene como objetivo profundizar en el conocimiento de estos elementos ya que la información existente sobre ellos es muy escasa. El análisis de estos rosetones se ha realizado desde una perspectiva globalizadora que abarca aspectos tales como los geográficos, morfológicos, funcionales, compositivos, constructivos, geométricos, ornamentales, otros. Así mismo, para el desarrollo de esta investigación se ha considerado necesario el estudio de temas históricos, estilísticos, simbólicos, religiosos, culturales, etc., que aportan el marco contextual que permiten su mejor entendimiento. El estudio de cada rosetón ha permitido implementar y desarrollar un método de trabajo analítico basado en el estudio particular de una serie de aspectos como los anteriormente mencionados, así como plantear una estrategia que permite la reconstitución gráfica de los rosetones, basándose en un sistema de módulos que facilitan trabajar de acuerdo a las proporciones de los elementos; hecho que permite acercarnos con gran exactitud a la representación del objeto real cuando se carece de medidas. El desarrollo de esta investigación ha llevado a establecer entre otras cosas que la definición de “ventana circular” que se le atribuye a los rosetones románicos no es acertada, puesto que la función que cumplen en el edificio religioso es más bien de carácter simbólico. ABSTRACT This thesis studies the Romanesque rose windows of the Zamora city. The choice of topic is intended to deepen the knowledge of these elements as the existing information about them is very scarce. The analysis of these rose windows was made from a global perspective covering aspects such as geographic, morphological, functional, compositional, construction, geometric, ornamental, other. Also, for the development of this research it was considered necessary to study historical, stylistic, symbolic, religious, cultural issues, etc., that provide the contextual framework that allow for better understanding. The study of each rose windows has allowed implement and develop a method of analytical work based on the particular study a number of issues such as those mentioned above, as well as devise a strategy that allows the graphic reconstitution of the rose windows, based on a system of modules facilitate work according to the proportions of the elements; made with great precision approach allows the representation of the real thing when it lacks measures. The development of this research has led to establish among other things that the definition of "circular window" that is attributed to the Romanesque rose windows is not successful because the role in the religious building is rather symbolic.