A aula de orquestra como laboratório para a criatividade

Relatório de estágio de mestrado em Ensino da Música

Desenvolvimento do pensamento computacional com recurso ao Scratch: uma experiência com alunos do 8ºano

Relatório de estágio de mestrado em Ensino de Informática

Pervasive decision support to predict football corners and goals by means of data mining

Football is considered nowadays one of the most popular sports. In the betting world, it has acquired an outstanding position, which moves millions of euros during the period of a single football match. The lack of profitability of football betting users has been stressed as a problem. This lack gave origin to this research proposal, which it is going to analyse the possibility of existing a way to support the users to increase their profits on their bets. Data mining models were induced with the purpose of supporting the gamblers to increase their profits in the medium/long term. Being conscience that the models can fail, the results achieved by four of the seven targets in the models are encouraging and suggest that the system can help to increase the profits. All defined targets have two possible classes to predict, for example, if there are more or less than 7.5 corners in a single game. The data mining models of the targets, more or less than 7.5 corners, 8.5 corners, 1.5 goals and 3.5 goals achieved the pre-defined thresholds. The models were implemented in a prototype, which it is a pervasive decision support system. This system was developed with the purpose to be an interface for any user, both for an expert user as to a user who has no knowledge in football games.

A realização do sujeito em complementos infinitivos de verbos causativos e percetivos no português língua de herança

Dissertação de mestrado em Ciências da Linguagem

Modelo de gestão integrada dos contratos públicos eletrónicos orientados ao valor público

Tese de Doutoramento em Tecnologias e Sistemas de Informação.

Pacifier : construção e aplicação de um programa para pais nos cuidados de saúde primários

Este trabalho teve como objetivo fundamental a construção, aplicação e avaliação dos efeitos de um programa de educação parental universal, numa vertente preventiva, designado como – Pacifier – visando a sua implementação nos Cuidados de Saúde Primários, a pais de crianças dos 0 aos 6 meses e com carácter domiciliário. Foi construído com base numa revisão da literatura e práticas baseadas em evidência sobre parentalidade positiva e programas de educação parental e posteriormente aplicado a quatro mães e dois pais – dois casais e duas mães –, sendo que os efeitos foram avaliados de acordo com um modelo de estudos de caso múltiplos, constituídos por quatro famílias. Neste sentido, de modo a medir os objetivos que definimos para o programa, realizámos uma avaliação inicial e final com os instrumentos adaptados Sentido de Competência Parental e Inventário sobre o Conhecimento de Desenvolvimento Infantil. Ainda incluímos um questionário final relativo à Satisfação dos Pais com o Programa. No que respeita aos resultados, nos quatro estudos de caso verificaram-se melhorias nos resultados de ambos os instrumentos aplicados, o que nos permite considerar que o programa foi eficaz e melhorou o sentido de competência parental assim como o conhecimento do desenvolvimento infantil nestes pais. Por último, os pais mostraram uma grande satisfação com o programa.

Sistemas de Tipos para Verificación de Programas Concurrentes. Type Systems for Concurrent Programs Verification.

La programación concurrente es una tarea difícil aún para los más experimentados programadores. Las investigaciones en concurrencia han dado como resultado una gran cantidad de mecanismos y herramientas para resolver problemas de condiciones de carrera de datos y deadlocks, problemas que surgen por el mal uso de los mecanismos de sincronización. La verificación de propiedades interesantes de programas concurrentes presenta dificultades extras a los programas secuenciales debido al no-determinismo de su ejecución, lo cual resulta en una explosión en el número de posibles estados de programa, haciendo casi imposible un tratamiento manual o aún con la ayuda de computadoras. Algunos enfoques se basan en la creación de lenguajes de programación con construcciones con un alto nivel de abstración para expresar concurrencia y sincronización. Otros enfoques tratan de desarrollar técnicas y métodos de razonamiento para demostrar propiedades, algunos usan demostradores de teoremas generales, model-checking o algortimos específicos sobre un determinado sistema de tipos. Los enfoques basados en análisis estático liviano utilizan técnicas como interpretación abstracta para detectar ciertos tipos de errores, de una manera conservativa. Estas técnicas generalmente escalan lo suficiente para aplicarse en grandes proyectos de software pero los tipos de errores que pueden detectar es limitada. Algunas propiedades interesantes están relacionadas a condiciones de carrera y deadlocks, mientras que otros están interesados en problemas relacionados con la seguridad de los sistemas, como confidencialidad e integridad de datos. Los principales objetivos de esta propuesta es identificar algunas propiedades de interés a verificar en sistemas concurrentes y desarrollar técnicas y herramientas para realizar la verificación en forma automática. Para lograr estos objetivos, se pondrá énfasis en el estudio y desarrollo de sistemas de tipos como tipos dependientes, sistema de tipos y efectos, y tipos de efectos sensibles al flujo de datos y control. Estos sistemas de tipos se aplicarán a algunos modelos de programación concurrente como por ejemplo, en Simple Concurrent Object-Oriented Programming (SCOOP) y Java. Además se abordarán propiedades de seguridad usando sistemas de tipos específicos. Concurrent programming has remained a dificult task even for very experienced programmers. Concurrency research has provided a rich set of tools and mechanisms for dealing with data races and deadlocks that arise of incorrect use of synchronization. Verification of most interesting properties of concurrent programs is a very dificult task due to intrinsic non-deterministic nature of concurrency, resulting in a state explosion which make it almost imposible to be manually treat and it is a serious challenge to do that even with help of computers. Some approaches attempts create programming languages with higher levels of abstraction for expressing concurrency and synchronization. Other approaches try to develop reasoning methods to prove properties, either using general theorem provers, model-checking or specific algorithms on some type systems. The light-weight static analysis approach apply techniques like abstract interpretation to find certain kind of bugs in a conservative way. This techniques scale well to be applied in large software projects but the kind of bugs they may find are limited. Some interesting properties are related to data races and deadlocks, while others are interested in some security problems like confidentiality and integrity of data. The main goals of this proposal is to identify some interesting properties to verify in concurrent systems and develop techniques and tools to do full automatic verification. The main approach will be the application of type systems, as dependent types, type and effect systems, and flow-efect types. Those type systems will be applied to some models for concurrent programming as Simple Concurrent Object-Oriented Programming (SCOOP) and Java. Other goals include the analysis of security properties also using specific type systems.

Knowledge representation with condensed set-valued attributes

Magdeburg, Univ., Fak. für Informatik, Diss., 2012

Verification of system properties of polynomial systems using discrete-time approximations and set-based analysis

Magdeburg, Univ., Fak. für Elektrotechnik und Informationstechnik, Diss., 2015

Two new species of the Drosophila serido sibling set (Diptera, Drosophilidae)

Drosophila antonietae sp. nov. and D. gouveai sp. nov. are members of the D. buzzatii cluster of the D. repleta species group of the genus Drosophila. They can be distinguished from their cryptic species, D. borborema Vilela & Sene, 1977, D. koepferae Fontdevila & Wasserman, 1988, D. serido Vilela & Sene, 1977, and D. seriema Tidon-Sklorz & Sene, 1995 by morphological, genetic and ecological criteria.

On the set of subrings wich are directed unions of Artinian subrings

The paper contributes to the investigation of zero-dimensional rings which can be written as a directed union of Artinian subrings. We give conditions on DU(R) in order to be nonempty.

Testing of stair climbing point-of-choice prompts in Barcelona at an outdoor set of stairs and scalators on the Montjuïc site

Regular stair climbing has well-documented health dividends, such as increased fitness and strength, weight loss and reduced body fat, improved lipid profiles and reduced risk of osteoporosis. The general absence of barriers to participation makes stair climbing an ideal physical activity (PA) for health promotion. Studies in the US and the UK have consistently shown that interventions to increase the accumulation of lifestyle PA by climbing stairs rather than using the escalators are effective. However, there are no previous in Catalonia. This project tested one message for their ability to prompt travelers on the Montjuïc site to choose the stairs rather than the escalator when climbing up the Monjuïc hill. One standard message, " Take the stairs! 7 minutes of stair climbing a day protects your heart" provided a comparison with previous research done in the UK. Translated into Catalan and Spanish, it was presented on a poster positioned at the point of choice between the stairs and the escalator. The study used a quasi-experimental, interrupted time series design. Travelers, during several and specific hours on two days of the week, were coded for stair or escalator use, gender, age, ethnic status, presence of accompanying children or bags by one observer. Overall, the intervention resulted in a 81% increase in stair climbing. In the follow-up period without messages, stair climbing dropped out to baseline levels. This preliminary study showed a significant effect on stair use. However, caution is needed since results are based on a small sample and, only a low percentage of the sample took the stairs at baseline or the intervention phase . Future research on stair use in Catalonia should focus on using bigger samples, different sites (metro stations, airports, shopping centers, etc) , different messages and techniques to promote stair climbing.

Renormalization and α-limit set for expanding Lorenz maps

We establish a one-to-one correspondence between the renormalizations and proper totally invariant closed sets (i.e., α-limit sets) of expanding Lorenz map, which enable us to distinguish periodic and non-periodic renormalizations. We describe the minimal renormalization by constructing the minimal totally invariant closed set, so that we can define the renormalization operator. Using consecutive renormalizations, we obtain complete topological characteriza- tion of α-limit sets and nonwandering set decomposition. For piecewise linear Lorenz map with slopes ≥ 1, we show that each renormalization is periodic and every proper α-limit set is countable.

Integració de tècniques per a la comprovació eficient de restriccions d'integritat en la generació de programari per entorns web

Estudi elaborat a partir d’una estada al Politecnico de Milano, Itàlia, entre gener i juny del 2006. Un dels principals objectius de l’Enginyeria del Programari és automatitzar el màxim possible el procés de desenvolupament del programari, reduint costos mitjançant la generació automàtica del programari a partir de la seva especificació. Per assolir-ho, entre altres, cal resoldre el problema de la comprovació eficient de restriccions, que són una part fonamental de l’especificació del programari. Aquest és precisament l’àmbit en què s’està desenvolupant una tesi que presentarà un mètode que poden integrar totes les eines generadores de codi per tal d’assolir una implementació eficient de les restriccions d’integritat. En l’actual fase del projecte s’ha treballat per validar el mètode de la tesi, optimitzant-lo pel cas específic de les aplicacions web i estendre’l per poder tractar també aplicacions basades en workflows. Pel que fa a l’optimització del mètode per aplicacions web, s’han definit una sèrie de paràmetres que permeten configurar la implementació del mètode tenint en compte les necessitats específiques de rendiment de cada aplicació web en particular. Respecte als workflows (cada cop més populars i que s’usen com a definició d’alt nivell per a les aplicacions a desenvolupar) s’ha estudiat quins són els tipus de restriccions que impliquen i com després es pot aplicar el mètode de la tesi sobre aquestes restriccions per tal de generar de forma eficient també les aplicacions basades en workflows.