Syftet med uppsatsen är att utreda hur rätten till liv har ett samband med tvångsförsvinnande enligt den Inter-Amerikanska Domstolen om Mänskliga Rättigheter. För att uppnå uppsatsens syfte genomförs en rättsutredning kring gällande rätt, där en rättsdogmatisk metod och fallstudie applicerats. Uppsatsen kommer vidare att analyseras mot bakgrund av en rättsvetenskaplig teori, där relevant rättspraxis som den Inter-Amerikanska Domstolen om Mänskliga Rättigheter bemött samt en kortfattad genomgång av kontexters påverkan. Under utredningen av de konventionella källorna finns vissa krav för att uppfylla om en stat kan hållas ansvarig. Utifrån det och med de grova mänskliga rättighets kränkningarna staten utfärdat i åtanke, är bevisbördan och statsansvar av stor relevans för att klargöra sambandet mellan rättigheten och handlingen. Uppsatsen avslutas med att konkludera att det råder brister i hur den Inter-Amerikanska Domstolen om Mänskliga Rättigheter arbetar mot att förvara och skydda Mänskliga Rättigheter i fall som berör tvångsförsvinnande. / The aim of this paper is to evaluate how the right to life has a connection with the forced disappearance of persons, according to the Inter-American Court on Human Rights. In order to reach this purpose, a legal dogmatic approach and a case study is used, in the light of a legal theory. The research concerns relevant cases that the Inter-American Court on Human Rights has been confronted with, and, to clarify the contextual importance, a brief explanation on the surroundings is provided. With the grave human rights violations committed by State authorities in mind, the thesis shows that the standard of proof, and principle of state responsibility, becomes of importance, in order to be able to determine whether the right to life is violated in cases of forced disappearance. The essay will conclude that the issue prevails defectiveness in relation to preventing and protecting human rights in cases of forced disappearance of persons.

Cette thèse propose de nouveaux protocoles cryptographiques, plus efficaces que l’existant, et qui permettent aux utilisateurs du nuage informatique (le cloud) de vérifier (i) la bonne conservation des données externalisées et (ii) l'exécution correcte de calculs externalisés. Nous décrivons d'abord un protocole cryptographique qui génère des preuves de récupérabilité, qui permettent aux propriétaires de données de vérifier que le cloud stocke leurs données correctement. Nous détaillons ensuite trois schémas cryptographiques pour vérifier l’exactitude des calculs externalisés en se focalisant sur trois opérations fréquentes dans les procédures de traitement de données, à savoir l’évaluation de polynômes, la multiplication de matrices et la recherche de conjonction de mots-clés. La sécurité de nos solutions est analysée dans le cadre de la sécurité prouvable et nous démontrons également leur efficacité grâce à des prototypes. Nous présentons également A-PPL, un langage de politiques pour l’imputabilité qui permet l'expression des obligations de responsabilité et de traçabilité dans un format compréhensible par la machine. Nous espérons que nos contributions pourront encourager l'adoption du cloud par les entreprises encore réticentes à l’idée d'utiliser ce paradigme prometteur. / This thesis proposes more efficient cryptographic protocols that enable cloud users to verify (i) the correct storage of outsourced data and (ii) the correct execution of outsourced computation. We first describe a cryptographic protocol that generates proofs of retrievability, which enable data owners to verify that the cloud correctly stores their data. We then detail three cryptographic schemes for verifiable computation by focusing on three operations frequent in data processing routines, namely polynomial evaluation, matrix multiplication and conjunctive keyword search. The security of our solutions is analyzed in the provable security framework and we also demonstrate their efficiency thanks to prototypes. We also introduce A-PPL, an accountability policy language that allows the expression of accountability obligations into machine-readable format. We expect our contributions to foster cloud adoption by organizations still wary of using this promising paradigm.

The objective of this thesis is to enhance the TC1500 LAB converter, which is anelectrical train converter to be waterproof up to a height of 650 [mm] from raillevel, addressing a pressing need in railway systems. The critical components ofthe converter have been identified for consideration. Using Freddy Olsson'smethod and the concept screening method, various designs were generated, withone alternative design chosen for each critical part identified. The result of thisproject includes innovative designs that fulfill both the company's requirementsand the functional needs identified during the project. Each design's resilienceunder various loads and environmental conditions was assessed using simulationsconducted in SimSolid, all of which successfully met the defined requirements.An actual experiment was done to validate the simulation model used in SimSolid.This work not only advances our understanding of converter design andwaterproofing, but also provides practical solutions for enhancing the durability ofrailway systems. The insights from this thesis serve as valuable resources forfuture research and the improvement of similar components in other railwaysystems.

[pt] O objetivo desta dissertação é construir um tableaux linear intuicionista a partir de um cálculo de sequentes relevante clássico. Os passos principais dessa construção são: i) tradução das regras do cálculo dos sequentes relevante clássico para regras de tableaux (capítulo 3), usando a estratégia apresentada por D Agostino et al. em Tableau Methods for Substructural Logic. ii) construção de um tableaux linear clássico através da linearização do tableaux clássico relevante (capítulo 4). iii) apresentar um tableau intuicionista ao estilo Fitting, em que são adicionados rótulos T s e F s às fórmulas (capítulo 5). / [en] The main goal of this master tesis is intuitionistic linear tableaux from a relevant sequent calculus. The central steps are: i) Apply D Agostino et al. strategy to translate classical relevant sequent calculus rules to tableaux rules for classical relevant logic (Chapter 3). ii) Use Meyer et al. strategy to linearize the classical relevant tableaux (Chapter 4). iii) Build a new intuicionistic linear tableaux with Fitting labels.

Companies developing integrated circuits are expected to enhance their products’ performance at every new release, while reducing size and power consumption. The demand for more elaborate and diverse functionality, together with a reduced time-to-market, irremediably raises costs and increases the probability of bugs. Even high-performance ASICs are not immune: the complexity of the design flow implies significant non-recurring engineering and production costs. Similar challenges affect the FPGA design flow, where the allocation of programmable logic requires considerable engineering effort. Moreover, due to the limited visibility of internal operations, isolating and back-tracing malfunctions are open challenges. Ericsson AB is exploring novel approaches to deal with this complex ecosystem.This thesis investigates the feasibility and the benefits of a flexible design approach, by developing and characterizing a Proof-of-Concept (PoC) transceiver handler for highspeed link applications. The flexibility lies in the software-based controller, exploited to handle the reset and dynamic reconfiguration of a transceiver physical layer (PHY). The objective of the software implementation is to simplify error detection and on-the-fly modification compared to a traditional HW-based controller. The firmware, running on a Nios II soft-core processor, drives the control signals while monitoring the transceiver’s status. Unexpected synchronization losses are handled by a dedicated Interrupt Service Routine.The correct HW/SW interaction has been tested through simulation, whereas the software profiling proves that the timing requirements are met (only 167µs are spent on the reset sequence). Finally, the PoC has been benchmarked against an analogous system with a traditional HW-based controller, to evaluate the drawbacks of the introduction of a soft-core processor (in terms of logic utilization and power consumption).Despite the promising engineering effort reduction, further research is required to scale up the system and move from the PoC stage towards product release. / Företag som utvecklar integrerade kretsar förväntas öka prestandan i nya produkter, och samtidigt reducera storlek samt effektförbrukning. Efterfrågan på mer komplicerad funktionalitet, tillsammans med förkortad time-to-market, orsakar oundvikligen högre kostnader och ökad sannolikhet för buggar. Även högprestererande ASICs drabbas av detta: det komplicerade designflödet resulterar i signifikanta engångskostnader för teknisk utveckling samt tillverkning. Liknande utmaningar påverkar designflödet hos FPGA:er, där allokeringen av programmerbar logik kräver påtagligt utvecklingsarbete. Eftersom insynen i interna operationer är begränsad är isolation och spårning av fel aktuella utmaningar. Ericsson AB utforskar nya tillvägagångssätt för att hantera sådana komplexa ekosystem.Det här examensarbetet undersöker genomförbarheten och fördelarna med ett flexibelt tillvägagångssätt för design, genom utveckling och karaktärisering av ett konceptbevis för en transceiver-hanterare för höghastighetslänkar. Flexibiliteten realiseras med en mjukvarubaserad kontroller som används för att hantera återställningssignaler och dynamisk rekonfigurering av en transceiver (PHY). Målet med mjukvaruimplementationen är att förenkla feldetektion samt modifikation i realtid, jämfört med en traditionell hårdvarubaserad kontroller. Mjukvaran, som körs på en Nios II soft-coreprocessor, driver styrsignaler och övervakar transceiverns status. Oväntade synkroniseringsförluster hanteras av en dedikerad avbrottshanteringsrutin. Simulationer har gjorts för att testa korrekt interaktion mellan hårdvara och mjukbara. Profilering av mjukvara visar att timingkraven uppfylls (återställningssekvensen tar endast 167 µs). Avslutningsvis har konceptbeviset jämförts med ett likvärdigt hårdvarubaserat system för att utvärdera nackdelarna med introduktionen av Nios II (vad gäller resursanvändningen och effektförbrukningen).Trots lovande resultat är den begränsade detaljnivån i konceptbeviset en tydlig begränsning. Vidare arbete måste göras för att skala upp systemet och generalisera det här nya tillvägagångssättet.

Our research is in the general area of String Algorithms and Combinatorics on Words. Specifically, we study a generalization of square-free strings, shuffle properties of strings, and formalizing the reasoning about finite strings. The existence of infinitely long square-free strings (strings with no adjacent repeating word blocks) over a three (or more) letter finite set (referred to as Alphabet) is a well-established result. A natural generalization of this problem is that only subsets of the alphabet with predefined cardinality are available, while selecting symbols of the square-free string. This problem has been studied by several authors, and the lowest possible bound on the cardinality of the subset given is four. The problem remains open for subset size three and we investigate this question. We show that square-free strings exist in several specialized cases of the problem and propose approaches to solve the problem, ranging from patterns in strings to Proof Complexity. We also study the shuffle property (analogous to shuffling a deck of cards labeled with symbols) of strings, and explore the relationship between string shuffle and graphs, and show that large classes of graphs can be represented with special type of strings. Finally, we propose a theory of strings, that formalizes the reasoning about finite strings. By engaging in this line of research, we hope to bring the richness of the advanced field of Proof Complexity to Stringology. / Thesis / Doctor of Philosophy (PhD)

No description available.

No description available.

The paper contains a proof of completeness of a goal-directed inference system for general E-unification with eager Variable Elimination. The proof is based on an analysis of a concept of ground, equational proof. The theory of equational proofs is developed in the first part. Solving variables in a goal is then shown to be reflected in defined transformations of an equational proof. The termination of these transformations proves termination of inferences with eager Variable Elimination.

<p>In this thesis we are concerned with the complexity of formalizing reasoning in Combinatorial Matrix Theory (CMT). We are interested in the strength of the bounded arithmetic theories necessary in order to prove the fundamental results of this field. Bounded Arithmetic can be seen as the uniform counterpart of Propositional Proof Complexity.</p> <p>Perhaps the most famous and fundamental theorem in CMT is the K{\"o}nig's Min-Max Theorem $(\KMM)$ which arises naturally in all areas of combinatorial algorithms. As far as we know, in this thesis we give the first feasible proof of $\KMM$. Our results show that Min-Max reasoning can be formalized with uniform Extended Frege.</p> <p>We show, by introducing new proof techniques, that the first order theory $\LA$ with induction restricted to $\Sigma_1^B$ formulas---i.e., restricted to bounded existential matrix quantification---is sufficient to formalize a large portion of CMT, in particular $\KMM$. $\Sigma_1^B$-$\LA$ corresponds to polynomial time reasoning, also known as $\ELA$.</p> <p>While we consider matrices over $\{0,1\}$, the underlying ring is $\mathbb{Z}$, since we require that $\Sigma A$ compute the number of 1s in the matrix $A$ (which for a 0-1 matrix is simply the sum of all entries---meaning $\Sigma A$). Thus, over $\mathbb{Z}$, $\LA$ translates to $\TC^0$-Frege, while, as mentioned before, $\ELA$ translates into Extended Frege.</p> <p>In order to prove $\KMM$ in $\ELA$, we need to restrict induction to $\Sigma_1^B$ formulas. The main technical contribution is presented in Claim~4.3.4, ~Section~4.3.3. Basically, we introduce a polynomial time procedure, whose proof of correctness can be shown with $\ELA$, that works as follow: given a matrix of size $e \times f$ such that $e\leq f$, where the minimum cover is of size $e$, our procedure computes a maximum selection of size $e$, row by row.</p> <p>Furthermore, we show that Menger's Theorem, Hall's Theorem, and Dilworth's Theorem---theorems related to $\KMM$---can also be proven feasibly; in fact, all these theorems are equivalent to KMM, and the equivalence can be shown in $\LA$. We believe that this captures the proof complexity of Min-Max reasoning rather completely.</p> <p>We also present a new Permutation-Based algorithm for computing a Minimum Vertex Cover from a Maximum Matching in a bipartite graph. Our algorithm is linear-time and computationally very simple: it permutes the rows and columns of the matrix representation of the bipartite graph in order to extract the vertex cover from a maximum matching in a recursive fashion. Our Permutation-Based algorithm uses properties of $\KMM$ Theorem and it is interesting for providing a new permutation---and CMT---perspective on a well-known problem.</p> / Doctor of Philosophy (PhD)