Doctor of Philosophy / Department of Computing and Information Sciences / David A. Schmidt / We are interested in modular static analysis to analyze softwares automatically. We focus on programs with data structures, and in particular, programs with pointers. The final goal is to find errors in a program (problems of dereferencing, aliasing, etc) or to prove that a program is correct (regarding those problems) in an automatic way. Isthiaq, Pym, O'Hearn and Reynolds have recently developed separation logics, which are Hoare logics with assertions and predicates language that allow to prove the correctness of programs that manipulate pointers. The semantics of the logic's triples ({P}C{P'}) is defined by predicate transformers in the style of weakest preconditions. We expressed and proved the correctness of those weakest preconditions (wlp) and strongest postconditions (sp), in particular in the case of while-loops. The advance from the existing work is that wlp and sp are defined for any formula, while previously existing rules had syntactic restrictions. We added fixpoints to the logic as well as a postponed substitution which then allow to express recursive formula. We expressed wlp and sp in the extended logic and proved their correctness. The postponed substitution is directly useful to express recursive formula. For example, [equations removed, still appears in abstract] describes the set of memory where x points to a list of integers. Next, the goal was to use separation logic with fixpoints as an interface language for pointer analysis. That is, translating the domains of those analyses into formula of the logic (and conversely) and to prove their correctness. One might also use the translations to prove the correctness of the pointer analysis itself. We illustrate this approach with a simple pointers-partitioning analysis. We translate the logic formula into an abstract language we designed which allows us to describe the type of values registered in the memory (nil, integer, booleans, pointers to pairs of some types, etc.) as well as the aliasing and non-aliasing relations between variables and locations in the memory. The main contribution is the definition of the abstract language and its semantics in a concrete domain which is the same as the one for the semantics of formula. In particular, the semantics of the auxiliary variables, which is usually a question of implementation, is explicit in our language and its semantics. The abstract language is a partially reduced product of several subdomains and can be parametrised with existing numerical domains. We created a subdomain which is a tabular data structure to cope with the imprecision from not having sets of graphs. We expressed and proved the translations of formula into this abstract language.

There was a culture debate during 2019 in the Swedish newspaper, Dagens Nyheter, about what kind of literature children should take part of. We took an interest in the debate and wanted to study teachers’ approach to literature in preschools. We found a problem whether the literature should have an educational purpose for the unready child or as stated in the curriculum that children should be viewed as owners of their agency. From the social constructivism concepts of being and becoming, this paper aims to investigate educators’ selection processes of literature and approaches to reading in preschools, and to conceptualise how this type of literary content can be used to teach children civic pointers.In this qualitative study we interviewed people who were working in preschools. We included teachers from different workplaces, assignments and age groups. The results of this study show that the preschools not exclusively have a being or becoming approach to literature, but that the approaches actually coexist in the everyday work. That is, the children are sometimes considered competent enough to handle rather complex ethical problems in the literature, but in other situations the preschool teachers change the stories to for example not scare the children. The literature had distinct purposes in the preschools, for example to help the children reflect over different life situations and teach them how to properly handle such situations. A common strategy the teachers used to accomplish this was to change the stories or characters of the literature they used. In conclusion, this study shows that the selection processes of literature in preschools aim for children to recognise themselves in the literature and it should be developing and challenging for the children. Furthermore, teachers make conscious choices when reading to the children. We also found that teaching civic pointers to children is a constant process in early education. This study can help teachers to be aware of how literature is selected in preschools, that different approaches to literature might form children and that it is an ongoing process.

The fast and furious pace of change in computing technology has become an article of faith for many. The reliability of computer-based systems cru- cially depends on the correctness of its computing. Can man, who created the computer, be capable of preventing machine-made misfortune? The theory of static analysis strives to achieve this ambition. The analysis of numerical properties of programs has been an essential research topic for static analysis. These kinds of properties are commonly modeled and handled by the concept of numerical abstract domains. Unfor- tunately, lifting these domains to heap-manipulating programs is not obvious. On the other hand, points-to analyses have been intensively studied to an- alyze pointer behaviors and some scale to very large programs but without inferring any numerical properties. We propose a framework based on the theory of abstract interpretation that is able to combine existing numerical domains and points-to analyses in a modular way. The static numerical anal- ysis is prototyped using the SOOT framework for pointer analyses and the PPL library for numerical domains. The implementation is able to analyze large Java program within several minutes. The second part of this thesis consists of a theoretical study of the com- bination of the points-to analysis with another pointer analysis providing information called must-alias. Two pointer variables must alias at some pro- gram control point if they hold equal reference whenever the control point is reached. We have developed an algorithm of quadruple complexity that sharpens points-to analysis using must-alias information. The algorithm is proved correct following a semantics-based formalization and the concept of bisimulation borrowed from the game theory, model checking etc.

Les travaux décrits dans cette thèse portent sur le problème de vérification des systèmes avec espaces d’états infinis, et, en particulier, avec des structures de données chaînées. Plusieurs approches ont émergé, sans donner des solutions convenables et robustes, qui pourrait faire face aux situations rencontrées dans la pratique. Nos travaux proposent une approche nouvelle, qui combine les avantages de deux approches très prometteuses: la représentation symbolique a base d’automates d’arbre, et la logique de séparation. On présente également plusieurs améliorations concernant l’implementation de différentes opérations sur les automates d’arbre, requises pour le succès pratique de notre méthode. En particulier, on propose un algorithme optimise pour le calcul des simulations sur les systèmes de transitions étiquettes, qui se traduit dans un algorithme efficace pour le calcul des simulations sur les automates d’arbre. En outre, on présente un nouvel algorithme pour le problème d’inclusion sur les automates d’arbre. Un nombre important d’expérimentes montre que cet algorithme est plus efficace que certaines des méthodes existantes. / This work addresses verification of infinite-state systems, more specifically, verification of programs manipulating complex dynamic linked data structures. Many different approaches emerged to date, but none of them provides a sufficiently robust solution which would succeed in all possible scenarios appearing in practice. Therefore, in this work, we propose a new approach which aims at improving the current state of the art in several dimensions. Our approach is based on using tree automata, but it is also partially inspired by some ideas taken from the methods based on separation logic. Apart from that, we also present multiple advancements within the implementation of various tree automata operations, crucial for our verification method to succeed in practice. Namely, we provide an optimised algorithm for computing simulations over labelled transition systems which then translates into more efficient computation of simulations over tree automata. We also give a new algorithm for checking inclusion over tree automata, and we provide experimental evaluation demonstrating that the new algorithm outperforms other existing approaches.

Made available in DSpace on 2014-12-17T14:53:17Z (GMT). No. of bitstreams: 1 FernandoPSO.pdf: 492161 bytes, checksum: 7d1ef5318566c9b041e602617b1650f7 (MD5) Previous issue date: 2006-05-19 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / At present, the network re appear like alternatives of find forms in arrangements inter-organizational that offer his members better opportunities of modernizes technological, insertion in the market, managerial and at the same time permit the exchange of experiences, information and knowledge for fortify and compete of equal for equal, permitting brighten up the harmful effects of the compete wild. A threat that can be minimized by the organization in net and the use of other forms interorganizational and strategic alliances. Therefore the demonstrates the context of the competitive cooperation in network, seeking criteria of analysis of that phenomenon organizational, on the basis of a study of case of the net ITCPs and in the literature researched, aimed with that criterion and indicator for creation of a model of evaluation in the future (Factor Net) that be prominent for the drawing of those forms organizational you maintained, supportive, competitive and cooperative / Atualmente, as redes re-aparecem como alternativas de encontrar formas em arranjos interorganizacionais que ofere?am aos seus integrantes melhores oportunidades de moderniza??o tecnol?gica, inser??o no mercado, gerencial e ao mesmo tempo permitam a troca de experi?ncias, informa??es e conhecimentos para fortalecer e competir de igual para igual, permitindo amenizar os efeitos danosos da concorr?ncia selvagem. Uma amea?a que pode ser minimizada pela organiza??o em rede pelo uso de outras formas interorganizacionais e alian?as estrat?gicas. Portanto, o trabalho demonstra o contexto da coopera??o competitiva em redes, buscando crit?rios de an?lise desse fen?meno organizacional, com base num estudo de caso da rede ITCPs e na literatura pesquisada, apontando com isso crit?rios e indicadores para a cria??o de um modelo de avalia??o, no futuro (Fator Rede), que seja relevante para o desenho dessas formas organizacionais sustent?veis, solid?rias, competitivas e cooperativas

Hoare and He's Unifying Theories of Programming (UTP) provides a rich model of programs as relational predicates. This theory is intended to provide a single framework in which any programming paradigms, languages, and features, can be modelled, compared and contrasted. The UTP already has models for several programming formalisms, such as imperative programming, higher-order programming (e.g. programing with procedures), several styles of concurrent programming (or reactive systems), class-based object-orientation, and transaction processing. We believe that the UTP ought to be able to represent all significant computer programming language formalisms, in order for it to be considered a unifying theory. One gap in the UTP work is that of object-based object-orientation, such as that presented in Abadi and Cardelli's untyped object calculi (sigma-calculi). These sigma-calculi provide a prominent formalism of object-based object-oriented (OO) programs, which models programs as objects. We address this gap within this dissertation by presenting an embedding of an Abadi--Cardelli-style object calculus in the UTP. More formally, the thesis that his dissertation argues is that it is possible to provide an object-based object rientation to the UTP, with value- and reference-based objects, and a fully abstract model of references. We have made three contributions to our area of study: first, to extend the UTP with a notion of object-based object orientation, in contrast with the existing class-based models; second, to provide an alternative model of pointers (references) for the UTP that supports both value-based compound values (e.g. objects) and references (pointers), in contrast to existing UTP models with pointers that have reference-based compound values; and third, to model an Abadi-Cardelli notion of an object in the UTP, and thus demonstrate that it can unify this style of object formalism.

Si la production de logiciel fiable est depuis longtemps la préoccupation d'ingénieurs, elle devient à ce jour une branche de sujets de recherche riche en applications, dont l'analyse statique. Ce travail a porté sur l'analyse statique de programmes et, plus précisément, sur l'analyse des propriétés numériques. Ces analyses sont traditionnellement basées sur le concept de domaine abstrait. Le problème est que, ce n'est pas évident d'étendre ces domaines dans le contexte de programmes avec pointeurs. Nous avons proposé une approche qui sait systématiquement combiner ces domaines avec l'information de l'analyse de points-to (une sorte d'analyse de pointeurs). L'approche est formalisée en théorie de l'interprétation abstraite, prouvée correct et prototypée avec une modular implémentation qui sait inférer des propriétés numériques des programmes de millions de lignes de codes. La deuxième partie de la thèse vise à améliorer la précision de l'analyse points-to. Nous avons découvert que l'analyse de must-alias (qui analyse si deux variables sont nécessairement égaux) peut servir à raffiner l'analyse points-to. Nous avons formalisé cette combinaison en s'appuyant sur la notion de bisimulation, bien connue en vérification de modèle ou théorie de jeu... Un algorithme de complexité quadruple est proposé et prouvé correct. / The fast and furious pace of change in computing technology has become an article of faith for many. The reliability of computer-based systems cru- cially depends on the correctness of its computing. Can man, who created the computer, be capable of preventing machine-made misfortune? The theory of static analysis strives to achieve this ambition. The analysis of numerical properties of programs has been an essential research topic for static analysis. These kinds of properties are commonly modeled and handled by the concept of numerical abstract domains. Unfor- tunately, lifting these domains to heap-manipulating programs is not obvious. On the other hand, points-to analyses have been intensively studied to an- alyze pointer behaviors and some scale to very large programs but without inferring any numerical properties. We propose a framework based on the theory of abstract interpretation that is able to combine existing numerical domains and points-to analyses in a modular way. The static numerical anal- ysis is prototyped using the SOOT framework for pointer analyses and the PPL library for numerical domains. The implementation is able to analyze large Java program within several minutes. The second part of this thesis consists of a theoretical study of the com- bination of the points-to analysis with another pointer analysis providing information called must-alias. Two pointer variables must alias at some pro- gram control point if they hold equal reference whenever the control point is reached. We have developed an algorithm of quadruple complexity that sharpens points-to analysis using must-alias information. The algorithm is proved correct following a semantics-based formalization and the concept of bisimulation borrowed from the game theory, model checking etc.

Conselho Nacional de Desenvolvimento CientÃfico e TecnolÃgico / Este trabalho se propÃs a avaliar as alteraÃÃes nas atividades microbiana, quÃmica e fÃsica em solo sob sistemas agrÃcolas anuais e perenes na regiÃo da Chapada do Apodi - CE. Procurou-se testar a hipÃtese de que o uso agrÃcola de Ãreas sob sistemas anuais e perenes causam alteraÃÃes ambientais que influenciam a biomassa e a atividade microbiana do solo, reduzindo-a em relaÃÃo a Ãreas sob vegetaÃÃo natural. Foram selecionadas duas Ãreas com respectivas testemunhas (vegetaÃÃo natural); a primeira sob cultivo de bananeiras (Fazenda Frutacor) e a outra sob cultivo de rotaÃÃo milho e soja (Fazenda Faedo). Coletaram-se amostras compostas de solo em trÃs profundidades (0-5, 5-15 e 15-25 cm) com quatro repetiÃÃes. Nas amostras coletadas foram realizadas anÃlises fÃsicas, quÃmicas e microbiolÃgicas. Fisicamente, observou-se uma elevaÃÃo no teor de argila, com o aumento da profundidade na Ãrea cultivada com banana e na mata natural pivot. Em relaÃÃo aos atributos quÃmicos do solo, os riscos potenciais de salinidade e de saturaÃÃo por sÃdio aparentemente sÃo desprezÃveis. As prÃticas de manejo reduziram o N e o carbono orgÃnico total nos solos das Ãreas sob cultivo. Quanto à microbiologia dos solos, o carbono da biomassa microbiana e a populaÃÃo de fungos micorrÃzicos arbusculares foram mais elevados na profundidade de 0-5cm do solo. A respiraÃÃo basal do solo mostrou que os solos das Ãreas avaliadas tÃm baixa atividade microbiana quando comparados a solos do Cerrado. A atividade e produÃÃo da arilsulfatase e da fosfatase Ãcida foram estimuladas possivelmente, pela competiÃÃo dos Ãnions H2PO4 - e SO4 - pelos mesmos sÃtios de adsorÃÃo nos colÃides do solo, nas Ãreas de banana e rotaÃÃo milho e soja. A maior atividade da enzima β-glucosidase ocorreu nas Ãreas cultivadas, influenciada pela quantidade e qualidade do resÃduo vegetal retornado ao solo. / This work had the proposed to evaluate the alterations in the microbial activities, chemistry and physics in soil under annual and perennial agricultural systems in the area of the Chapada do Apodi - CE. It tried to test the hypothesis that the agricultural use of areas under annual and perennial systems causes environmental alterations that they influence the biomass and the microbial activity of the soil, reducing it in relation to areas under natural vegetation. Two areas were selected with respective witness (natural vegetation); the first under cultivation of banana trees (Fazenda Frutacor) and the other under cultivation of rotation corn and soy (Fazenda Faedo). Samples composed of soil were collected in three depths (0-5, 5-15 and 15-25 cm) with four repetitions. In the collected samples physical analyses, chemistries and microbiological were accomplished. Physically, an elevation was observed in the clay text, with the increase of the depth in the area cultivated with banana and in the forest natural pivot. In relation to the chemical attributes of the soil, the potential risks of salinity and of saturation for sodium seemingly are worthless. The handling practices reduced N and the total organic carbon in the soils of the areas under cultivation. With relationship to the microbiology of the soils, the carbon of the microbial biomass and the population of arbuscular mycorrhizal fungi were more elevated in the depth of 0-5cm of the soil. The basal breathing of the soil identified that the soils of the appraised areas have microbial when compared low activity the soils of the Cerrado. The activity and production of the arylsulphatase and of the acid phosphatase were stimulated possibly, for the competition of the anions H2PO4- and SO4- for the same ranches of adsorption in the coloides of the soil, in the banana areas and rotation corn and soy. The largest activity of the enzyme β-glucosidase happened in the cultivated areas, influenced by the amount and quality of the vegetable residue come back to the soil.

CoordenaÃÃo de AperfeiÃoamento de Pessoal de NÃvel Superior / Neste trabalho, analisam-se os impactos da Proposta de AdesÃo da UFC ao REUNI no atendimento do Restaurante UniversitÃrio, decorrentes do grande aumento na demanda, sob o prisma do planejamento e da gestÃo estratÃgica, focando-se nas aÃÃes realizadas no perÃodo de 2003 a 2008. Para tanto, utilizam-se como suporte teÃrico-empÃrico os postulados da AdministraÃÃo EstratÃgica e da Escola de Aprendizado, tendo como referencial o cenÃrio atual e futuro e o diagnÃstico estratÃgico formulado com base na anÃlise SWOT. Foram utilizados os mÃtodos de pesquisa bibliogrÃfica, documental e pesquisa-aÃÃo. O estudo mostra que a expansÃo prevista de 3.000 para 6.000 refeiÃÃes/dia afetarà a qualidade dos serviÃos e do atendimento aos usuÃrios em funÃÃo das limitaÃÃes atuais de infra-estrutura fÃsica, de equipamentos, de pessoal qualificado e, sobretudo, da necessidade de implantaÃÃo de um modelo da gestÃo focada em resultados. Para esse novo cenÃrio, sugere-se um Plano EstratÃgico para o perÃodo 2009-2020, um Plano TÃtico 2009-2012, uma matriz de indicadores de desempenho focada no mÃtodo do Balanced scorecard, alÃm das diretrizes do modelo da gestÃo orientado para resultados e aderentes Ãs peculiaridades do Restaurante UniversitÃrio da UFC. As propostas de aÃÃo e do modelo de gerenciamento contidos nos planos estratÃgicos, quando adotadas, darÃo ao RU condiÃÃes objetivas de infra-estrutura operacional, suporte de pessoal e excelÃncia da gestÃo para assegurar e atà aumentar a aprovaÃÃo da qualidade dos serviÃos que hoje à 60,3% para os atributos Bom e Ãtimo. / The present work focuses on the analysis of the impacts of the Federal University of Cearà affiliation proposal to the Reuni, concerning attendance to the University Restaurant on a result of the increasing demand, in the perspective of strategic planning and management, based on the actions carried out from 2003 to 2008. For such end, the postulates of Strategic administration and of Learning School have been adopted, having as a reference the present and future scenario and the strategic diagnosis based on the SWOT analysis. The present research (study) adopted the bibliographical, documental and action-research methods. The research shows that the foreseen expansion in the number of meals per day, from 3000 to 6000, will have an impact on the quality of the services delivered to the users, due to the present limitations in infra-structure, equipments, qualified personnel, and, above all, the need for implementing a pattern of management aimed at results. For this new scenario the following measures have been suggested, including a Strategic Plan for 2009-2020, a Tatic Plan for 2009-2012, a performance marker matrix focused on the Balanced scorecard method, besides management pattern guidelines, oriented towards results and users in the specific context of the University restaurant. The actions and management patterns proposed in the strategic plans, when adopted , will allow the University restaurant to have operational infra-structure, staff support and management excellence to assure and contribute to the approval in the service quality from the present percentage of 60.3% aiming to reach the concepts of good and excellent.

Tato práce se zabývá verifikací nekonečně stavových systémů, konkrétně, verifikací programů využívajích složité dynamicky propojované datové struktury. V minulosti se k řešení tohoto problému objevilo mnoho různých přístupů, avšak žádný z nich doposud nebyl natolik robustní, aby fungoval ve všech případech, se kterými se lze v praxi setkat. Ve snaze poskytnout vyšší úroveň automatizace a současně umožnit verifikaci programů se složitějšími datovými strukturami v této práci navrhujeme nový přístup, který je založen zejména na použití stromových automatů, ale je také částečně inspirován některými myšlenkami, které jsou převzaty z metod založených na separační logice. Mimo to také představujeme několik vylepšení v oblasti implementace operací nad stromovými automaty, které jsou klíčové pro praktickou využitelnost navrhované verifikační metody. Konkrétně uvádíme optimalizovaný algoritmus pro výpočet simulací pro přechodový systém s návěštími, pomocí kterého lze efektivněji počítat simulace pro stromové automaty. Dále uvádíme nový algoritmus pro testování inkluze stromových automatů společně s experimenty, které ukazují, že tento algoritmus překonává jiné existující přístupy.