Magíster en Ciencias, Mención Computación / Los tipos refinados (Refinement Types) son una técnica efectiva de verificación basada en lenguajes que extienden la expresividad de los sistemas de tipos tradicionales incluyendo la posibilidad de restringir valores usando predicados lógicos. Sin embargo, como cualquier otra disciplina de tipos expresiva, obligan a los programadores a lidiar con las estrictas restricciones impuestas por los tipos. Esto puede resultar ser demasiado tedioso para los programadores, especialmente en etapas tempranas de desarrollo donde el código cambia constantemente. Nosotros conjeturamos que esta rigidez no deseada puede obstaculizar la adopción de los tipos refinados. Los tipos graduales (Gradual Typing) permiten combinar la flexibilidad de los lenguajes dinámicamente tipados con las garantías otorgadas por los lenguajes estáticamente tipados. Usando tipos graduales, los programadores pueden comenzar un desarrollo con código chequeado completamente de forma dinámica y aprovechar la flexibilidad de las construcciones idiomáticas típicas de los lenguajes dinámicos. A medida que el código se vuelve más estable, el programador o la programadora puede escoger verificar estáticamente ciertas porciones del programa, haciendo precisos los tipos en esos puntos. Finalmente, si lo desea, también puede decidir verificar el código completamente de forma estática. Los sistemas de tipos graduales aseguran una transición suave entre estos distintos niveles de precisión. Esta tesis demuestra como los tipos graduales pueden ser extendidos para soportar los tipos refinados, permitiendo una evolución suave además de interoperabilidad entre tipos simples y tipos lógicamente refinados. Al hacer esto, se atacan dos desafíos previamente inexplorados en la literatura sobre tipos graduales: lidiar con información lógica imprecisa y con la presencia de tipos dependientes. El primer desafío condujo a una noción crucial de localidad para fórmulas, mientras que el segundo desafío terminó en la definición de novedosos operadores relacionados con substitución al nivel de tipos y términos, que identifican nuevas oportunidades para errores en tiempo de ejecución en lenguajes graduales con tipos dependientes. / Este trabajo ha sido parcialmente financiado por CONICYT - PCHA Magíster Nacional 2015-22150894

This research study seeks to examine the challenges faced by School Management Teams in terms of school safety at schools in the Motetema Circuit. The problem is the disruption of lessons and the number of cases reported to the nearest police station from schools in the Motetema Circuit. Learners and educators tend to be concerned about their safety instead of concentrating on learning and teaching. Local and international articles and other sources were used in the literature review to form the basis of my study. Most of the literature studied reveals that if learners and educators do not feel safe, learning and teaching will not be effective. Learning should be conducted in a safe environment. Well-disciplined schools should be established and programmes should be developed to address school safety. Three schools were sampled in the Motetema Circuit, Greater Sekhukhune District, Limpopo Province in South Africa. Data was collected through interviews, observations and document analysis. At each school SMT members were engaged in focus group interviews for a period of one and half hours. Categories and themes were used to analyse the data collected. In consideration of all the challenges associated with school safety, School Management Teams need to have sufficient knowledge, skills and resources to promote safety at school. Copyright / Dissertation (MEd)--University of Pretoria, 2012. / Education Management and Policy Studies / unrestricted

Many computational problems require reasoning about relational structures. Examples include high-level system design, architectural configuration of network systems, reasoning about ontologies, and verification of programs with linked data structures. Traditionally, relational models are translated to propositional formulas and then solved by leveraging SAT solvers. However, SAT solvers can only reason about problems within a finite scope, i.e, concrete cardinality bounds on the relations involved. SMT solvers, on the other hand, are efficient tools that can check automatically the satisfiability of complex constraints over several domains without scope restrictions. They are used as the back-end solvers in many verification tools. To break the limitation of bounded analysis, this thesis presents a many-sorted relational logic in SMT where relations of arity n are defined as sets of n-tuples with parametrized sorts for tuple elements. We define a version of this logic as a first-order theory of finite relations where relation terms are built from relation constants and variables, set operators, and relational operators such as join, transpose, product, and transitive closure. We also present a deductive calculus for that theory and provide proofs of refutation soundness and model soundness of our calculus. In addition, we implement the calculus as a relational solver in the SMT solver CVC4, expanding its already large set of built-in theories, and evaluate the relational solver in two applications: Alloy and Ontology, showing promising results. Moreover, with the goal of improving the performance of SMT solvers in general, we present a symmetry detection algorithm to detect symmetries in SMT formulas and present a symmetry breaking algorithm to generate blocking constraints that eliminate those symmetries. We then discuss an experimental evaluation of our implementation of these algorithms in CVC4 against SMT-LIB benchmarks.

No description available.

La sûreté de fonctionnement occupe une place prépondérante dans la conception de systèmes critiques, puisqu'un dysfonctionnement peut être dangereux pour les utilisateurs ou l'environnement. Les concepteurs doivent également démontrer aux autorités de certification que les risques encourus sont acceptables. Pour cela, le concepteurs définissent une architecture contenant un ensemble de mécanismes de sûreté permettant de mitiger ou tout du moins limiter la probabilité d’occurrence des risques identifiés. L'objectif de ce travail est de développer une méthode automatique et générique de synthèse d’architecture assurant formellement le respect d’exigences de sûreté. Cette activité de synthèse est formalisée comme un problème d'exploration de l'espace des architectures c'est-à-dire trouver un candidat appartenant à un espace de recherche fini, respectant les exigences de sûreté. Ainsi nous proposons un processus de résolution complet et correct des problèmes d'exploration basé sur l'utilisation des solveurs SMT. Les contributions principales sont:1- La formalisation de la synthèse comme un problème de Satisfiabilité Modulo Théorie (SMT) afin d’utiliser les solveurs existants pour générer automatiquement une solution assurant formellement le respect des exigences;2- Le développement de méthodes d’analyse spécialement conçues pour évaluer efficacement la conformité d’une architecture vis-à-vis d’un ensemble d’exigences;3- La définition d'un langage KCR permettant de formuler les problèmes d'exploration et l'implantation des méthodes de résolution au sein de l'outil KCR Analyser. / Safety is a major issue in the design of critical systems since any failure can be hazardous to the users or the environment of such systems. In some areas, such as aeronautics, designers must also demonstrate to the certification authorities that the risks are acceptable. To do so, the designers define an architecture containing a set of security mechanisms to mitigate or at least limit the probability of occurrence of the identified risks. The objective of this work is to develop an automatic and generic method of architectural synthesis which formally ensures compliance with the safety requirements. This synthesis activity is then formalized as a design space exploration problem, i.e. find a candidate belonging to a finite set of architectures, fulfilling the safety requirements. Thus, we propose in this document a complete and correct resolution process of the design space exploration problem based on the use of SMT solvers. The main contributions are:1- the formalization of the synthesis as a problem of Satisfiability Modulo Theory (SMT) in order to use existing solvers to automatically generate a solution formally ensuring safety requirements;2- the development of analytic methods specially designed to efficiently assess the conformity of an architecture with respect to a set of safety requirements;3- the definition of a language named, KCR, allowing to formulate the design space exploration problem and the implementation of the methods of resolution presented in this work within the tool KCR Analyser.

Dans cette thèse, nous proposons une amélioration de l'automatisation des preuves dans l'assistant de preuve Coq. Cette automatisation est obtenue en intégrant à Coq les procédures de décision pour la logique propositionnelle, l'égalité et l'arithmétique linéaire constituant le noyau du solveur SMT Alt-Ergo. Cette intégration est réalisée en utilisant la technique de preuve par réflexion, qui consiste à développer en Coq ces algorithmes et à prouver formellement leur correction de manière à les exécuter directement dans l'assistant de preuve. Comme les algorithmes formalisés en Coq sont exactement ceux utilisés dans le noyau d'Alt-Ergo, notre travail permet également d'augmenter considérablement la confiance que l'on peut avoir dans ce dernier. En particulier, il utilise un algorithme original de combinaison de l'égalité modulo une théorie, inspiré de la combinaison de Shostak et appelé CC(X), et dont la justification est relativement complexe.Notre développement Coq est utilisable sous la forme de tactiques qui permettent de valider automatiquement des formules combinant logique propositionnelle, égalité et arithmétique. Afin que ces tactiques soient le plus efficaces possibles, nous avons attaché une grande importance aux performances de notre implantation Coq, et en particulier à l'utilisation de structures de données efficaces courantes, dont nous proposons ici une bibliothèque. / In this thesis, we propose new automation capabilities for the Coq proof assistant. We obtain this mechanization via an integration into Coq of decision procedures for propositional logic, equality reasoning and linear arithmetic which make up the core of the Alt-Ergo SMT solver. This integration is achieved through the reflection technique, which consists in implementing and formally proving these algorithms in Coq in order to execute them directly in the proof assistant. Because the algorithms formalized in Coq are exactly those in use in Alt-Ergo's kernel, this work significantly increases our trust in the solver. In particular, it embeds an original algorithm for combining equality modulo theory reasoning, called CC(X) and inspired by the Shostak combination algorithm, and whose justification is quite complex. Our Coq implementation is available in the form of tactics which allow one to automatically solve formulae combining propositional logic, equality and arithmetic. In order to make these tactics as efficient as may be, we have taken special care with performance in our implementation, in particular through the use of classical efficient data structures, which we provide as a separate library.

O fósforo é um elemento essencial para todas as formas de vida na Terra, podendo ser introduzido no ambiente aquático através de fontes naturais ou antropogênicas. A avaliação deste elemento em ecossistemas aquáticos é de suma importância, uma vez que ele atua na regulação da produtividade primária. Logo, este trabalho teve por objetivo avaliar a distribuição das diferentes frações do fósforo no sedimento superficial dos rios Aracaí, Carambeí e Guaçu na cidade de São Roque- SP, a fim de avaliar possíveis impactos antrópicos na qualidade das águas. Para tanto, foram realizadas quatro coletas de amostras de sedimentos nos meses de março, maio, julho e setembro de 2017 e avaliaram-se cinco pontos amostrais (A1, C1, G1, G3 e G4) sendo, dois a montante das cabeçeiras dos rios Aracaí e Carambeí e três ao longo do rio Guaçu, onde determinaram-se as concentrações de fósforo, juntamente com os parâmetros físico-químicos (umidade, granulometria, pH, e matéria orgânica). Os teores de sedimentos finos e de matéria orgânica foram os principais parâmetros ambientais correlacionados com as frações de fósforo. O método analítico utilizado foi o Protocolo desenvolvido pelo Standards, Measurements and Testing (SMT), que fracionou o fósforo dos sedimentos em: total (PT), inorgânico (PI), orgânico (PO), não apatítico (PINA) e apatítico (PIA). Observou-se que as maiores concentrações ocorreram nos sedimentos do ponto G1 da segunda coleta com 1839,6 mg kg-1 para PT e que os teores de PI foram maiores que os de PO em todas as coletas realizadas. / Phosphorus is an essential element for all forms of life on Earth and can be introduced into the aquatic environment through natural or anthropogenic sources. The evaluation of this element in aquatic ecosystems is of paramount importance, since it acts on the regulation of primary productivity. The objective of this work was to evaluate the distribution of the different phosphorus fractions in the surface sediments of the Aracaí, Carambeí and Guaçu rivers in the city of São Roque, SP, in order to evaluate possible anthropogenic impacts on water quality. Four samples of sediments were collected in March, May, July and September of 2017, and five sample points (A1, C1, G1, G3 and G4) were evaluated, two upstream of the river headwaters Aracaí and Carambeí and three along the Guaçu River, where the phosphorus concentration was determined, together with the physical-chemical parameters (humidity, grain size, pH, and organic matter). The levels of fine sediments and organic matter were the main environmental parameters correlated with the phosphorus fractions. The analytical method used was the protocol developed by Standards, Measurements and Testing (SMT), which fractionated phosphorus in: total (PT), inorganic (PI), organic (PO), non-apatite (PINA) and apatite (PIA). It was observed that the highest concentrations occurred in the sediments of the G1 point of the second collection with 1839.6 mg kg-1 for PT and that the contents of PI were higher than those of PO in all collections.

O fósforo é um elemento essencial para todas as formas de vida na Terra, podendo ser introduzido no ambiente aquático através de fontes naturais ou antropogênicas. A avaliação deste elemento em ecossistemas aquáticos é de suma importância, uma vez que ele atua na regulação da produtividade primária. Logo, este trabalho teve por objetivo avaliar a distribuição das diferentes frações do fósforo no sedimento superficial dos rios Aracaí, Carambeí e Guaçu na cidade de São Roque- SP, a fim de avaliar possíveis impactos antrópicos na qualidade das águas. Para tanto, foram realizadas quatro coletas de amostras de sedimentos nos meses de março, maio, julho e setembro de 2017 e avaliaram-se cinco pontos amostrais (A1, C1, G1, G3 e G4) sendo, dois a montante das cabeçeiras dos rios Aracaí e Carambeí e três ao longo do rio Guaçu, onde determinaram-se as concentrações de fósforo, juntamente com os parâmetros físico-químicos (umidade, granulometria, pH, e matéria orgânica). Os teores de sedimentos finos e de matéria orgânica foram os principais parâmetros ambientais correlacionados com as frações de fósforo. O método analítico utilizado foi o Protocolo desenvolvido pelo Standards, Measurements and Testing (SMT), que fracionou o fósforo dos sedimentos em: total (PT), inorgânico (PI), orgânico (PO), não apatítico (PINA) e apatítico (PIA). Observou-se que as maiores concentrações ocorreram nos sedimentos do ponto G1 da segunda coleta com 1839,6 mg kg-1 para PT e que os teores de PI foram maiores que os de PO em todas as coletas realizadas. / Phosphorus is an essential element for all forms of life on Earth and can be introduced into the aquatic environment through natural or anthropogenic sources. The evaluation of this element in aquatic ecosystems is of paramount importance, since it acts on the regulation of primary productivity. The objective of this work was to evaluate the distribution of the different phosphorus fractions in the surface sediments of the Aracaí, Carambeí and Guaçu rivers in the city of São Roque, SP, in order to evaluate possible anthropogenic impacts on water quality. Four samples of sediments were collected in March, May, July and September of 2017, and five sample points (A1, C1, G1, G3 and G4) were evaluated, two upstream of the river headwaters Aracaí and Carambeí and three along the Guaçu River, where the phosphorus concentration was determined, together with the physical-chemical parameters (humidity, grain size, pH, and organic matter). The levels of fine sediments and organic matter were the main environmental parameters correlated with the phosphorus fractions. The analytical method used was the protocol developed by Standards, Measurements and Testing (SMT), which fractionated phosphorus in: total (PT), inorganic (PI), organic (PO), non-apatite (PINA) and apatite (PIA). It was observed that the highest concentrations occurred in the sediments of the G1 point of the second collection with 1839.6 mg kg-1 for PT and that the contents of PI were higher than those of PO in all collections.

Dans l’objectif d’augmenter les performances, l’architecture des processeurs a évolué versdes plate-formes "multi-core" et "many-core" composées de multiple unités de traitements.Toutefois, trouver des moyens efficaces pour exécuter du logiciel parallèle reste un problèmedifficile. Avec un grand nombre d’unités de calcul disponibles, le logiciel doit orchestrer lacommunication et assurer la synchronisation lors de l’exécution du code. La communication(transport des données entre les différents processeurs) est gérée de façon transparente par lematériel ou explicitement par le logiciel.Les modèles qui représentent les algorithmes de façon structurée et formelle mettent enévidence leur parallélisme inhérent. Le déploiement des logiciels représentés par ces modèlesnécessite de spécifier placement (sur quel processeur s’exécute une certaine tâche) et l’ordonnancement(dans quel ordre sont exécutées les tâches). Le placement et l’ordonnancement sontdes problèmes combinatoires difficile avec un nombre exponentiel de solutions. En outre, lessolutions ont différents coûts qui doivent être optimisés : la consommation de mémoire, letemps d’exécution, les ressources utilisées, etc. C’est un problème d’optimisation multi-critères.La solution à ce problème est ce qu’on appelle un ensemble Pareto-optimal nécessitant desalgorithmes spéciaux pour l’approximer.Nous ciblons une classe d’applications, appelées applications de streaming, qui traitentun flux continu de données. Ces applications qui appliquent un calcul similaire sur différentséléments de données successifs, peuvent être commodément exprimées par une classe de modèlesappelés modèles de flux de données. Le problème du placement et de l’ordonnancementest codé sous forme de contraintes logiques et résolu par un solveur Satisfaisabilité ModuloThéories (SMT). Les solveurs SMT résolvent le problème en combinant des techniques derecherche et de la propagation de contraintes afin d’attribuer des valeurs aux variables duproblème satisfaisant les contraintes de coût données.Dans les applications de flux de données, l’espace de conception explose avec l’augmentationdu nombre de tâches et de processeurs. Dans cette thèse, nous nous attaquons à ceproblème par l’introduction des techniques de réduction de symétrie et démontrons que larupture de symétrie accélère la recherche dans un solveur SMT, permettant ainsi l’augmentationde la taille du problème qui peut être résolu. Notre algorithme d’exploration de l’espacede conception approxime le front de Pareto du problème et produit des solutions pour différentscompromis de coûts. De plus, nous étendons le problème d’ordonnancement pour lesplate-formes "many-core" qui sont une catégorie de plate-forme multi coeurs où les unités sontconnectés par un réseau sur puce (NoC). Nous fournissons un flot de conception qui réalise leplacement des applications sur de telles plate-formes et insert automatiquement des élémentssupplémentaires pour modéliser la communication à l’aide de mémoires de taille bornée. Nousprésentons des résultats expérimentaux obtenus sur deux plate-formes existantes : la machineKalray à 256 processeurs et les Tilera TILE-64. / In order to achieve performance gains, computers have evolved to multi-core and many-core platforms abounding with multiple processor cores. However the problem of finding efficient ways to execute parallel software on them is hard. With a large number of processor cores available, the software must orchestrate the communication, synchronization along with the code execution. Communication corresponds to the transport of data between different processors, handled transparently by the hardware or explicitly by the software.Models which represent the algorithms in a structured and formal way expose the available parallelism. Deployment of the software algorithms represented by such models needs a specification of which processor to execute the tasks on (mapping) and when to execute them (scheduling). Mapping and scheduling is a hard combinatorial problem with exponential number of solutions. In addition, the solutions have multiple costs that need to be optimized, such as memory consumption, time to execute, resources used etc. Such a problem with multiple costs is called a multi-criteria optimization problem. The solution to this problem is a set of incomparable solutions called Pareto solutions which need special algorithms to approximate them.We target a class of applications called streaming applications, which process a continuous stream of data. These applications apply similar computation on different data items, can be conveniently expressed by a class of models called dataflow models. We encode mapping and scheduling problem in form of logical constraints and present it to satisfiability modulo theory (SMT) solvers. SMT solvers, solve the encoded problem by using a combination of search techniques and constraint propagation to find an assignment to the problem variables satisfying the given cost constraints.In dataflow applications, the design space explodes with increased number of tasks and processors. In this thesis, we tackle this problem by introduction symmetry reduction techniques and demonstrate that symmetry breaking accelerates search in SMT solver, increasing the size of the problem that can be solved. Our design-space exploration algorithm approximates Pareto front of the problem and produces solutions with different cost trade-offs. Further we extend the scheduling problem to the many-core platforms which are a group of multi-core platforms connected by network-on-chip. We provide a design flow which performs mapping of the applications on such platforms and automatic insertion of additional elements to model the communication using bounded memory. We provide experimental results obtained on the 256-processor Kalray and the Tilera TILE-64 platforms.The multi-core processors have typically a small amount of memory close to the processor, generally insufficient for all application data to fit. We study a class of parallel applications having a regular data access pattern and large amount of data to be processed by a uniform computation. The data must be brought from main memory to local memory, processed and then the results written back to main memory, all in batches. Selecting the proper granularity of the data that is brought into local memory is an optimization problem. We formalize this problem and provide a way to determine the optimal transfer granularity depending on the characteristics of application and the hardware platform.In addition to the scheduling problems and local memory management, we study a part of the problem of runtime management of the applications. Applications in modern embedded systems can start and stop dynamically. In order to execute all the applications efficiently and to optimize global costs such as power consumption, execution time etc., the applications must be reconfigured dynamically at runtime. We present a predictable and composable (executing independently without affecting others) way of migrating tasks according to the reconfiguration decision.

Les solveurs SMT sont des outils dédiés à la vérification d'un ensemble de formules mathématiques, en général sans quantificateurs, utilisant un certain nombre de théories prédéfinies, telles que la congruence, l'arithmétique linéaire sur les entiers, les rationnels ou les réels, les tableaux de bits ou les tableaux. Ajouter une nouvelle théorie à un solveur SMT nécessite en général une connaissance assez profonde du fonctionnement interne du solveur, et, de ce fait, ne peut en général être exécutée que par ses développeurs. Pour de nombreuses théories, il est également possible de fournir une axiomatisation finie en logique du premier ordre. Toutefois, si les solveurs SMT sont généralement complets et efficaces sur des problèmes sans quantificateurs, ils deviennent imprévisibles en logique du premier ordre. Par conséquent, cette approche ne peut pas être utilisée pour fournir une procédure de décision pour ces théories. Dans cette thèse, nous proposons un cadre d'application permettant de résoudre ce problème en utilisant des déclencheurs. Les déclencheurs sont des annotations permettant de spécifier la forme des termes avec lesquels un quantificateur doit être instancié pour obtenir des instances utiles pour la preuve. Ces annotations sont utilisées par la majorité des solveurs SMT supportant les quantificateurs et font partie du format SMT-LIB v2. Dans notre cadre d'application, l'utilisateur fournit une axiomatisation en logique du premier ordre de sa théorie, ainsi qu'une démonstration de sa correction, de sa complétude et de sa terminaison, et obtient en retour un solveur correct, complet et qui termine pour sa théorie. Dans cette thèse, nous décrivons comment un solveur SMT peut être étendu à notre cadre nous basant sur l'algorithme DPLL modulo théories, utilisé traditionnellement pour modéliser ls solveurs SMT. Nous prouvons également que notre extension a bien les propriétés attendues. L'effort à fournir pour implémenter cette extension dans un solveur SMT existant ne doit être effectué qu'une fois et le mécanisme peut ensuite être utilisé sur de multiples théories axiomatisées. De plus, nous pensons que, en général, cette implémentation n'est pas plus compliquée que l'ajout d'une unique théorie au solveur. Nous avons fait ce travail pour le solveur SMT Alt-Ergo, nous en présentons certains détails dans la thèse. Pour valider l'utilisabilité de notre cadre d'application, nous avons prouvé la complétude et la terminaison de plusieurs axiomatizations, dont une pour les listes impératives doublement chaînée, une pour les ensembles applicatifs et une pour les vecteurs de Ada. Nous avons ensuite utilisé notre implémentation dans Alt-Ergo pour discuter de l’efficacité de notre système dans différents cas. / SMT solvers are efficient tools to decide the satisfiability of ground formulas, including a number of built-in theories such as congruence, linear arithmetic, arrays, and bit-vectors. Adding a theory to that list requires delving into the implementation details of a given SMT solver, and is done mainly by the developers of the solver itself. For many useful theories, one can alternatively provide a first-order axiomatization. However, in the presence of quantifiers, SMT solvers are incomplete and exhibit unpredictable behavior. Consequently, this approach can not provide us with a complete and terminating treatment of the theory of interest. In this thesis, we propose a framework to solve this problem, based on the notion of instantiation patterns, also known as triggers. Triggers are annotations that suggest instances which are more likely to be useful in proof search. They are implemented in all SMT solvers that handle first-order logic and are included in the SMT-LIB format. In our framework, the user provides a theory axiomatization with triggers, along with a proof of completeness and termination properties of this axiomatization, and obtains a sound, complete, and terminating solver for her theory in return. We describe and prove a corresponding extension of the traditional Abstract DPLL Modulo Theory framework. Implementing this mechanism in a given SMT solver requires a one-time development effort. We believe that this effort is not greater than that of adding a single decision procedure to the same SMT solver. We have implemented the proposed extension in the Alt-Ergo prover and we discuss some implementation details in the thesis. To show that our framework can handle complex theories, we prove completeness and termination of three axiomatization, one for doubly-linked lists, one for applicative sets, and one for Ada's vectors. Our tests show that, when the theory is heavily used, our approach results in a better performance of the solver on goals that stem from the verification of programs manipulating these data-structures.