A Write-Based Solver for SAT Modulo the Theory of Arrays

The extensional theory of arrays is one of the most important ones for applications of SAT Modulo Theories (SMT) to hardware and software verification. Here we present a new T-solver for arrays in the context of the DPLL(T) approach to SMT. The main characteristics of our solver are: (i) no translation of writes into reads is needed, (ii) there is no axiom instantiation, and (iii) the T-solver interacts with the Boolean engine by asking to split on equality literals between indices. As far as we know, this is the first accurate description of an array solver integrated in a state-of-the-art SMT solver and, unlike most state-of-the-art solvers, it is not based on a lazy instantiation of the array axioms. Moreover, it is very competitive in practice, specially on problems that require heavy reasoning on array literals

Description of diffusive and propagative behavior on fractals

The known properties of diffusion on fractals are reviewed in order to give a general outlook of these dynamic processes. After that, we propose a description developed in the context of the intrinsic metric of fractals, which leads us to a differential equation able to describe diffusion in real fractals in the asymptotic regime. We show that our approach has a stronger physical justification than previous works on this field. The most important result we present is the introduction of a dependence on time and space for the conductivity in fractals, which is deduced by scaling arguments and supported by computer simulations. Finally, the diffusion equation is used to introduce the possibility of reaction-diffusion processes on fractals and analyze their properties. Specifically, an analytic expression for the speed of the corresponding travelling fronts, which can be of great interest for application purposes, is derived

Toward a comparative analysis of coming and going verbs in Spanish, German, and Polish

This work deals with coming and going verbs in three typologically distinct languages: a Romance one (Spanish), a Germanic one (German) and a Slavic one (Polish) within Fillmore`s (1966, 1971, 1975, 1982, 1983) framework. On the grounds of data description it is shown that visible linguistic phenomena, such as deixis or Aktionsart related clearly to the coming and going verbs, can be transcended, resorting to the more abstract notion called by the author, following Winston (1987) and Speas and Tenny (2003), “viewpoint”.

The word problem distinguishes counter languages

Counter automata are more powerful versions of finite state automata where addition and subtraction operations are permitted on a set of n integer registers, called counters. We show that the word problem of Zn is accepted by a nondeterministic m-counter automaton if and only if m &= n.

Disseny i implementació hardware d'algorismes de reconeixement de caràcters per comptadors d'aigua

Aquest projecte consisteix en l'estudi, comparació i implementació en hardware d'algoritmes de reconeixement de caràcters per integrar en un sistema intel·ligent de captura d'imatges. Aquest sistema, integrat per una càmera amb format i característiques específiques i que anirà acoblat a un comptador d'aigua tradicional, en captarà imatges i les enviarà per RF al punt de recepció de la companyia. L'objectiu principal consisteix en aconseguir un disseny que redueixi al màxim la quantitat d'informació per transmetre, tenint en compte les limitacions de l'entorn.

Simulació d'arquitectures VLIW

L'objectiu d'aquest projecte es dissenyar i implementar en Java una interfície gràfica que permeti simular l'arquitectura VLIW. Ha d'interactuar amb un simulador ja existent, VEX, i amb l'usuari. VEX permet analitzar, desenvolupar i depurar codi escrit en C sobre un processador VLIW configurable, des dels recursos hardware fíns al comportament de la "caché". L'interfície gràfica desenvolupada es diu JavaVEX. Té el gran avantatge d'evitar la introducció de les comandes de text que necesita VEX perquè son substituïdes per elements. És una eina més intuïtiva, ràpida i eficient. JavaVEX mostra informació sobre el codi C traduït a instruccions VLIW de fins a 4 operacions. També mostra els resultats de les instrucciones VLIW simulades. JavaVEX s'ha incorporat a un LiveCD. Així es pot executar l'aplicació sobre qualsevol ordinador. La finalitat docent de JavaVEX és ser utilitzada en les pràctiques de l'assignatura Arquitectura per a Computadors 2.

Recepción y difusión internacionales de Mercè Rodoreda: obra original, crítica y traducción

RESUM Recepción y difusión internacionales de Mercè Rodoreda: obra original, crítica y traducción té per objecte determinar la recepció i la difusió de l’obra original de Mercè Rodoreda, així com de l’obra crítica i de les traduccions, en el context internacional a partir de la interpretació de quatre bases de dades: obra literària de Mercè Rodoreda, obra crítica de Mercè Rodoreda i la seva obra, traductors i traduccions en funció de la llengua i de l’obra i, per últim, presència documental de Mercè Rodoreda a les Biblioteques Nacionals del món. El treball de recerca s’estructura de la següent manera. En primer lloc, plantegem i delimitem el tema, els objectius, la metodologia i la descripció de les bases de dades. Acte seguit, interpretem les bases de dades i exposem algunes consideracions. A continuació, presentem les conclusions finals que hem desenvolupat en cadascun dels àmbits en els que se centra la nostra recerca, així com el projecte de tesi doctoral i les noves línies de recerca. Per últim, exposem la bibliografia i els annexes, en els que incloem les bases de dades i reproduim els estudis traductològics comentats en el treball. Amb l’elaboració d’aquest treball de recerca pretenem, entre d’altres, donar a conèixer els gèneres literaris que va cultivar Mercè Rodoreda; recopilar l’obra crítica al voltant de l’autora i distingir la seva temàtica per determinar el nombre d’estudis crítics sobre traducció; identificar quins títols de l’obra de Mercè Rodoreda s’han traslladat a altres llengües, així com confirmar quina és l’obra més traduïda i quines les llengües a les que s’ha traslladat la seva obra; i, per últim, constatar la presència d’obres originals, estudis crítics i traduccions a les Biblioteques Nacionals del món i identificar-ne les possibles àrees d’expansió.

Motion analysis in terms of wireless video capsule endoscopy

El treball presentat suposa una visió general de l'"Endoscopia amb Càpsula de Vídeo Wireless" i la inspecció de sequències de contraccions intestinals amb les últimes tecnologies de visió per computador. Després de la observació preliminar dels fonaments mèdics requerits, la aplicació de visió per computador es presenta en aquestos termes. En essència, aquest treball proveïx una exhaustiva selecció, descripció i avaluació de cert conjunt de mètodes de processament d'imatges respecte a l'anàlisi de moviment, en el entorn de seqüències d'imatges preses amb una càpsula endoscòpica. Finalment, es presenta una aplicació de software per configurar i emprar de forma ràpida i fàcil un entorn experimental.

Sistema de monitorització Open Source: projecte d'empresa per Computer Technology Catalunya

L’objectiu del projecte consisteix en l’estudi, simulació i implantació d’un conjunt d’aplicacions que permeten tenir un control sobre possibles problemes que puguin succeir a la nostra xarxa. Aquest projecte és la solució als problemes de detecció d’errors en el funcionament de les infraestructures de networking de les que disposen els nostres clients.

Análisis de prestaciones de sistemas de comunicaciones inalámbricas en aplicaciones de robótica: sistema hardware

Una característica importante de la robótica es la comunicación entre sistema base y robot que puede establecerse de forma remota. Ello representa la base del proyecto que se describe a continuación, el cual se descompone de dos partes, una por cada miembro del proyecto: Sistema software y sistema hardware. En el sistema software analizaremos las diferentes tecnologías inalámbricas (características, funcionamiento, seguridad, etc.), se realizará una comparativa de los diferentes módulos de comunicación y finalmente decidiremos aquellos que nos interesa para la implementación en Radiofrecuencia (RF) y Bluetooth. En este sistema también estudiaremos la interfaz gráfica que se utilizará, así como los programas creados en este entorno para realizar las implementaciones. En el sistema hardware trataremos de realizar el control de dos periféricos de forma independiente, un servomotor y un sonar, que nos servirán como ejemplo para analizar una posible comunicación entre varios robots y un PC. Por lo tanto, en este apartado analizaremos a fondo los diferentes componentes que harán posible tanto la comunicación, vía RF y Bluetooth, como el control de los diferentes dispositivos.

Mathematical description of bacterial traveling pulses

The Keller-Segel system has been widely proposed as a model for bacterial waves driven by chemotactic processes. Current experiments on E. coli have shown precise structure of traveling pulses. We present here an alternative mathematical description of traveling pulses at a macroscopic scale. This modeling task is complemented with numerical simulations in accordance with the experimental observations. Our model is derived from an accurate kinetic description of the mesoscopic run-and-tumble process performed by bacteria. This model can account for recent experimental observations with E. coli. Qualitative agreements include the asymmetry of the pulse and transition in the collective behaviour (clustered motion versus dispersion). In addition we can capture quantitatively the main characteristics of the pulse such as the speed and the relative size of tails. This work opens several experimental and theoretical perspectives. Coefficients at the macroscopic level are derived from considerations at the cellular scale. For instance the stiffness of the signal integration process turns out to have a strong effect on collective motion. Furthermore the bottom-up scaling allows to perform preliminary mathematical analysis and write efficient numerical schemes. This model is intended as a predictive tool for the investigation of bacterial collective motion.

Mejorando la robustez de aplicaciones frente a fallos transitorios

Computer chips implementation technologies evolving to obtain more performance are increasing the probability of transient faults. As this probability grows and on-chip solutions are expensive or tend to degrade processor performance, the efforts to deal with these transient faults in higher levels (such as the operating system or even at the application level) are increasing. Mostly, these efforts are trying to avoid silent data corruptions using hardware, software and hybrid based techniques to add redundancy to detect the errors generated by the transient faults. This work presents our proposal to improve the robustness of applications with source code based transformation adding redundancy. Also, our proposal takes account of the tradeoff between the improved robustness and the overhead generated by the added redundancy.

L'ús dels clítics pronominals del català i la seva adquisició per parlants de romanès i de tagal

El nostre estudi ha analitzat els mecanismes de transferència de la L1 en dos grups de parlants, un que té el romanès i l’altre el tagal com a llengües mare, en el procés d’aprenentatge del català com a L2. En concret ens hem centrat en l’estudi de l’ús dels clítics pronominals, una de les parts de la gramàtica catalana més apassionant per les seves idiosincràsies i la seva diversitat formal. L’ús d’aquest tipus de pronoms és un aspecte que resulta complicat d’adquirir per parlants de llengües en què no existeixen o on l’ús que en fan és diferent. En el nostre estudi, ens hem basat inicialment en la descripció de les característiques fonamentals dels clítics pronominals del català, del romanès i del tagal, a partir de bibliografia especialitzada i més general, i, en el cas del català, fent servir també la pròpia competència. Després d’aquest apartat més descriptiu, hem utilitzat un corpus d’entrevistes fetes en català a dos grups de parlants, el primer amb aprenents de català que tenen el romanès com a L1 i el segon amb aprenents de català que tenen el tagal com a L1, per analitzar quantitativament i qualitativament l’ús dels clítics pronominals. Un altre grup d’entrevistes, aquesta vegada a persones autòctones (català L1), ens ha servit com a grup de control. El nostre estudi dóna suport a la hipòtesi que atorga una importància especial a la transferència de la L1 en l’adquisició d'una segona llengua en general, i en la dels clítics pronominals d’una llengua romànica, en particular. Els resultats mostren que hi ha diferències entre els dos grups d'aprenents que són estadísticament significatives (ús del programa SPSS) i poden ser atribuïdes a les característiques de la L1.

Desarrollo de software para el procesado numérico en tarjetas gráficas

Debido al gran número de transistores por mm2 que hoy en día podemos encontrar en las GPU convencionales, en los últimos años éstas se vienen utilizando para propósitos generales gracias a que ofrecen un mayor rendimiento para computación paralela. Este proyecto implementa el producto sparse matrix-vector sobre OpenCL. En los primeros capítulos hacemos una revisión de la base teórica necesaria para comprender el problema. Después veremos los fundamentos de OpenCL y del hardware sobre el que se ejecutarán las librerías desarrolladas. En el siguiente capítulo seguiremos con una descripción del código de los kernels y de su flujo de datos. Finalmente, el software es evaluado basándose en comparativas con la CPU.

Teaching foreign languages through translation: considering multiple intelligences

Aquest treball de recerca tracta de la relació existent entre pedagogia, traducció, llengües estrangeres i intel•ligències múltiples. El debat sobre si la traducció és una eina útil a la classe de llengües estrangeres és un tema actual sobre el qual molts investigadors encara indaguen. Estudis recents, però, han demostrat que qualsevol tasca de traducció -en la qual s’hi poden incloure treballs amb les diferents habilitats- és profitosa si la considerem un mitjà, no una finalitat en ella mateixa. Evidentment, l’ús de la traducció dins l’aula és avantatjosa, però també hem de tenir presents certs desavantatges d’aquesta aplicació. Un possible desavantatge podria ser la creença que, al principi, molta gent té referent a l’equivalència, paraula per paraula, d’una llengua vers una altra. Però després de presentar vàries tasques de traducció als estudiants, aquests poden arribar a controlar, fins i tot, les traduccions inconscients i poden assolir un cert nivell de precisió i flexibilitat que val la pena mencionar. Però l’avantatge principal és que s’enfronten a una activitat molt estesa dins la societat actual que combina dues llengües, la llengua materna i la llengua objecte d’estudi, per exemple. De tot això en podem deduir que utilitzar la llengua materna a la classe no s’ha de considerar un crim, com fins ara, sinó una virtut, evidentment si és emprada correctament. En aquest treball de recerca s’hi pot trobar una síntesi tant de les principals teories d’adquisició i aprenentatge de llengües com de les teories de traducció. A la pregunta de si les teories, tant de traducció com de llengües estrangeres, s’haurien d’ensenyar implícita o explícitament, es pot inferir que segons el nivell d’estudis on estiguin els aprenents els convindrà aprendre les teories explícitament o les aprendran, de totes maneres, implícitament. Com que qualsevol grup d’estudiants és heterogeni -és a dir que cada individu té un ritme i un nivell d’aprenentatge concret i sobretot cadascú té diferents estils de percepció (visual, auditiu, gustatiu, olfactiu, de moviment) i per tant diferents intel•ligències-, els professors ho han de tenir en compte a l’hora de planificar qualsevol programa d’actuació vers els alumnes. Per tant, podem concloure que les tasques o projectes de traducció poden ajudar als alumnes a aprendre millor, més eficaçment i a aconseguir un aprenentatge més significatiu.