Dissertations / Theses on the topic 'Separation logic'
To see the other types of publications on this topic, follow the link: Separation logic.
Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles
Consult the top 50 dissertations / theses for your research on the topic 'Separation logic.'
Next to every source in the list of references, there is an 'Add to bibliography' button. Press on it, and we will generate automatically the bibliographic reference to the chosen work in the citation style you need: APA, MLA, Harvard, Chicago, Vancouver, etc.
You can also download the full text of the academic publication as pdf and read online its abstract whenever available in the metadata.
Browse dissertations / theses on a wide variety of disciplines and organise your bibliography correctly.
1
Wright, Adam. "Structural separation logic." Thesis, Imperial College London, 2013. http://hdl.handle.net/10044/1/17838.
Full textAbstract:
This thesis presents structural separation logic, a novel program reasoning approach for software that manipulates both standard heaps and structured data such as lists and trees. Structural separation logic builds upon existing work in both separation logic and context logic. It considers data abstractly, much as it is exposed by library interfaces, ignoring implementation details. We provide a programming language that works over structural heaps, which are similar to standard heaps but allow data to be stored in an abstract form. We introduce abstract heaps, which extend structural heaps to enable local reasoning about abstract data. Such data can be split up with structural addresses. Structural addresses allow sub-data (e.g. a sub-tree within a tree) to be abstractly allocated, promoting the sub-data to an abstract heap cell. This cell can be analysed in isolation, then re-joined with the original data. We show how the tight footprints this allows can be refined further with promises, which enable abstract heap cells to retain information about the context from which they were allocated. We prove that our approach is sound with respect to a standard Hoare logic. We study two large examples. Firstly, we present an axiomatic semantics for the Docu- ment Object Model in structural separation logic. We demonstrate how structural separa- tion logic allows abstract reasoning about the DOM tree using tighter footprints than were possible in previous work. Secondly, we give a novel presentation of the POSIX file system library. We identify a subset of the large POSIX standard that focuses on the file system, including commands that manipulate both the file heap and the directory structure. Axioms for this system are given using structural separation logic. As file system resources are typically identified by paths, we use promises to give tight footprints to commands, so that that they do not require all the resource needed to explain paths being used. We demonstrate our reasoning using a software installer example.
2
Coughlin, Devin. "Type-Intertwined Separation Logic." Thesis, University of Colorado at Boulder, 2015. http://pqdtopen.proquest.com/#viewpdf?dispub=3704668.
Full textAbstract:
Static program analysis can improve programmer productivity and software reliability by definitively ruling out entire classes of programmer mistakes. For mainstream imperative languages such as C, C++, and Java, static analysis about the heap---memory that is dynamically allocated at run time---is particularly challenging because heap memory acts as global, mutable state. This dissertation describes how to soundly combine two static analyses that each take vastly different approaches to reasoning about the heap: type systems and separation logic. Traditional type systems take an alias-agnostic, global view of the heap that affords both fast verification and light-weight annotation of invariants holding over the entire program. Separation logic, in contrast, provides an alias-aware, local view of the heap in which invariants can vary at each program point. In this work, I show how type systems and separation logic can be safely and efficiently combined. The result is type-intertwined separation logic, an analysis that applies traditional type-based reasoning to some regions of the program and separation logic to others---converting between analysis representations at region boundaries---and summarizes some portions of the heap with coarse type invariants and others with precise separation logic invariants. The key challenge that this dissertation addresses is the communication and preservation of heap invariants between analyses. I tackle this challenge with two core contributions. The first is type-consistent summarization and materialization, which enables type-intertwined separation logic to both leverage and selectively violate the global type invariant. This mechanism allows the analysis to efficiently and precisely verify invariants that hold almost everywhere. Second, I describe gated separating conjunction, a non-commutative strengthening of standard separating conjunction that expresses local dis-pointing relationships between sub-heaps. Gated separation enables local heap reasoning by permitting the separation logic to frame out portions of memory and prevent the type system from interfering with its contents---an operation that would be unsound in type-intertwined analysis with only standard separating conjunction. With these two contributions, type-intertwined separation logic combines the benefits of both type-like global reasoning and separation-logic-style local reasoning in a single analysis.
3
Sims, Elodie-Jane. "Pointer analysis and separation logic." Diss., Manhattan, Kan. : Kansas State University, 2007. http://hdl.handle.net/2097/506.
Full text
4
Raza, Mohammad. "Resource Reasoning and Labelled Separation Logic." Thesis, Imperial College London, 2010. http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.523755.
Full text
5
Tuerk, Thomas. "A separation logic framework for HOL." Thesis, University of Cambridge, 2011. http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.609585.
Full text
6
Winterstein, Felix. "Separation logic for high-level synthesis." Thesis, Imperial College London, 2016. http://hdl.handle.net/10044/1/33371.
Full textAbstract:
High-level synthesis (HLS) promises a significant shortening of the digital hardware design cycle by raising the abstraction level of the design entry to high-level languages such as C/C++. However, applications using dynamic, pointer-based data structures remain difficult to implement well, yet such constructs are widely used in software. Automated optimisations that leverage the memory bandwidth of dedicated hardware implementations by distributing the application data over separate on-chip memories and parallelise the implementation are often ineffective in the presence of dynamic data structures, due to the lack of an automated analysis that disambiguates pointer-based memory accesses. This thesis takes a step towards closing this gap. We explore recent advances in separation logic, a rigorous mathematical framework that enables formal reasoning about the memory access of heap-manipulating programs. We develop a static analysis that automatically splits heap-allocated data structures into provably disjoint regions. Our algorithm focuses on dynamic data structures accessed in loops and is accompanied by automated source-to-source transformations which enable loop parallelisation and physical memory partitioning by off-the-shelf HLS tools. We then extend the scope of our technique to pointer-based memory-intensive implementations that require access to an off-chip memory. The extended HLS design aid generates parallel on-chip multi-cache architectures. It uses the disjointness property of memory accesses to support non-overlapping memory regions by private caches. It also identifies regions which are shared after parallelisation and which are supported by parallel caches with a coherency mechanism and synchronisation, resulting in automatically specialised memory systems. We show up to 15x acceleration from heap partitioning, parallelisation and the insertion of the custom cache system in demonstrably practical applications.
7
Brochenin, Rémi. "Separation logic : expressiveness, complexity, temporal extension." Phd thesis, École normale supérieure de Cachan - ENS Cachan, 2013. http://tel.archives-ouvertes.fr/tel-00956587.
Full textAbstract:
This thesis studies logics which express properties on programs. These logics were originally intended for the formal verification of programs with pointers. Overall, no automated verification method will be proved tractable here- rather, we give a new insight on separation logic. The complexity and decidability of some essential fragments of this logic for Hoare triples were not known before this work. Also, its combination with some other verification methods was little studied. Firstly, in this work we isolate the operator of separation logic which makes it undecidable. We describe the expressive power of this logic, comparing it to second-order logics. Secondly, we try to extend decidable subsets of separation logic with a temporal logic, and with the ability to describe data. This allows us to give boundaries to the use of separation logic. In particular, we give boundaries to the creation of decidable logics using this logic combined with a temporal logic or with the ability to describe data.
8
Long, Byron L. "Validity in a variant of separation logic." [Bloomington, Ind.] : Indiana University, 2009. http://gateway.proquest.com/openurl?url_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:dissertation&res_dat=xri:pqdiss&rft_dat=xri:pqdiss:3378369.
Full textAbstract:
Thesis (Ph.D.)--Indiana University, Dept. of Computer Science, 2009.Title from PDF t.p. (viewed on Jul 9, 2010). Source: Dissertation Abstracts International, Volume: 70-10, Section: B, page: 6348. Adviser: Daniel Leivant.
9
Hussain, Akbar. "Session types, concurrent separation logic & algebra." Thesis, Queen Mary, University of London, 2013. http://qmro.qmul.ac.uk/xmlui/handle/123456789/8503.
Full textAbstract:
This dissertion explores the relation between two formalisms and one algebraic framework for concurrency. Session Types and Concurrent Separation Logic are formalisms that support independent reasoning about concurrent processes, and our motivating question is whether their modularity springs from the same source despite the distance between their models. We first translate a small language we call Baby Session Types (BST), into a ‘basic’ version of Concurrent Separation Logic (BCSL), and we show that the translation is sound. We then describe a model for Separation Logic (SL) based on Actions, which exhibits some of the structure of a Concurrent Kleene Algebra, an algebra where operators for parallel and sequential composition are linked by a version of the exchange law from category theory. The model connects the algebraic notions to locality concepts that underlie Separation Logic. We then move on to provide a more general construction of an algebra model of BCSL, which can be built from (Baby) Session Types. Thus, we end up with a model that brings together concepts from all of Session Types, Separation Logic, and Concurrent Kleene Algebra. Thus, the model links diverse models of concurrency. In addition to this it suggests alterations of the algebraic axioms as well as the foundational models underlying Separation Logic. It is hoped that, apart from these specific results, this dissertation can in some modest way contribute to unification in concurrency theory, a theory (or theories) based presently on diverse models.
10
Krishnaswami, Neelakantan R. "Verifying Higher-Order Imperative Programs with Higher-Order Separation Logic." Research Showcase @ CMU, 2012. http://repository.cmu.edu/dissertations/164.
Full textAbstract:
In this thesis I show is that it is possible to give modular correctness proofs of interesting higher-order imperative programs using higher-order separation logic.
To do this, I develop a model higher-order imperative programming language, and develop a program logic for it. I demonstrate the power of my program logic by verifying a series of examples. This includes both realistic patterns of higher-order imperative programming such as the subject-observer pattern, as well as examples demonstrating the use of higher-order logic to reason modularly about highly aliased data structures such as the union-find disjoint set algorithm.
11
Dang, Han Hing [Verfasser], and Bernhard [Akademischer Betreuer] Möller. "Algebraic Calculi for Separation Logic / Han Hing Dang. Betreuer: Bernhard Möller." Augsburg : Universität Augsburg, 2015. http://d-nb.info/1077704933/34.
Full text
12
Hurlin, Clément. "Specification and verification of multithreaded object-oriented programs with separation logic." Nice, 2009. http://www.theses.fr/2009NICE4064.
Full textAbstract:
First, we develop verification rules in separation logic for primitives concerning multithreading : the primitives fork and join that control how threads start and how threads wait, and the primitive for reentrant locks (locks that can be acquired and released more than once) that are used in Java. Second, we develop three analyses that use separation logic. The first analysis permits to specify sequences of method calls and to verify that they are correct w. R. T. Method contracts. The second analysis presents a fast algorithm to disprove entailment between separation logic formulae. The third analysis shows how to parallelize and optimize programs by rewriting their proofs. This thesis develops a verification system in separation logic for multithreaded Java programs. In addition, this thesis shows three new analyses based on separation logic. Separation logic is a variant of linear logic that did a recent breakthrough in program verification. In the literature, separation logic has been applied to simple while programs, while programs with parallelism, and sequential object oriented programs. We complete these works by adapting separation logic to multithreaded object-oriented programs à la Java. To pursue this goal, we develop new verification rules for Java's primitives for multithreading. The basis of our work consists of a model language that we use throughout the thesis. All our formalisation is based on this model language. First, we propose new verification rules for fork and join. Fork starts a new thread while join waits until the receiver thread terminates. Fork and join are used in many mainstream languages including Java, C++, C#, and python. Then, we describe verification rules for reentrant locks i. E. Java's locks. Reentrant locks - as opposed to Posix locks - can be acquired multiple times (and released accordingly). This property eases the programmer's task, but it makes verification harder. Second, we present three new analyses based on separation logic. The first analysis completes Cheon et al. 's work on sequences of allowed method calls (i. E. Protocols). We extend this work to multithreaded programs and propose a technique to verify that method contracts comply with class protocols. The second analysis permits to show that a separation logic formula does not entail another formula. This algorithm works as follows: given two formulas A and B, the size of A and B's models is approximated; then if the sizes of models are incompatible, the algorithm concludes that A does not entail B. This algorithm is useful in program verifiers, because they have to decide entailment often. The third analysis shows how to parallelize and optimize programs by looking at their proofs in separation logic. This algorithm is implemented in a tool called éterlou. Finally, we conclude and discuss possible future workEn premier lieu, nous développons des règles de vérification en logique de séparation pour les primitives en rapport avec le parallélisme : les primitives fork et join qui contrôlent le départ et l’attente des processus, et les verrous rééentrants qui sont utilisés en Java. En second lieu, nous développons trois analyses utilisant la logique de séparation. La première analyse permet de spécifier les séquences d’appels de méthodes autorisées et de vérifier leur cohérence. La deuxième analyse permet de montrer qu’une formula de logique de séparation n’en implique pas une autre. La troisième analyse montre comment paralléliser et optimiser des programmes en réécrivant leurs preuves. Cette thèse développe un système de vérification en logique de séparation pour des programmes orientés-objets parallèles et de nouvelles analyses utilisant la logique de séparation. La logique de séparation est une variante de la logique linéaire qui connaît un récent succès pour la vérification de programmes. Dans la littérature, la logique de séparation a été appliquée à des programmes while simples, des programmes while parallèles, et des programmes objets séquentiels. Dans cette thèse nous continuons ces travaux en adaptant la logique de séparation aux programmes objets parallèles similaires à Java. Dans ce but, nous développons de nouvelles règles de vérification pour les primitives de Java concernant le parallélisme. Pour se faire, nous élaborons un langage modèle similaire à Java qui sert de base à la première partie de la thèse. Ensuite, nous mettons en œuvre un système de vérification en logique de séparation pour les programmes écrits dans ce langage modèle. Dans la première partie de la thèse, nous proposons des règles de vérification pour les primitives fork et join. La primitive fork démarre un nouveau thread et la primitive join permet d'attendre la terminaison d'un thread. Ces primitives sont utilisées par un certain nombre de langages: Java, C++, python, et C#. Ensuite, nous décrivons des règles de vérification pour les verrous réentrants i. E. Les verrous utilisés en Java. Les verrous réentrants – contrairement aux verrous Posix – peuvent être acquis plusieurs fois. Cette propriété simplifie la tâche du programmeur mais complique la vérification. La suite de la thèse présente trois nouvelles analyses utilisant la logique de séparation. La première analyse continue le travail de Cheon et al. Sur les séquences d'appels de méthodes autorisées (aka protocoles). Nous étendons ces travaux aux programmes parallèles et inventons une technique afin de vérifier que les spécifications des méthodes d'une classe sont conformes au protocole de cette classe. La deuxième analyse propose un algorithme pour montrer qu'une formule de logique de séparation n'en implique pas une autre. Cet algorithme fonctionne de la manière suivante: étant donné deux formules A et B, la taille des modèles potentiels de A et B est calculée approximativement, puis; si les tailles obtenues sont incompatibles, l'algorithme conclut que A n'implique pas B. Cet algorithme est utile dans les vérificateurs de programmes car ceux-ci doivent souvent décider des implications. Enfin, la troisième analyse montre comment paralléliser et optimiser des programmes en observant leurs preuves en logique de séparation. Cet algorithme est mis en œuvre dans l'outil éterlou. Pour finir, nous concluons et proposons des pistes pour compléter les résultats de la présente thèse
13
Matheja, Christoph [Verfasser], Joost-Pieter [Akademischer Betreuer] Katoen, and Radu [Akademischer Betreuer] Iosif. "Automated reasoning and randomization in separation logic / Christoph Matheja ; Joost-Pieter Katoen, Radu Iosif." Aachen : Universitätsbibliothek der RWTH Aachen, 2020. http://d-nb.info/1216175748/34.
Full text
14
Mansutti, Alessio. "Reasoning with separation logics : complexity, expressive power, proof systems." Electronic Thesis or Diss., université Paris-Saclay, 2020. http://www.theses.fr/2020UPASG050.
Full textAbstract:
Cette thèse propose une étude approfondie de problèmes de décision classiques, tels que la satisfaisabilité et la validité pour des logiques de séparation, langages d'assertion bien connus développés pour la vérification de programmes avec structures dynamiques. La première partie de la thèse s'intéresse à la notion d'accessibilité pour les logiques de séparation. Notre motivation est double: d'une part, il s'agit de comprendre les frontières de la décidabilité de fragments de la logique de séparation du premier ordre connue pour être indécidable; d'autre part l'intention est de concevoir une logique de séparation aussi expressive que possible qui contienne des prédicats d'accessibilité, et dont le problème de satisfaisabilité soit décidable avec une complexité algorithmique relativement modeste (PSpace).Dans la seconde partie de la thèse, nous tirons profit des techniques développées dans la première partie pour définir une axiomatisation à la Hilbert de logiques de séparation et d'autres logiques spatiales. En particulier, nous définissons le premier calcul interne correct et complet pour la logique de séparation sans quantification. En utilisant la même approche, nous définissons une axiomatisation pour une logique modale enrichie d'un opérateur de composition issu d'une logique des ambients, formalisme logique dédié à la vérification de systèmes distribués. Les deux systèmes de preuves mettent en lumière des relations intéressantes entre les logiques de séparation et les logiques des ambients.Dans la troisième partie de la thèse, nous approfondissons encore davantage les relations entre les logiques de séparation et les logiques des ambients. Des similarités et des différences sont établies en termes de pouvoir d'expression et de complexité algorithmique, en comparant la conjonction séparante des logiques de séparation avec l'opérateur de composition des logiques des ambients. Afin de mener à bien nos comparaisons, nous nous plaçons dans une cadre uniforme issu de la logique modale, ce qui permet de partir d'une base commune pour étudier ces deux logiquesThis thesis proposes an in-depth study of classical decision problems, such as satisfiability and validity, for separation logics: well-known assertion languages developed to verify heap-manipulating programs. The first part of the thesis focus on the notion of reachability in separation logics. Our motivation is twofold: on one side, we want to understand the decidability frontier for fragments of the otherwise undecidable first-order separation logic; on the other side, we want to devise a very expressive separation logic featuring reachability predicates, whose satisfiability problem is decidable with a relatively low complexity (PSpace).In the second part, we take advantage of some of the techniques developed in the first part of the thesis in order to design Hilbert-style axiomatisations for separation logics and other spatial logics. In particular, we introduce the first sound and complete internal proof system for quantified-free separation logic and, by relying on the same technique, we design an axiomatisation for a modal logic enriched with the composition operator from ambient logic (a logic to verify distributed systems). The two proof systems reveal interesting connections between separation logics and ambient logics.In the third part of the thesis, we dig deep in the connections between separation logics and ambient logics, and find surprising similarities and differences, in terms of expressive power and computational complexity, between the separating conjunction of separation logic and the composition operator of ambient logic. In order to carry out our comparison, we devise a suitable framework based on modal logic, which gives us a common ground to study the two logics
15
Magill, Stephen. "Instrumentation Analysis: An Automated Method for Producing Numeric Abstractions of Heap-Manipulating Programs." Research Showcase @ CMU, 2010. http://repository.cmu.edu/dissertations/73.
Full textAbstract:
A number of questions regarding programs involving heap-based data structures can be phrased as questions about numeric properties of those structures. A data structure traversal might terminate if the length of some path is eventually zero or a function to remove n elements from a collection may only be safe if the collection has size at least n.
In this thesis, we develop proof methods for reasoning about the connection between heap-manipulating programs and numeric programs. In addition, we develop an automatic method for producing numeric abstractions of heap-manipulating programs. These numeric abstractions are expressed as simple imperative programs over integer variables and have the feature that if a property holds of the numeric program, then it also holds of the original, heap-manipulating program. This is true for both safety and liveness. The abstraction procedure makes use of a shape analysis based on separation logic and has support for user-defined inductive data structures.
We also discuss a number of applications of this technique. Numeric abstractions, once obtained, can be analyzed with a variety of existing verification tools. Termination provers can be used to reason about termination of the numeric abstraction, and thus termination of the original program. Safety checkers can be used to reason about assertion safety. And bound inference tools can be used to obtain bounds on the values of program variables. With small changes to the program source, bounds analysis also allows the computation of symbolic bounds on memory use and computational complexity.
16
Lively, Matthew C. "The Extraction of Shock Waves and Separation and Attachment Lines From Computational Fluid Dynamics Simulations Using Subjective Logic." BYU ScholarsArchive, 2012. https://scholarsarchive.byu.edu/etd/3287.
Full textAbstract:
The advancement of computational fluid dynamics to simulate highly complex fluid flow situations have allowed for simulations that require weeks of computation using expensive high performance clusters. These simulations often generate terabytes of data and hinder the design process by greatly increasing the post-processing time. This research discusses a method to extract shock waves and separation and attachment lines as the simulation is calculating and as a post-processing step. Software agents governed by subjective logic were used to make decisions about extracted features in converging and converged data sets. Two different extraction algorithms were incorporated for shock waves and separation and attachment lines and were tested on four different simulations. A supersonic ramp simulation showed two shock waves at 10% of convergence, but did not reach their final spatial locations until 85% convergence. A similar separation and attachment line analysis was performed on a cylinder in a cross flow simulation. The cylinder separation and attachment lines were within 5% of their final spatial locations at 10% convergence, and at 85% convergence, much of the cylinder and trailing separation and attachment lines showed probability expectation values of approximately 0.90 - 1.00. An Onera M6 wing simulation was used to investigate the belief tuples of the two separate shock waves at full convergence. Probability expectation values of approximately 0.90 - 1.00 were displayed within the two shock waves because they are strong shock waves and because they met the physical requirements of shock waves. A separation and attachment line belief tuple analysis was also performed on a delta wing simulation. The forward portions of these lines showed probability expectation values of approximately 0.90 - 1.00, but dropped to approximately 0.60 - 0.75 as a consequence of their respective vortices breaking down and losing their strength. Similar to shock waves, high probability expectation values meant the separation and attachment lines were strong and physically met separation and attachment line physics. The subjective logic process presented in this research was able to determine which shock waves and separation and attachment lines were most probable, making it easier to view and further investigate these important features.
17
Jansen, Christina Verfasser], Joost-Pieter [Akademischer Betreuer] [Katoen, Marieke [Akademischer Betreuer] Huisman, and Thomas [Akademischer Betreuer] Noll. "Static Analysis of Pointer Programs - Linking Graph Grammars and Separation Logic / Christina Jansen ; Joost-Pieter Katoen, Marieke Huisman, Thomas Noll." Aachen : Universitätsbibliothek der RWTH Aachen, 2017. http://d-nb.info/1161809023/34.
Full text
18
Jansen, Christina [Verfasser], Joost-Pieter [Akademischer Betreuer] Katoen, Marieke [Akademischer Betreuer] Huisman, and Thomas [Akademischer Betreuer] Noll. "Static Analysis of Pointer Programs - Linking Graph Grammars and Separation Logic / Christina Jansen ; Joost-Pieter Katoen, Marieke Huisman, Thomas Noll." Aachen : Universitätsbibliothek der RWTH Aachen, 2017. http://d-nb.info/1161809023/34.
Full text
19
Dias, Ricardo Jorge Freire. "Maintaining the correctness of transactional memory programs." Doctoral thesis, Faculdade de Ciências e Tecnologia, 2013. http://hdl.handle.net/10362/11092.
Full textAbstract:
Dissertação para obtenção do Grau de Doutor em
Engenharia InformáticaThis dissertation addresses the challenge of maintaining the correctness of transactional memory programs, while improving its parallelism with small transactions and relaxed isolation levels. The efficiency of the transactional memory systems depends directly on the level of parallelism, which in turn depends on the conflict rate. A high conflict rate between memory transactions can be addressed by reducing the scope of transactions, but this approach may turn the application prone to the occurrence of atomicity violations. Another way to address this issue is to ignore some of the conflicts by using a relaxed isolation level, such as snapshot isolation, at the cost of introducing write-skews serialization anomalies that break the consistency guarantees provided by a stronger consistency property, such as opacity. In order to tackle the correctness issues raised by the atomicity violations and the write-skew anomalies, we propose two static analysis techniques: one based in a novel static analysis algorithm that works on a dependency graph of program variables and detects atomicity violations; and a second one based in a shape analysis technique supported by separation logic augmented with heap path expressions, a novel representation based on sequences of heap dereferences that certifies if a transactional memory program executing under snapshot isolation is free from writeskew anomalies. The evaluation of the runtime execution of a transactional memory algorithm using snapshot isolation requires a framework that allows an efficient implementation of a multi-version algorithm and, at the same time, enables its comparison with other existing transactional memory algorithms. In the Java programming language there was no framework satisfying both these requirements. Hence, we extended an existing software transactional memory framework that already supported efficient implementations of some transactional memory algorithms, to also support the efficient implementation of multi-version algorithms. The key insight for this extension is the support for storing the transactional metadata adjacent to memory locations. We illustrate the benefits of our approach by analyzing its impact with both single- and multi-version transactional memory algorithms using several transactional workloads.
Fundação para a Ciência e Tecnologia - PhD research grant SFRH/BD/41765/2007, and in the research projects Synergy-VM (PTDC/EIA-EIA/113613/2009), and RepComp (PTDC/EIAEIA/ 108963/2008)
20
Bodin, Martin. "Certified semantics and analysis of JavaScript." Thesis, Rennes 1, 2016. http://www.theses.fr/2016REN1S087/document.
Full textAbstract:
JavaScript est un langage de programmation maintenant très utilisé - y compris dans des domaines où la sécurité est importante. Il est donc important de permettre de vérifier la qualité des logiciels écrit en JavaScript. Cette thèse explore l'approche de la preuve formelle, visant à donner une preuve mathématique qu'un programme donné se comporte comme prévu. Pour construire cette preuve, nous utilisons un assistant de preuve tel que Coq - un programme de confiance permettant de vérifier nos preuves formelles. Pour pouvoir énoncer qu'un programme JavaScript se comporte correctement, nous avons tout d'abord besoin d'une sémantique du langage JavaScript. Cette thèse s'est donc inscrite dans le projet JSCert visant à produire une sémantique formelle pour le langage JavaScript. Devant la taille de la sémantique de JavaScript, il est important de savoir comment on peut lui faire confiance : une faute de frappe peut compromettre toute la sémantique. Pour pouvoir faire confiance à JSCert, nous nous sommes appuyés sur deux sources de confiance. D'une part, JSCert a été conçue pour être très similaire à la spécification officielle de JavaScript, le standard ECMAScript : ils utilisent les mêmes structures de donnée, et il est possible d'associer chaque règle de réduction dans JSCert à une ligne d'ECMAScript. D'autre part, nous avons défini et prouvé relativement à JSCert un interpréteur nommé JSRef. Nous avons aussi pu lancer JSRef sur les suites de test de JavaScript. La sémantique de JSCert n'est pas la première sémantique formelle pour le JavaScript, mais c'est la première à proposer deux manières distinctes pour relier la sémantique formelle au langage JavaScript : en ayant une sémantique très similaire à la spécification officielle, et en ayant testé cette sémantique pour la comparer aux autres interpréteurs. Plutôt que de prouver indépendamment que chaque programme JavaScript s'exécute comme prévu, nous analysons ses programmes par interprétation abstraite. Cela consiste à interpréter la sémantique d'un langage avec des domaines abstraits. Par exemple la valeur concrète 1 pourra être remplacée par la valeur abstraite +. L'interprétation abstraite se compose en deux étapes : d'abord une sémantique abstraite est construite et prouvée correcte vis à vis de sa sémantique concrète, puis des analyseurs sont construits selon cette sémantique abstraite. Nous ne nous intéresserons qu'à la première étape dans cette thèse. La sémantique de JSCert est immense - plus de huit cent règles de réduction. La construction d'une sémantique abstraite traditionnelle ne passent pas à l'échelle face à de telles tailles. Nous avons donc conçu une nouvelle manière de construire des sémantiques abstraites à partir de sémantiques concrètes. Notre méthode se base sur une analyse précise de la structure des règles de réduction et vise à minimiser l'effort de preuve. Nous avons appliqué cette méthode sur plusieurs langages. Dans le but d'appliquer notre approche sur JavaScript, nous avons construit un domaine basé sur la logique de séparation. Cette logique requiert de nombreuses adaptations pour pouvoir s'appliquer dans le cadre de l'interprétation abstraite. Cette thèse en étudie les interactions et propose une nouvelle approche pour les solutionner dans le cadre construit précédemment. Nos domaines, bien qu'assez simple par rapport au modèle mémoire de JavaScript, semblent permettre la preuve d'analyseurs déjà existant. Les contributions de cette thèse sont donc triples : une sémantique formelle de confiance pour le langage JavaScript, un formalisme générique pour construire des sémantiques abstraites, et un domaine non trivial pour ce formalismeJavaScript is a trending programming language. It is not used in applications in which security may be an important issue. It thus becomes important to be able to control the quality of softwares written in JavaScript. This thesis explores a formal proof approach, which aims at giving a mathematical proof that a given program behaves as expected. To build this proof, we use proof assistants such as Coq—a trusted program enabling to check formal proofs. To state that a JavaScript program is behaving as expected, we first need a semantics of the JavaScript language. This thesis is thus part of the JSCert project, whose aim it to prove a formal semantics for JavaScript. Because of the size of JavaScript's semantics, it is crucial to know how it can be trusted: a typing mistake could compromise the whole semantics. To trust JSCert, we based ourselves on two trust sources. On one hand, JSCert has been designed to be the most similar it can be from the official JavaScript specification, the ECMAScript standard: they use the same data structures, and it is possible to relate each derivation rule in JSCert to a line of ECMAScript. On the other hand, we defined and proved correct with respect to JSCert an interpreter named JSRef. We have been able to run JSRef on JavaScript test suites. The JSCert semantics is not the first formal semantics of JavaScript, but it is the first to propose two distinct ways to relate the formal semantics to the JavaScript language: by having a semantics close to the official specification, and by testing this semantics and comparing it to other interpreters. Instead of independently proving that each JavaScript program behaves as expected, we chose to analyse programs using abstract interpretation. It consists of interpreting the semantics of a programming language with abstract domains. For instance, the concrete value 1 can be replaced by the abstract value +. Abstract interpretation is split into two steps : first, an abstract semantics is built and proven correct with respect to its concrete semantics, then, analysers are built from this abstract semantics. We only focus on the first step in this thesis. The JSCert semantics is huge - more than height hundred derivation rules. Building an abstract semantics using traditional techniques does not scale towards such sizes. We thus designed a new way to build abstract semantics from concrete semantics. Our approach is based on a careful analysis on the structure of derivation rules. It aims at minimising the proof effort needed to build an abstract semantics. We applied our method on several languages. With the goal of applying our approach to JavaScript, we built a domain based on separation logic. This logic require several adaptations to be able to apply in the context of abstract interpretation. This thesis precisely studies these interactions and introduces a new approach to solve them in our abstract interpretation framework. Our domains, although very simple compared to the memory model of JavaScript, seems to enable the proof of already existing analysers. This thesis has thus three main contributions : a trusted formal semantics for the JavaScript, a generic framework to build abstract semantics, and a non-trivial domain for this formalism
21
Tuch, Harvey Computer Science & Engineering Faculty of Engineering UNSW. "Formal memory models for verifying C systems code." Publisher:University of New South Wales. Computer Science & Engineering, 2008. http://handle.unsw.edu.au/1959.4/41233.
Full textAbstract:
Systems code is almost universally written in the C programming language or a variant. C has a very low level of type and memory abstraction and formal reasoning about C systems code requires a memory model that is able to capture the semantics of C pointers and types. At the same time, proof-based verification demands abstraction, in particular from the aliasing and frame problems. In this thesis, we study the mechanisation of a series of models, from semantic to separation logic, for achieving this abstraction when performing interactive theorem-prover based verification of C systems code in higher- order logic. We do not commit common oversimplifications, but correctly deal with C's model of programming language values and the heap, while developing the ability to reason abstractly and efficiently. We validate our work by demonstrating that the models are applicable to real, security- and safety-critical code by formally verifying the memory allocator of the L4 microkernel. All formalisations and proofs have been developed and machine-checked in the Isabelle/HOL theorem prover.
22
Boudou, Joseph. "Procédures de décision pour des logiques modales d'actions, de ressources et de concurrence." Thesis, Toulouse 3, 2016. http://www.theses.fr/2016TOU30145/document.
Full textAbstract:
Les concepts d'action et de ressource sont omniprésents en informatique. La caractéristique principale d'une action est de changer l'état actuel du système modélisé. Une action peut ainsi être l'exécution d'une instruction dans un programme, l'apprentissage d'un fait nouveau, l'acte concret d'un agent autonome, l'énoncé d'un mot ou encore une tâche planifiée. La caractéristique principale d'une ressource est de pouvoir être divisée, par exemple pour être partagée. Il peut s'agir des cases de la mémoire d'un ordinateur, d'un ensemble d'agents, des différent sens d'une expression, d'intervalles de temps ou de droits d'accès. Actions et ressources correspondent souvent aux dimensions temporelles et spatiales du système modélisé. C'est le cas par exemple de l'exécution d'une instruction sur une case de la mémoire ou d'un groupe d'agents qui coopèrent. Dans ces cas, il est possible de modéliser les actions parallèles comme étant des actions opérant sur des parties disjointes des ressources disponibles. Les logiques modales permettent de modéliser les concepts d'action et de ressource. La sémantique relationnelle d'une modalité unaire est une relation binaire permettant d'accéder à un nouvel état depuis l'état courant. Ainsi une modalité unaire correspond à une action. De même, la sémantique d'une modalité binaire est une relation ternaire permettant d'accéder à deux états. En considérant ces deux états comme des sous-états de l'état courant, une modalité binaire modélise la séparation de ressources. Dans cette thèse, nous étudions des logiques modales utilisées pour raisonner sur les actions, les ressources et la concurrence. Précisément, nous analysons la décidabilité et la complexité du problème de satisfaisabilité de ces logiques. Ces problèmes consistent à savoir si une formule donnée peut être vraie. Pour obtenir ces résultats de décidabilité et de complexité, nous proposons des procédures de décision. Ainsi, nous étudions les logiques modales avec des modalités binaires, utilisées notamment pour raisonner sur les ressources. Nous nous intéressons particulièrement à l'associativité. Alors qu'il est généralement souhaitable que la modalité binaire soit associative, puisque la séparation de ressources l'est, cette propriété rend la plupart des logiques indécidables. Nous proposons de contraindre la valuation des variables propositionnelles afin d'obtenir des logiques décidables ayant une modalité binaire associative. Mais la majeure partie de cette thèse est consacrée à des variantes de la logique dynamique propositionnelle (PDL). Cette logiques possède une infinité de modalités unaires structurée par des opérateurs comme la composition séquentielle, l'itération et le choix non déterministe. Nous étudions tout d'abord des variantes de PDL comparables aux logiques temporelle avec branchement. Nous montrons que les problèmes de satisfaisabilité de ces variantes ont la même complexité que ceux des logiques temporelles correspondantes. Nous étudions ensuite en détails des variantes de PDL ayant un opérateur de composition parallèle de programmes inspiré des logiques de ressources. Cet opérateur permet d'exprimer la séparation de ressources et une notion intéressante d'actions parallèle est obtenue par la combinaison des notions d'actions et de séparation. En particulier, il est possible de décrire dans ces logiques des situations de coopération dans lesquelles une action ne peut être exécutée que simultanément avec une autre. Enfin, la contribution principale de cette thèse est de montrer que, dans certains cas intéressants en pratique, le problème de satisfaisabilité de ces logiques a la même complexité que PDLThe concepts of action and resource are ubiquitous in computer science. The main characteristic of an action is to change the current state of the modeled system. An action may be the execution of an instruction in a program, the learning of a new fact, a concrete act of an autonomous agent, a spoken word or a planned task. The main characteristic of resources is to be divisible, for instance in order to be shared. Resources may be memory cells in a computer, performing agents, different meanings of a phrase, time intervals or access rights. Together, actions and resources often constitute the temporal and spatial dimensions of a modeled system. Consider for instance the instructions of a computer executed at memory cells or a set of cooperating agents. We observe that in these cases, an interesting modeling of concurrency arises from the combination of actions and resources: concurrent actions are actions performed simultaneously on disjoint parts of the available resources. Modal logics have been successful in modeling both concepts of actions and resources. The relational semantics of a unary modality is a binary relation which allows to access another state from the current state. Hence, unary modalities are convenient to model actions. Similarly, the relational semantics of a binary modality is a ternary relation which allows to access two states from the current state. By interpreting these two states as substates of the current state, binary modalities allow to divide states. Hence, binary modalities are convenient to model resources. In this thesis, we study modal logics used to reason about actions, resources and concurrency. Specifically, we analyze the decidability and complexity of the satisfiability problem of these logics. These problems consist in deciding whether a given formula can be true in any model. We provide decision procedures to prove the decidability and state the complexity of these problems. Namely, we study modal logics with a binary modality used to reason about resources. We are particularly interested in the associativity property of the binary modality. This property is desirable since the separation of resources is usually associative too. But the associativity of a binary modality generally makes the logic undecidable. We propose in this thesis to constrain the valuation of propositional variables to make modal logics with an associative binary modality decidable. The main part of the thesis is devoted to the study of variants of the Propositional Dynamic Logic (PDL). These logics features an infinite set of unary modalities representing actions, structured by some operators like sequential composition, iteration and non-deterministic choice. We first study branching time variants of PDL and prove that the satisfiability problems of these logics have the same complexity as the corresponding branching-time temporal logics. Then we thoroughly study extensions of PDL with an operator for parallel composition of actions called separating parallel composition and based on the semantics of binary modalities. This operator allows to reason about resources, in addition to actions. Moreover, the combination of actions and resources provides a convenient expression of concurrency. In particular, these logics can express situations of cooperation where some actions can be executed only in parallel with some other actions. Finally, our main contribution is to prove that the complexity of the satisfiability problem of a practically useful variant of PDL with separating parallel composition is the same as the satisfiability problem of plain PDL
23
Serban, Cristina. "Raisonnement automatisé pour la logique de séparation avec des définitions inductives." Thesis, Université Grenoble Alpes (ComUE), 2018. http://www.theses.fr/2018GREAM030/document.
Full textAbstract:
La contribution principale de cette thèse est un système de preuve correct et complet pour les implications entre les prédicats inductifs, fréquemment rencontrées lors de la vérification des programmes qui utilisent des structures de données récursives allouées dynamiquement. Nous introduisons un système de preuve généralisé pour la logique du premier ordre et nous l'adaptons à la logique de séparation, car ceci est un cadre qui répond aux plusieurs difficultés posées par le raisonnement sur les tas alloués dynamiquement. La correction et la complétude sont assurées par quatre restrictions sémantiques et nous proposons également un semi-algorithme de recherche de preuves qui devient une procédure de décision pour le problème d'implication lorsque les restrictions sémantiques sont respectées.Ce raisonnement d'ordre supérieur sur les implications nécessite des procédures de décision de premier ordre pour la logique sous-jacente lors de l'application des règles d'inférence et lors de la recherche des preuves. Ainsi, nous fournissons deux procédures de décision pour la logique de séparation, en considérant le fragment sans quantificateurs et le fragment quantifié de façon Exists*Forall*, qui ont été intégrées dans le solveur SMT open source CVC4.Finalement, nous présentons une implémentation de notre système de preuve pour la logique de séparation, qui utilise ces procédures de décision. Étant donné des prédicats inductifs et une requête d'implication, un avertissement est émis lorsqu'une ou plusieurs restrictions sémantiques sont violées. Si l'implication est valide, la sortie est une preuve. Sinon, un ou plusieurs contre-exemples sont fournisThe main contribution of this thesis is a sound and complete proof system for entailments between inductive predicates, which are frequently encountered when verifying programs that work with dynamically allocated recursive data structures. We introduce a generalized proof system for first-order logic, and then adapt it to separation logic, a framework that addresses many of the difficulties posed by reasoning about dynamically allocated heaps. Soundness and completeness are ensured through four semantic restrictions and we also propose a proof-search semi-algorithm that becomes a decision procedure for the entailment problem when the semantic restrictions hold.This higher-order reasoning about entailments requires first-order decision procedures for the underlying logic when applying inference rules and during proof search. Thus, we provide two decision procedures for separation logic, considering the quantifier-free and the Exists*Forall*-quantified fragments, which were integrated in the open-source, DPLL(T)-based SMT solver CVC4.Finally, we also give an implementation of our proof system for separation logic, which uses these decision procedures. Given some inductive predicate definitions and an entailment query as input, a warning is issued when one or more semantic restrictions are violated. If the entailment is found to be valid, the output is a proof. Otherwise, one or more counterexamples are provided
24
Gueneau, Armaël. "Mechanized verification of the correctness and asymptotic complexity of programs : the right answer at the right time." Thesis, Université de Paris (2019-....), 2019. http://www.theses.fr/2019UNIP7110.
Full textAbstract:
Cette thèse s’intéresse à la question de démontrer rigoureusement que l’implantation d’un algorithme donné est non seulement correcte (elle renvoie bien le bon résultat dans tous les cas possibles), mais aussi possède la bonne complexité asymptotique (elle calcule toujours ce résultat en le temps attendu).Pour les chercheurs en algorithmique, caractériser la performance d’un algorithme se fait généralement en indiquant sa complexité asymptotique, notamment à l’aide de la notation “grand O” due à Landau. Nous détaillons, tout d’abord informellement, pourquoi de telles bornes de complexité asymptotiques sont également utiles en tant que spécifications formelles. La raison est que celles-ci permettent de raisonner de façon modulaire à propos du coût d’un programme : une borne en O s’abstrait de l’expression exacte du coût du programme, et par là des divers détails d’implantation. Par ailleurs, nous illustrons, à l’aide d’exemples simples, un certain nombre de difficultés liées à l’utilisation rigoureuse de la notation O, et qu’il est facile de négliger lors d’un raisonnement informel.Ces considérations sont mises en pratique en formalisant d’une part la notation O dans l’assistant de preuve Coq, et d’autre part en étendant CFML, un outil existant dédié à la vérification de programmes, afin de permettre à l’utilisateur d’élaborer des démonstrations robustes et modulaires établissant des bornes de complexité asymptotiques. Nous étendons la logique de séparation avec crédits temps—qui permet de raisonner à la fois sur des propriétés de correction et de complexité en temps—avec la notion de crédits temps négatifs. Ces derniers augmentent l’expressivité de la logique, donnent accès à des principes de raisonnement commodes et permettent d’exprimer certaines spécifications de manière plus élégante. Au niveau des spécifications, nous montrons comment des bornes de complexité asymptotique avec O s’expriment en logique de séparation avec crédits temps. Afin d’être capable d’établir de telles spécifications, nous développons une méthodologie qui permet à l’utilisateur de développer des démonstrations qui soient à la fois robustes et menées à un niveau d’abstraction satisfaisant. Celle-ci s’appuie sur deux principes clefs : d’une part, un mécanisme permettant de collecter et remettre à plus tard certaines contraintes durant une démonstration interactive, et par ailleurs, un mécanisme permettant de synthétiser semi-automatiquement une expression de coût, et ce sans perte de généralité.Nous démontrons l’utilité et l’efficacité de notre approche en nous attaquant à un certain nombre d’études de cas. Celles-ci comprennent des algorithmes dont l’analyse de complexité est relativement simple (par exemple, une recherche dichotomique, déjà hors de portée de la plupart des approches automatisées) et des structures de données (comme les “binary random access lists” d’Okasaki). Dans notre étude de cas la plus significative, nous établissons la correction et la complexité asymptotique d’un algorithme incrémental de détection de cycles publié récemment. Nous démontrons ainsi que notre méthodologie passe à l’échelle, permet de traiter des algorithmes complexes, donc l’analyse de complexité s’appuie sur des invariants fonctionnels subtils, et peut vérifier du code qu’il est au final possible d’utiliser au sein de programmes réellement utiles et utilisésThis dissertation is concerned with the question of formally verifying that the imple- mentation of an algorithm is not only functionally correct (it always returns the right result), but also has the right asymptotic complexity (it reliably computes the result in the expected amount of time).In the algorithms literature, it is standard practice to characterize the performance of an algorithm by indicating its asymptotic time complexity, typically using Landau’s “big-O” notation. We first argue informally that asymptotic complexity bounds are equally useful as formal specifications, because they enable modular reasoning: a O bound abstracts over the concrete cost expression of a program, and therefore abstracts over the specifics of its implementation. We illustrate—with the help of small illustrative examples—a number of challenges with the use of the O notation, in particular in the multivariate case, that might be overlooked when reasoning informally.We put these considerations into practice by formalizing the O notation in the Coq proof assistant, and by extending an existing program verification framework, CFML, with support for a methodology enabling robust and modular proofs of asymptotic complexity bounds. We extend the existing framework of Separation Logic with Time Credits, which allows to reason at the same time about correctness and time complexity, and introduce negative time credits. Negative time credits increase the expressiveness of the logic, and enable convenient reasoning principles as well as elegant specifications. At the level of specifications, we show how asymptotic complexity specifications using O can be integrated and composed within Separation Logic with Time Credits. Then, in order to establish such specifications, we develop a methodology that allows proofs of complexity in Separation Logic to be robust and carried out at a relatively high level of abstraction, by relying on two key elements: a mechanism for collecting and deferring constraints during the proof, and a mechanism for semi-automatically synthesizing cost expressions without loss of generality.We demonstrate the usefulness and practicality of our approach on a number of increasingly challenging case studies. These include algorithms whose complexity analysis is relatively simple (such as binary search, which is nonetheless out of the scope of many automated complexity analysis tools) and data structures (such as Okasaki’s binary random access lists). In our most challenging case study, we establish the correctness and amortized complexity of a state-of-the-art incremental cycle detection algorithm: our methodology scales up to highly non-trivial algorithms whose complexity analysis intimately depends on subtle functional invariants, and furthermore makes it possible to formally verify OCaml code which can then actually be used as part of real world programs
25
Li, Huisong. "Shape abstractions with support for sharing and disjunctions." Thesis, Paris Sciences et Lettres (ComUE), 2018. http://www.theses.fr/2018PSLEE060.
Full textAbstract:
L'analyse statique des programmes permet de calculer automatiquement des propriétés sémantiques valides pour toutes les exécutions. En particulier, dans le cas des programmes manipulant des structures de données complexes en mémoire, l'analyse statique peut inférer des invariants utiles pour prouver la sûreté des accès à la mémoire ou la préservation d'invariants structurels. Beaucoup d'analyses de ce type manipulent des états mémoires abstraits représentés par des conjonctions en logique de séparation dont les prédicats de base décrivent des blocs de mémoire atomiques ou bien résument des régions non-bornées de la mémoire telles que des listes ou des arbres. De telles analyses utilisent souvent des disjonctions finies d’états mémoires abstraits afin de mieux capturer leurs dissimilarités. Les analyses existantes permettent de raisonner localement sur les zones mémoires mais présentent les inconvénients suivants: (1) Les prédicats inductifs ne sont pas assez expressifs pour décrire précisément toutes les structures de données dynamiques, du fait de la présence de pointeurs vers des parties arbitraires (i.e., non-locales) de ces structures ; (2) Les opérations abstraites correspondant à des accès en lecture ou en écriture sur ces prédicats inductifs reposent sur une opération matérialisant les cellules mémoires correspondantes. Cette opération de matérialisation crée en général de nouvelles disjonctions, ce qui nuit à l'impératif d'efficacité. Hélas, les prédicats exprimant des contraintes de structure locale ne sont pas suffisants pour déterminer de façon adéquate les ensembles de disjonctions devant être fusionnés, ni pour définir les opérations d'union et d'élargissement d'états abstraits. Cette thèse est consacrée à l'étude et la mise au point de prédicats en logique de séparation permettant de décrire des structures de données dynamiques, ainsi que des opérations abstraites afférentes. Nous portons une attention particulière aux opérations d'union et d'élargissement d’états abstraits. Nous proposons une méthode pratique permettant de raisonner globalement sur ces états mémoires au sein des méthodes existantes d'analyse de propriétés structurelles et autorisant la fusion précise et efficace de disjonctions. Nous proposons et implémentons une abstraction structurelle basée sur les variables d'ensembles qui lorsque elle est utilisée conjointement avec les prédicats inductifs permet la spécification et l'analyse de propriétés structurelles globales. Nous avons utilisé ce domaine abstrait afin d'analyser une famille de programmes manipulant des graphes représentés par liste d'adjacence. Nous proposons un critère sémantique permettant de fusionner les états mémoires abstraits similaires en se basant sur leur silhouette, cette dernière représentant certaines propriétés structurelles globales vérifiées par l'état correspondant. Les silhouettes s'appliquent non seulement à la fusion de termes dans les disjonctions d'états mémoires mais également à l'affaiblissement de conjonctions de prédicats de logique de séparation en prédicats inductifs. Ces contributions nous permettent de définir des opérateurs d’union et d'élargissement visant à préserver les disjonctions requises pour que l'analyse se termine avec succès. Nous avons implémenté ces contributions au sein de l'analyseur MemCAD et nous en avons évaluées l'impact sur l'analyse de bibliothèques existantes écrites en C et implémentant différentes structures de données, incluant des listes doublement chaînées, des arbres rouge-noir, des arbres AVL et des arbres "splay". Nos résultats expérimentaux montrent que notre approche est à même de contrôler la taille des disjonctions à des fins de performance sans pour autant nuire à la précision de l'analyseShape analyses rely on expressive families of logical properties to infer complex structural invariants, such that memory safety, structure preservation and other memory properties of programs dealing with dynamic data structures can be automatically verified. Many such analyses manipulate abstract memory states that consist of separating conjunctions of basic predicates describing atomic blocks or summary predicates that describe unbounded heap regions like lists or trees using inductive definitions. Moreover, they use finite disjunctions of abstract memory states in order to take into account dissimilar shapes. Although existing analyses enable local reasoning of memory regions, they do, however, have the following issues: (1) The summary predicates are not expressive enough to describe precisely all the dynamic data structures. In particular, a fairly large number of data structures with unbounded sharing, such as graphs, cannot be described inductively in a local manner; (2) Abstract operations that read or write into summaries rely on materialization of memory cells. The materialization operation in general creates new disjunctions, yet the size of disjunctions should be kept small for the sake of efficiency. However, local predicates are not enough to determine the right set of disjuncts that should be clumped together and to define precise abstract join and widen operations. In this thesis, we study separating conjunction-based shape predicates and the related abstract operations, in particular, abstract joining and widening operations that lead to critical modifications of abstract states. We seek a lightweight way to enable some global reasoning in existing shape analyses such that shape predicates are more expressive for abstracting data structures with unbounded sharing and disjuncts can be clumped precisely and efficiently. We propose a shape abstraction based on set variables that when integrated with inductive definitions enables the specification and shape analysis of structures with unbounded sharing. We implemented the shape analysis domain by combining a separation logic-based shape abstract domain of the MemCAD analyzer and a set abstract domain, where the set abstractions are used to track unbounded pointer sharing properties. Based on this abstract domain, we analyzed a group of programs dealing with adjacency lists of graphs. We design a general semantic criterion to clump abstract memory states based on their silhouettes that express global shape properties, \ie, clumping abstract states when their silhouettes are similar. Silhouettes apply not only to the conservative union of disjuncts but also to the weakening of separating conjunctions of memory predicates into inductive summaries. Our approach allows us to define union and widening operators that aim at preserving the case splits that are required for the analysis to succeed. We implement this approach in the MemCAD analyzer and evaluate it on real-world C libraries for different data structures, including doubly-linked lists, red-black trees, AVL-trees and splay-trees. The experimental results show that our approach is able to keep the size of disjunctions small for scalability and preserve case splits that takes into account dissimilar shapes for precision
26
Nigron, Pierre. "Effectful programs and their proofs in type theory : application to certified compilation and certified packet processing." Electronic Thesis or Diss., Sorbonne université, 2022. http://www.theses.fr/2022SORUS480.
Full textAbstract:
Pour pouvoir raisonner sur nos programmes, une méthode est de directement les écrire dans un assistant de preuve. Utilisant la correspondance de Curry-Howard, les programmes et les preuves ne font alors qu’un. Pour ne pas nuire à la cohérence logique de l’assistant de preuve, le système est obligé de restreindre les programmes à ne pas avoir d’effets de bord. Cependant, les effets de bord sont omniprésents et essentiels dans la programmation. Différentes techniques telles que les monades ou les effets algébriques ont alors émergé pour les modéliser offrant ainsi un moyen d'écrire des programmes impératifs dans des langages purement fonctionnels. C'est donc assez naturellement que les résultats de décennies de recherches investies pour raisonner sur des programmes impératifs tentent d'être adaptés au raisonnement sur des programmes avec effets. Dans cette thèse, nous nous intéressons d'abord à l'utilisation de la logique de séparation pour raisonner sur des programmes avec effets implémentés dans un assistant de preuve. Nous étudions une approche consistant à décrire les comportements des effets à l'aide d'un transformateur de prédicats. Nous nous concentrons d'abord sur la fraîcheur, puis sur le traitement de paquets et le zéro-copie. Pour étudier notre approche, nous nous appuyons sur deux exemples concrets qui sont le module SimplExpr de CompCert et la bibliothèque de décodeur Nom. Pour finir, pour compiler les analyseurs de paquets produits vers C, nous proposons une méthode par raffinement supprimant les continuations introduites par l'utilisation d'une monade libre et effectuant quelques optimisationsOne way to reason about our programs is to write them directly into a proof assistant. Using the Curry-Howard correspondence, programs and proofs are then one. In order not to undermine the logical consistency of the proof assistant, the system is forced to restrict the programs to have no side effects. However, side effects are ubiquitous and essential in programming. Different techniques such as monads or algebraic effects have emerged to model them, thus offering a way to write imperative programs in purely functional languages. It is therefore quite natural that the results of decades of research invested in reasoning about imperative programs try to be adapted to reasoning about programs with effects. In this thesis, we are first interested in the use of separation logic to reason about programs with effects implemented in a proof assistant. We study an approach to describe the behaviour of effects using a predicate transformer. We focus first on freshness, then on packet processing and zero-copy. To study our approach, we rely on two concrete examples which are the SimplExpr module of CompCert and the decoder library Nom. Finally, in order to compile the packet parsers produced to C, we propose a refinement method removing the continuations introduced by the use of a free monad and performing some optimizations
27
Faye, Wagane. "The Casamance Separatism from independence claim to resource logic." Thesis, Monterey, Calif. : Springfield, Va. : Naval Postgraduate School ; Available from National Technical Information Service, 2006. http://library.nps.navy.mil/uhtbin/hyperion/06Jun%5FFaye.pdf.
Full textAbstract:
Thesis (M.A. in Security Studies (Defense Decision Making and Planning))--Naval Postgraduate School, June 2006.Thesis Advisor(s): Letitia Lawson and Jessica Piombo. "June 2006." AD-A451 368. Includes bibliographical references. Also available via the World Wide Web.
28
Lengál, Ondřej. "Automaty v nekonečně stavové formální verifikaci." Doctoral thesis, Vysoké učení technické v Brně. Fakulta informačních technologií, 2015. http://www.nusl.cz/ntk/nusl-261279.
Full textAbstract:
Tato práce se zaměřuje na konečné automaty nad konečnými slovy a konečnými stromy, a použití těchto automatů při formální verifikaci nekonečně stavových systémů. Práce se nejdříve věnuje rozšíření existujícího přístupu pro verifikaci programů které manipulují s haldou (konkrétně programů s dynamickými datovými strukturami), jenž je založen na stromových automatech. V práci je navrženo několik rozšíření tohoto přístupu, jako například jeho plná automatizace či jeho rozšíření o podporu uspořádaných dat. V práci jsou popsány nové rozhodovací procedury pro dvě logiky, které jsou často používány ve formální verifikaci: pro separační logiku a pro slabou monadickou druhořádovou logiku s následníkem. Obě tyto rozhodovací procedury jsou založeny na převodu jejich problému do automatové domény a následné manipulaci v této cílové doméně. Posledním přínosem této práce je vývoj nových algoritmů k efektivní manipulaci se stromovými automaty, s důrazem na testování inkluze jazyků těchto automatů a manipulaci s automaty s velkými abecedami, a implementace těchto algoritmů v knihovně pro obecné použití. Tyto vyvinuté algoritmy jsou použity jako klíčová technologie, která umožňuje použití výše uvedených technik v praxi.
29
Bardou, Romain. "Vérification de programmes avec pointeurs à l'aide de régions et de permissions." Thesis, Paris 11, 2011. http://www.theses.fr/2011PA112220/document.
Full textAbstract:
La vérification déductive de programmes consiste à annoter des programmes par une spécification, c'est-à-dire un ensemble de formules logiques décrivant le comportement du programme, et à prouver que les programmes vérifient bien leur spécification. Des outils tels que la plate-forme Why prennent en entrée un programme et sa spécification et calculent des formules logiques telles que, si elles sont prouvées, le programme vérifie sa spécification. Ces formules logiques peuvent être prouvées automatiquement ou à l'aide d'assistants de preuve.Lorsqu'un programme est écrit dans un langage supportant les alias de pointeurs, c'est-à-dire si plusieurs variables peuvent désigner la même case mémoire, alors le raisonnement sur le programme devient particulièrement ardu. Il est nécessaire de spécifier quels pointeurs peuvent être égaux ou non. Les invariants des structures de données, en particulier, sont plus difficiles à vérifier.Cette thèse propose un système de type permettant de structurer la mémoire de façon modulaire afin de contrôler les alias de pointeurs et les invariants de données. Il est basé sur les notions de région et de permission. Les programmes sont ensuite interprétés vers Why de telle façon que les pointeurs soient séparés au mieux, facilitant ainsi le raisonnement. Cette thèse propose aussi un mécanisme d'inférence permettant d'alléger le travail d'annotation des opérations de régions introduites par le langage. Un modèle est introduit pour décrire la sémantique du langage et prouver sa sûreté. En particulier, il est prouvé que si le type d'un pointeur affirme que celui-ci vérifie son invariant, alors cet invariant est effectivement vérifié dans le modèle. Cette thèse a fait l'objet d'une implémentation sous la forme d'un outil nommé Capucine. Plusieurs exemples ont été écrits pour illustrer le langage, et ont été vérifié à l'aide de CapucineDeductive verification consists in annotating programs by a specification, i.e. logic formulas which describe the behavior of the program, and prove that programs verify their specification. Tools such as the Why platform take a program and its specification as input and compute logic formulas such that, if they are valid, the program verifies its specification. These logic formulas can be proven automatically or using proof assistants.When a program is written in a language supporting pointer aliasing, i.e. if several variables may denote the same memory cell, then reasoning about the program becomes particularly tricky. It is necessary to specify which pointers may or may not be equal. Invariants of data structures, in particular, are harder to maintain.This thesis proposes a type system which allows to structure the heap in a modular fashion in order to control pointer aliases and data invariants. It is based on the notions of region and permission. Programs are then translated to Why such that pointers are separated as best as possible, to facilitate reasoning. This thesis also proposes an inference mechanism to alleviate the need to write region operations introduced by the language. A model is introduced to describe the semantics of the language and prove its safety. In particular, it is proven that if the type of a pointer tells that its invariant holds, then this invariant indeed holds in the model. This work has been implemented as a tool named Capucine. Several examples have been written to illustrate the language, and where verified using Capucine
30
Illous, Hugo. "Abstractions relationnelles de la mémoire pour une analyse compositionnelle de structures de données." Thesis, Paris Sciences et Lettres (ComUE), 2019. http://www.theses.fr/2019PSLEE015.
Full textAbstract:
Les analyses statiques ont pour but d’inférer des propriétés sémantiques de programmes. Nous distinguons deux importantes classes d’analyses statiques : les analyses d’états et les analyses relationnelles. Alors que les analyses d’états calculent une sur-approximation de l’ensemble des états atteignables d’un programme, les analyses relationnelles calculent des propriétés fonctionnelles entre les états d’entrée et les états de sortie d’un programme. Les analyses relationnelles offrent plusieurs avantages, comme leur capacité à inférer des propriétés sémantiques plus expressives par rapport aux analyses d’états. De plus, elles offrent également la possibilité de rendre l’analyse compositionnelle, en utilisant les relations entrée-sortie comme des résumés de procédures, ce qui est un avantage pour le passage à l’échelle. Dans le cas des programmes numériques, plusieurs analyses ont été proposées qui utilisent des domaines abstraits numériques relationnels, pour décrire des relations. D’un autre côté, modéliser des abstractions de relations entre les états mémoires entrée-sortie tout en prenant en compte les structures de données est difficile. Dans cette Thèse, nous proposons un ensemble de nouveaux connecteurs logiques, reposant sur la logique de séparation, pour décrire de telles relations. Ces connecteurs peuvent exprimer qu’une certaine partie de la mémoire est inchangée, fraîchement allouée, ou désallouée, ou que seulement une seule partie de la mémoire est modifiée (et de quelle manière). En utilisant ces connecteurs, nous construisons un domaine abstrait relationnel et nous concevons une analyse statique compositionnelle par interprétation abstraite qui sur-approxime des relations entre des états mémoires contenant des structures de données inductives. Nous avons implémenté ces contributions sous la forme d’un plug-in de l’analyseur FRAMA-C. Nous en avons évalué l’impact sur l’analyse de petits programmes écrits en C manipulant des listes chaînées et des arbres binaires, mais également sur l’analyse d’un programme plus conséquent qui consiste en une partie du code source d’Emacs. Nos résultats expérimentaux montrent que notre approche permet d’inférer des propriétés sémantiques plus expressives d’un point de vue logique que des analyses d’états. Elle se révèle aussi beaucoup plus rapide sur des programmes avec un nombre conséquent d’appels de fonctions sans pour autant perdre en précisionStatic analyses aim at inferring semantic properties of programs. We distinguish two important classes of static analyses: state analyses and relational analyses. While state analyses aim at computing an over-approximation of reachable states of programs, relational analyses aim at computing functional properties over the input-output states of programs. Relational analyses offer several advantages, such as their ability to infer semantics properties more expressive compared to state analyses. Moreover, they offer the ability to make the analysis compositional, using input-output relations as summaries for procedures, which is an advantage for scalability. In the case of numeric programs, several analyses have been proposed that utilize relational numerical abstract domains to describe relations. On the other hand, designing abstractions for relations over input-output memory states and taking shapes into account is challenging. In this Thesis, we propose a set of novel logical connectives to describe such relations, which rely on separation logic. This logic can express that certain memory areas are unchanged, freshly allocated, or freed, or that only part of the memory is modified (and how). Using these connectives, we build an abstract domain and design a compositional static analysis by abstract interpretation that over-approximates relations over memory states containing inductive structures. We implement this approach as a plug-in of the FRAMA-C analyzer. We evaluate it on small programs written in C that manipulate singly linked lists and binary trees, but also on a bigger program that consists of a part of Emacs. The experimental results show that our approach allows us to infer more expressive semantic properties than states analyses, from a logical point of view. It is also much faster on programs with an important number of function calls without losing precision
31
Bambaci, Juliana. "Presidential discretion in separation of powers systems /." May be available electronically:, 2007. http://proquest.umi.com/login?COPT=REJTPTU1MTUmSU5UPTAmVkVSPTI=&clientId=12498.
Full text
32
Kilic, Alper, and Johan Åkesson. "Kartläggning av önskvärda egenskaper i arkitekturer samt ramverk för separation av användargränssnitt från logik." Thesis, Malmö universitet, Fakulteten för teknik och samhälle (TS), 2019. http://urn.kb.se/resolve?urn=urn:nbn:se:mau:diva-20669.
Full textAbstract:
Choosing an architecture or a framework for a system can be tricky at times especially for beginners. The wrong choice can not only affect the projects success rate negatively but can also be a bad business decision. When developing a new framework or architecture the developer should know what properties that framework or architecture should support. This study have therefore chosen to present different architectures and frameworks and analyze their properties.’By using semi-structured interviews and internet surveys to ask developers about these properties we have presented why and which properties are most important and what developers are looking for in an architecture or a framework. Thereby the purpose of this study is to either offer the reader help with choosing the right architecture or acknowledge the properties when developing a new one. Similar studies seem to focus on undefined adjectives whereas this study will explain and discuss these properties in detail. The result of the study is too weak to be able to represent all developers but could indicate that ease of use, documentation, a community and a unidirectional data flow are properties that are preferred. The respondents are however torn and seem to have different opinions on whether or not properties such as pre-generated code, modularity and testability should be preferred over other properties. The goal is to hopefully inspire other studies to examine these properties further or to help developers understand frameworks and architectures and their properties better, thereby making it easier for them to choose one or to develop one.
33
Sookbirsingh, Rudy. "Salt separation processes in salt cedar Tamarix ramosissima (Ledeb) /." To access this resource online via ProQuest Dissertations and Theses @ UTEP, 2009. http://0-proquest.umi.com.lib.utep.edu/login?COPT=REJTPTU0YmImSU5UPTAmVkVSPTI=&clientId=2515.
Full text
34
Liang, Yifan. "Separation optimality and generalized source-channel coding for time-varying channels /." May be available electronically:, 2008. http://proquest.umi.com/login?COPT=REJTPTU1MTUmSU5UPTAmVkVSPTI=&clientId=12498.
Full text
35
Khurana, Tarun K. "On-chip isotachophoresis assays for high sensitivity electrophoretic preconcentration, separation, and indirect detection /." May be available electronically:, 2008. http://proquest.umi.com/login?COPT=REJTPTU1MTUmSU5UPTAmVkVSPTI=&clientId=12498.
Full text
36
Delgado, Guillermo Guadalupe. "Treatment of RO concentrate using VSEP technology." To access this resource online via ProQuest Dissertations and Theses @ UTEP, 2009. http://0-proquest.umi.com.lib.utep.edu/login?COPT=REJTPTU0YmImSU5UPTAmVkVSPTI=&clientId=2515.
Full text
37
Fernandez, Alvaro. "Moving from rocks to hydrologic systems are Cu, Fe, and Zn isotopes fractionated during weathering? /." To access this resource online via ProQuest Dissertations and Theses @ UTEP, 2008. http://0-proquest.umi.com.lib.utep.edu/login?COPT=REJTPTU0YmImSU5UPTAmVkVSPTI=&clientId=2515.
Full text
38
Ducroux, Amélie. "Le problème de la relation dans la poésie de T.S. Eliot." Thesis, Lyon 2, 2011. http://www.theses.fr/2011LYO20065.
Full textAbstract:
Le problème de la relation a souvent été perçu par les lecteurs d’Eliot comme un manque de relations logiques, grammaticales, chronologiques, entraînant une difficulté à faire sens des poèmes. Ce manque perçu entraîne le lecteur à rechercher des relations dans la structure interne du poème ou dans le matériau intertextuel ou symbolique qu’il convoque. Il se confronte alors à une pratique intertextuelle bien particulière, non exempte d’une certaine forme de tromperie. La poésie d’Eliot fait jouer les relations syntaxiques, logiques et temporelles attendues. Cette poétique de l’indétermination met en déroute les tentatives de mise en relation logique. C’est pourtant l’ambiguïté de la syntaxe et cette poétique dialectique du paradoxe et de la non exclusion, qui rendent la lecture inépuisable. Le poète ne cesse de « parler » du problème de la relation. Il le met en œuvre et le travaille, instaurant une tension entre des dynamiques relationnelles qui s’opposent. La relation devient choc, collision. La logique du poème se fait autre, en appelle à la sensation autant qu’à la pensée. La relation déconstruit, elle devient porteuse tout en restant sous-entendue. T.S. Eliot n’a cessé, à travers sa poésie, de problématiser l’acte d’écriture lui-même. Il y apparaît comme un acte décisif, comme une mise en relation qui offre la possibilité d’une continuité tout en marquant une rupture. En donnant lieu au poème, le poète le relie à son extériorité même. Mais cette relation réinscrit en même temps la division au cœur du langage. La problématisation de ce rapport ambigu à l’écriture trouve à s’exprimer dans les relations établies entre des voix discordantes, entre le sujet et ses autres, et dans cette oscillation continue entre des positions discursives et métaphysiques en conflit. La construction du poème éliotien se fonde ainsi sur la possibilité même de sa déconstruction. Le poète offre des poèmes en déconstruction dans lesquels s’inscrit un sujet lui-même en perpétuelle dépossession de soi. Il ne s’agit pas, pour Eliot, de penser l’écriture, mais de se penser à partir de l’écriture. L’écriture est première. Elle est la condition même de la pensée de la relation qui s’élabore dans son œuvreThe problem of relation has often been perceived by readers of Eliot as a lack of logical or grammatical relations, which makes it difficult to understand his poems. This perceived deficiency causes the reader to look for relations in the very structure of the poem, in the texts the poem alludes to, or in the mythical structures it relies upon. The reader becomes aware of the singularity of Eliot’s sometimes misleading intertextual practice. The poetry of T.S. Eliot plays with and distorts syntactic, logical and temporal relations. His poetics of indeterminacy precludes any attempt to establish logical relations within the poems. Yet the very ambiguity of Eliot’s syntax and the paradoxical nature of his dialectical poetics make of reading itself an unlimited and unrestrained process. The poet constantly addresses the problem of relation. The problem itself is inseparable from the poetic idiom which gives it voice. It is explored along the lines of a tension between conflicting relational dynamics, creating a new logic which relies on sensibility as well as on thought and rationality. Relations deconstruct the poem; they are pregnant while remaining “hints half guessed”. Through his poetry, T.S. Eliot never stopped questioning writing itself. The act of writing results from a decision; it is an articulation offering the possibility of continuity while marking a rupture at the same time. By giving birth to the poem, the poet links it to its own exteriority. But such linkage also reiterates the division inherent to language itself. The problem of this ambiguous relation to writing is expressed through the relations established, within the poems, between discordant voices, between the subject and its masks, and through a constant oscillation between conflicting discursive and metaphysical stances. The construction of the poem thus relies on the very possibility of its deconstruction. Eliot offers poems in deconstruction in which the subject itself can only emerge through an act of self-dispossession. Eliot does not merely reflect upon writing through his poetry. Writing itself becomes the means of his own definition as a poet. Writing comes first. It is the condition of Eliot’s poetic exploration of relation
39
Snell, Brandon Charles. "The Origins of Ethno/National Separatist Terrorism: A Cross-National Analysis of the Background Conditions of Terrorist Campaigns." Wright State University / OhioLINK, 2009. http://rave.ohiolink.edu/etdc/view?acc_num=wright1244481182.
Full text
40
Bobot, François. "Logique de séparation et vérification déductive." Phd thesis, Université Paris Sud - Paris XI, 2011. http://tel.archives-ouvertes.fr/tel-00652508.
Full textAbstract:
Cette thèse s'inscrit dans la démarche de preuve de programmes à l'aide de vérification déductive. La vérification déductive consiste à produire, à partir des sources d'un programme, c'est-à-dire ce qu'il fait, et de sa spécification, c'est-à-dire ce qu'il est sensé faire, une conjecture qui si elle est vraie alors le programme et sa spécification concordent. On utilise principalement des démonstrateurs automatiques pour montrer la validité de ces formules. Quand ons'intéresse à la preuve de programmes qui utilisent des structures de données allouées en mémoire, il est élégant et efficace de spécifier son programme en utilisant la logique de séparation qui est apparu il y a une dizaine d'année. Cela implique de prouver des conjectures comportant les connectives de la logique de séparation, or les démonstrateurs automatiques ont surtout fait des progrès dans la logique du premier ordre qui ne les contient pas.Ce travail de thèse propose des techniques pour que les idées de la logique de séparation puissent apparaître dans les spécifications tout en conservant la possibilité d'utiliser des démonstrateurs pour la logique du premier ordre. Cependant les conjectures que l'ont produit ne sont pas dans la même logique du premier ordre que celles des démonstrateurs. Pour permettre une plus grande automatisation, ce travail de thèse a également défini de nouvelles conversions entre la logique polymorphe du premier ordre et la logique multi-sortée dupremier ordre utilisé par la plupart des démonstrateurs.La première partie a donné lieu à une implémentation dans l'outil Jessie, la seconde a donné lieu à une participation conséquente à l'écriture de l'outil Why3 et particulièrement dans l'architecture et écriture des transformations qui implémentent ces simplifications et conversions.
41
Kimmel, Pierre. "Extensions modales des logiques de ressources : expressivité et calculs." Thesis, Université de Lorraine, 2018. http://www.theses.fr/2018LORR0299/document.
Full textAbstract:
Le développement de nouveaux formalismes logiques est au cœur de nombreuses problématiques de méthodes formelles. Ces formalismes doivent répondre à la fois à des impératifs de modélisation (ils doivent permettre de décrire certains systèmes) et de calcul (ils doivent fournir des méthodes de calcul correctes et complètes). Dans ce contexte, nous nous intéressons aux logiques de ressources, en particulier les logiques BI et BBI qui traitent du partage et de la séparation de ressources et qui ont conduit aux diverses logiques de séparation dont les applications à la vérification de programmes se sont développées fortement ces dernières années. Nous proposons dans cette thèse d’étudier, à partir des logiques BI et BBI, des logiques de séparation modales et épistémiques en se focalisant sur leurs capacités de modélisation et leur expressivité mais aussi les nouveaux calculs de preuve pour ces logiques. Une première étude a porté sur la modélisation de propriétés dynamiques de ressources au travers d’une nouvelle logique LTBI, qui est une logique de séparation temporelle, fondée sur la logique BI et des modalités temporelles. Cette logique offre notamment des perspectives intéressantes de modélisation temporelle branchante, permettant par exemple de caractériser les processus multi-thread. Une étude complémentaire a porté sur la modélisation de l’accès par des agents à des propriétés sous conditions de posséder certaines ressources, au travers d’une nouvelle logique ERL, qui est une logique de séparation épistémique, fondée sur la logique BBI et des modalités épistémiques. Cette logique permet de nombreuses modélisations de systèmes de contrôle d’accès. En vue d’étendre l’expressivité de telles logiques de séparation, comme la logique BBI et ses variantes, une étude sur l’internalisation des symboles de ressources dans la syntaxe de la logique a été développée au travers des nouvelles logiques HRL et HBBI (version hybride de BBI). L’internalisation permet à la fois d’étendre l’expressivité des logiques et d’axiomatiser la logique BBI et certaines de ses variantes. Outre la conception de ces logiques, l’étude de leur sémantique et aussi de leurs capacités de modélisation, une partie de cette thèse a été consacrée à la définition de calculs de preuve, ici de tableaux, pour ces nouvelles logiques ainsi qu’à leurs preuves de correction et de complétudeThe design of new logical formalisms is at the heart of several problems in formal methods. Those formalisms must respond to requirements both concerning modelling (they must be able to describe certain systems) and computing (they must provide complete and sound calculus methods). In this context, we look at resource logics, and in particular BI and BBI logics, that deal with the separation and sharing of resources and have led to several separation logics whose applications to software verification have been widely developped recently. We propose in this thesis, starting from BI and BBI logics, to study some modal and epistemic separation logics by focusing on their modelling capacities and their expresiveness, as well as on the new proof calculi for those logics. A first study deals with the modelling of dynamic resource properties through new logic LTBI, which is a temporal separation logic, based on BI logic and temporal modalities. This logic notably offers interesting perspectives in temporal branching modelling, allowing for instance to characterize multi-thread processes. A complementary study concerns the modelling of access by agents to properties under the conditions of posessing some resources, through a new logic ERL, which is an epistemic separation logic, based on BBI logic and epistemic modalities. This logic allows many modellings of access control systems. In order to extend the expressivity of such separation logics, like BBI logic and its variants, a study on the internalization of resources symbols in the logic’s syntax has been developed through the new logics HRL and HBBI (hybrid version of BBI). Internalization allows both the extension of the expressivity of logics and the axiomatisation of BBI logic and some of its variants. In addition to the conception of those logics, the study of their semantics and their modelling capacities, a part of this thesis is dedicated to the definition of proof calculs, here tableaux calculus, for those new logics, as well as their proof of soundness and completeness
42
Piroska, Marian-Leonard. "Engineering artificial biomolecular condensates to study the aggregation of α-Synuclein." Electronic Thesis or Diss., Sorbonne université, 2023. https://accesdistant.sorbonne-universite.fr/login?url=https://theses-intra.sorbonne-universite.fr/2023SORUS542.pdf.
Full textAbstract:
Les maladies neurodégénératives, telles que les maladies d'Alzheimer, de Parkinson et de Huntington, sont des maladies incurables caractérisées par une perte progressive de neurones, entraînant des déficits cognitifs et moteurs chez les patients. Le développement de traitements efficaces est actuellement limité par notre compréhension incomplète des mécanismes à l’origine de l’initiation et de la progression de la maladie. Une caractéristique dominante observée dans les tissus affectés par les ces maladies est la présence de protéines agrégées, qui sont devenues la marque de maladies telles que la maladie de Parkinson et la maladie d’Alzheimer. Ainsi, le processus d’agrégation jouerait un rôle central dans la pathogenèse de la maladie. Cependant, les mécanismes spécifiques qui sous-tendent la transition des protéines solubles vers leur état agrégé restent insaisissables. Des recherches récentes ont proposé la séparation de phase (PS) comme étape intermédiaire critique dans la formation d'agrégats de protéines. La PS est un phénomène physique dans lequel certaines protéines subissent une transition de phase, formant des gouttelettes distinctes ayant des propriétés de liquide dans l'environnement cellulaire. Les condensats biomoléculaires sont impliqués dans divers processus physiologiques, mais sont de plus en plus supposes d’être sujets à des comportements aberrants pouvant déclencher des conditions pathologiques. Bien que prometteuse, l’étude du rôle du PS dans le contexte des maladies neurodégénératives reste une tâche difficile en raison de la composition complexe des condensats cellulaires. Ils sont constitués de dizaines, voire de centaines de biomolécules différentes, notamment des protéines, des acides nucléiques et des lipides, créant un milieu complexe qui exige des approches de recherche innovantes. Pour améliorer l'étude de la PS dans le contexte des maladies neurodégénératives, nous avons développé une méthode de formation et de dissolution contrôlées de condensats biomoléculaires enrichis en protéines impliquées dans l'agrégation pathologique. Tout d’abord, nous avons créé des condensats contenant de l’α-synucléine (α-Syn), le principal facteur pathologique de la maladie de Parkinson et d’autres pathologies. L'α-Syn est connue comme une protéine de type prion, ce qui signifie que son agrégat se propage de cellule en cellule et modèle l'agrégation de l'α-Syn cytosolique soluble, favorisant ainsi la progression de la maladie. Cependant, on sait peu de choses sur ce phénomène en ce qui concerne l’état condensé de la protéine. Pour simuler cela, nous avons exposé des cellules exprimant nos condensats α-Syn à des agrégats α-Syn préformés sous forme fibrillaire. Nous avons observé que les fibrilles déclenchaient la transition des condensats de leur état liquide à une forme agrégée ayant des propriétés solides et présentant des marqueurs biochimiques caractéristiques des amyloïdes. Cela nous a permis de proposer un modèle dans lequel la phase condensée de α-Syn accélère la propagation des agrégats pathologiques, en fournissant un pool de protéines concentrées pouvant subir plus facilement une transition amyloïde via le mécanisme de type prion. Par la suite, nous avons construit des condensats artificiels enrichis en α-Syn et la synapsine. Dans les neurones, α-Syn et la synapsine interagissent aux extrémités présynaptiques, où ils jouent un rôle important dans la libération des neurotransmetteurs en contrôlant le regroupement, le trafic et la libération de conteneurs de neurotransmetteurs appelés vésicules synaptiques. Nos condensats d'α-Syn/synapsine étaient eux également soumis à une transition liquide-solide médiée par les fibrilles d'α-SynNeurodegenerative diseases, such as Alzheimer's, Parkinson's, and Huntington's disease, are incurable illnesses characterized by the progressive degeneration of neurons, leading to cognitive and motor deficits in affected individuals. The development of effective treatments is currently limited by our incomplete understanding of the underlying mechanisms that drive disease initiation and progression. One prevailing characteristic observed in the tissues affected by neurodegenerative diseases is the presence of aggregated proteins, which have become hallmarks of diseases such as Parkinson’s and Alzheimer’s. Thus, the aggregation process is believed to play a pivotal role in disease pathogenesis. However, the specific mechanisms underlying the transition of soluble proteins to their aggregated state remain elusive. Recent research has proposed phase separation (PS) as a critical intermediate step in the formation of protein aggregates. PS is a physical phenomenon wherein certain proteins undergo a phase transition, forming distinct liquid-like droplets within the cellular environment. Biomolecular condensates are involved in various physiological cellular processes, but are also increasingly believed to be subject to aberrant behaviours that can trigger pathological conditions. Although promising, studying the role of PS in the context of neurodegenerative diseases is a challenging task, due to the intricate composition of cellular condensates. They consist of tens to hundreds of different biomolecules, including proteins, nucleic acids, and lipids, creating a complex milieu that demands innovative research approaches. To improve the study of LLPS in the context of neurodegenerative diseases, we have developed a method for the controlled formation and dissolution of biomolecular condensates enriched in proteins involved in pathological aggregation. First, we created condensates containing α-synuclein (α-Syn), the main pathological factor in Parkinson’s disease and other pathologies. α-Syn is known as a prion-like protein, meaning that its aggregates spreads from cell to cell and template the aggregation of soluble cytosolic α-Syn, promoting the progression of the disease. However, little is known about this phenomenon with respect to the condensed state of the protein. To simulate this phenomenon, we exposed cells expressing our α-Syn condensates to preformed α-Syn aggregates in fibrillar form. We observed that fibrils triggered the transition of condensates from their liquid-like state to an aggregated form with solid-like properties and exhibiting biochemical markers characteristic of amyloids. This allowed us to propose a model where the condensed phase of α-Syn speeds up the propagation of pathological aggregates, by providing a pool of concentrated protein that can undergo more easily an amyloid transition via the prion-like pathway. Subsequently, we have built artificial condensates enriched in α-Syn together with synapsin. In neurons, α-Syn and synapsin interact at the presynaptic termini, where they play an important role in the release of neurotransmitters by controlling the clustering, trafficking and release of membrane-enclosed neurotransmitter containers called synaptic vesicles. In our setting α-Syn/synapsin condensates were also subject to a liquid-to-solid transition mediated by α-Syn fibrils
43
Toudic, Hugo. "Inventer la république. L'héritage de Montesquieu dans la controverse constitutionnelle entre Antifédéralistes et Fédéralistes (1787-1789)." Electronic Thesis or Diss., Sorbonne université, 2024. https://accesdistant.sorbonne-universite.fr/login?url=https://theses-intra.sorbonne-universite.fr/2024SORUL033.pdf.
Full textAbstract:
Se pourrait-il que l'influence de Montesquieu sur les idées des Pères fondateurs américains ait été jusqu'à nos jours largement ignorée ? C'est ce que tend à démontrer et à corriger ce travail de recherche. Une simple étude de l'historiographie des différentes philosophies qui marquèrent la fin du XVIIIe siècle américain permet en effet de constater qu'à la place prépondérante qu'y occupe Montesquieu ne correspond pas de travaux d'ampleur à même de relever et d'analyser les emprunts faits à sa philosophie. Pourtant, une telle tâche permettrait de comprendre pourquoi Montesquieu fit figure d'autorité et même, selon les propres mots des Pères fondateurs, d'oracle de la science politique. Ce faisant, un tel travail permettrait enfin de redonner toutes ses lettres de noblesse à un chef-d'œuvre de philosophie politique - les Federalist papers - que loua en son temps Tocqueville et qui est, encore aujourd'hui, la bible laïque de la république américaineCould it be that the influence of Montesquieu on the Founding Fathers' ideas has been largely overlooked? That is what this dissertation aims at both proving and correcting. A mere historiographic study of influential philosophical thought in the late eighteenth century shows that the predominant importance of Montesquieu's philosophy is not met with extensive and careful academic works capable of finding and then analyzing the way in which the Founding Fathers borrowed from his philosophy. Yet, such an analysis would permit us to understand why Montesquieu was considered an authority and even, according to the very words of the Founding Fathers, an oracle of the science of politics. Furthermore, this research would finally allow to lend cachet within the European academic world to a masterpiece of political philosophy, the Federalist papers, whom no less than Tocqueville once praised and which remains the very secular bible of the American Republic
44
Michalak, Thomas. "Les Assemblées parlementaires, juge pénal : analyse d’un paradigme irréalisable : (1789-1918)." Electronic Thesis or Diss., Paris 2, 2020. https://buadistant.univ-angers.fr/login?url=https://bibliotheque.lefebvre-dalloz.fr/secure/isbn/9782247218530.
Full textAbstract:
L’intitulé renvoie, en première approche, aux expériences institutionnelles de la Cour des pairs (1814-1848) et du Sénat de la IIIe République (1875-1940). Ce sont les manifestations les plus marquantes de la participation d’une assemblée parlementaire à la reddition de la justice. Le procès des ministres de Charles X et celui de Malvy semblent être bien connus mais ils ne le sont en réalité qu’imparfaitement. Dans les deux cas, les Chambres hautes se sont détournées de leur mission de législateur et de contrôleur du gouvernement pour se métamorphoser, de manière très incomplète, en instances judiciaires. Cependant le traitement isolé de ces deux seules expériences ne permet pas de définir la mission d’une juridiction parlementaire. La notion de Haute Cour de justice, quelle que soit sa dénomination, doit alors être appréhendée dans sa globalité et dans son histoire. Une histoire qui, comme beaucoup d’autres, est marquée par la Révolution, qui va influencer le XIXe et le XXe siècles, et imposer un certain « prototype français » de tribunal politique. Ces Hautes Cours se voient confier des compétences spéciales : ratione personae et ratione materiae. À raison des personnes, il s’agit de juger des personnalités politiques et, dès la Révolution, on entrevoit la difficulté de le faire avec un droit criminel, qui n’est guère adapté à la résolution de différends politiques. Enfin, une Haute Cour est aussi un tribunal des grands crimes politiques, c’est-à-dire des graves atteintes à la souveraineté. Il s’agit dès lors de retracer l’histoire du « Tribunal suprême » français afin de faire apparaître le concept même de justice politique, dans toute sa nudité, comme une aporieAt first glance, the title refers to the judicial activity of the Cour des pairs (1814-1848) and the Senate of the Third Republic (1875-1940). These are the most striking involvements of French legislative bodies in rendering justice. The trials of the ending Restauration ministers, and the one of Louis Malvy seem to be well known, but in reality these are only imperfectly so. In both cases, the upper house has turned away from its initial mission of legislator and supervisor of the government to transform itself, in a very incomplete way, into criminal courts. However, study only these two cases is not enough to define the mission of a parliamentary jurisdiction. The concept of Haute Cour de justice must therefore be understood in its entirety and in its history. A history which, like many others, is marked by the Revolution, which will influence the 19th and 20th centuries, and set a French prototype of political court. These Hautes Cours possess special competencies: ratione personae et ratione materiae. They judge politicians, but since the Revolution one foresees the difficulty of doing so with criminal law, which is hardly suited to the resolution of political disputes. Finally, the French Haute Cour is also a tribunal for major political crimes, namely, serious attacks on sovereignty. It is thereforce a question of recount the history of the “Tribunal supreme” in order to reveal the concept of political justice as an aporia
45
Quinart, Emilien. "L'émancipation du pouvoir réglementaire (1914-1958)." Electronic Thesis or Diss., Université de Lille (2018-2021), 2019. https://buadistant.univ-angers.fr/login?url=https://bibliotheque.lefebvre-dalloz.fr/secure/isbn/9782247210275.
Full textAbstract:
La République parlementaire s’enracine, à la fin du XIXe siècle, dans l’exaltation des principes de 1789 et le rejet du pouvoir personnel. Dans cet idéal, le pouvoir réglementaire fait figure de hantise. Il n’est admis qu’à condition d’être étroitement subordonné à la loi. Au XXe siècle, cette situation change. Les guerres et les crises économiques, financières ou sociales sont à l’origine d’une mutation profonde des activités de l’Etat, qui bouleversent l’exercice des fonctions de législation et heurtent les idéaux républicains. Cette étude entend démontrer comment, entre 1914 et 1958, l’Exécutif retrouve un pouvoir réglementaire non réductible à l’exécution des lois. Né d’un dérèglement des pratiques, et des violations (souvent assumées) des textes constitutionnels, ce processus d’émancipation se trouve progressivement – sous l’influence de la doctrine universitaire et des sections administratives du Conseil d’Etat – rapatrié sous l’empire du droit. Sur la période considérée, la législation gouvernementale apparaît effectivement nécessaire à la sauvegarde et à la continuité de l’Etat. Elle acquiert alors un fondement autonome et gagne en discrétionnalité. Sous les IIIe et IVe Républiques déjà, l’exécution des lois ne justifie plus l’existence et ne définit plus l’étendue du pouvoir réglementaire. Les innovations – supposées – de la Constitution de 1958 doivent donc être relativisées. Loin d’innover, le dispositif des articles 16, 21, 34, 37, 38, 41 et 92 du texte constitutionnel de la Ve République formalise, et systématise, les acquis du droit constitutionnel antérieurAt the end of the 19th century, the Parliamentary Republic took root by exalting the principles of 1789 French Revolution and rejecting personal power. Following this ideal, the Executive’s power to make regulations is dreaded – only allowed when strictly subordinate to the law supremacy. In the 20th century, the situation has changed. Wars and crises caused an essential transformation of the activities of the State, which disturbed the exercise of legislative functions and republican ideals. This thesis aims to explain how, between 1914 and 1958, the Executive Branch recovered a power to make regulations, that exceeds the mere implementation of legislation. The data show that this emancipation process stemmed from both disruption of practices and constitutional violations, gradually establishing a new law – thanks to the influence of law professors and advisory departments of the Conseil d’Etat. This dynamic relied on the need for Executive regulation to protect the security and the continuity of the State. Progressively, that kind of regulation got an autonomous constitutional basis, and the Executive enjoyed an increased level of discretion to enact it. The result is that, already under the Third and Fourth French Republics, the implementation of legislation no longer defined the source and the scope of the power to make regulations. Finally, these findings allow to challenge the current understanding of the Constitution of the Fifth Republic : the articles 16, 21, 34, 37, 38, 41 and 92 should no longer be considered as “innovations”, but only as a formalisation and a systematisation what previous constitutional law introduced
46
Van, Rooijen Lorijn. "Une approche combinatoire du problème de séparation pour les langages réguliers." Thesis, Bordeaux, 2014. http://www.theses.fr/2014BORD0229/document.
Full textAbstract:
Le problème de séparation pour une classe de langages S est le suivant : étant donnés deux langages L1 et L2, existe-t-il un langage appartenant à S qui contient L1, en étant disjoint de L2 ? Si les langages à séparer sont des langages réguliers, le problème de séparation pour la classe S est plus général que le problème de l'appartenance à cette classe, et nous fournit des informations plus détaillées sur la classe. Ce problème de séparation apparaît dans un contexte algébrique sous la forme des parties ponctuelles, et dans un contexte profini sous la forme d'un problème de séparation topologique. Pour quelques classes de langages spécifiques, ce problème a été étudié en utilisant des méthodes profondes de la théorie des semigroupes profinis.Dans cette thèse, on s'intéresse, dans un premier temps, à la décidabilité de ce problème pour plusieurs sous-classes des langages réguliers. Dans un second temps, on s'intéresse à obtenir un langage séparateur, s'il existe, ainsi qu'à la complexité de ces problèmes.Nous établissons une approche générique pour prouver que le problème de séparation est décidable pour une classe de langages donnée. En utilisant cette approche, nous obtenons la décidabilité du problème de séparation pour les langages testables par morceaux, les langages non-ambigus, les langages localement testables, et les langages localement testables à seuil. Ces classes correspondent à des fragments de la logique du premier ordre, et sont parmi lesclasses de langages réguliers les plus étudiées. De plus, cette approche donne une description d'un langage séparateur, pourvu qu'il existeThe separation problem, for a class S of languages, is the following: given two input languages, does there exist a language in S that contains the first language and that is disjoint from the second langage ?For regular input languages, the separation problem for a class S subsumes the classical membership problem for this class, and provides more detailed information about the class. This separation problem first emerged in an algebraic context in the form of pointlike sets, and in a profinite context as a topological separation problem. These problems have been studied for specific classes of languages, using involved techniques from the theory of profinite semigroups.In this thesis, we are not only interested in showing the decidability of the separation problem for several subclasses of the regular languages, but also in constructing a separating language, if it exists, and in the complexity of these problems.We provide a generic approach, based on combinatorial arguments, to proving the decidability of this problem for a given class. Using this approach, we prove that the separation problem is decidable for the classes of piecewise testable languages, unambiguous languages, and locally (threshold) testable languages. These classes are defined by different fragments of first-order logic, and are among the most studied classes of regular languages. Furthermore, our approach yields a description of a separating language, in case it exists
47
Kaděrka, Petr. "Systém pro zobrazování černobílých snímků v nepravých barvách (Pseudocolor)." Master's thesis, Vysoké učení technické v Brně. Fakulta elektrotechniky a komunikačních technologií, 2008. http://www.nusl.cz/ntk/nusl-217184.
Full textAbstract:
This diploma thesis treats the possibilities of the black-white picture depiction in pseudo colors (Pseudocolor). The individual methods, software or hardware are described there and the detailed block scheme of the system Pseudocolor is suggested. The block scheme is created on the basis of gained theoretical knowledge. In the thesis, individual functional blocks of the scheme are described and their circuit designs are realized. Some of the functional blocks are simulated by the PSpice program and accompanied by corresponding signal process data. The suitable choice of the active and passive components is performed, from which the general integration of the system Pseudocolor is made. All the source materials for the realization of the device are given there – double-sided drawing of the printed circuit, layout and specification of the components.
48
Hou, Zhe. "Labelled sequent calculi and automated reasoning for assertions in separation logic." Phd thesis, 2015. http://hdl.handle.net/1885/155766.
Full textAbstract:
Separation logic (SL) is an extension of Hoare logic to reason about programs with mutable data structures. This thesis studies automated reasoning for the assertional language (i.e., formulae that represent pre- and post-conditions) of separation logic. We start from the core of separation logic called Boolean BI (BBI), then consider various propositional abstract separation logics (PASLs) as extensions of BBI. These logics are "abstract" because they are independent of any particular concrete memory model. Finally, we look at separation logic with Reynolds's heap model semantics. We first try to capture BI logics using nested sequents, our design has a special structure of interleaving additive and multiplicative nested sequents. We discover that this nested structure causes much complication when considering the rules for transferring information between nested sequents. Then we change the angle to solve this problem by using labelled sequents. We present a labelled sequent calculus LS_BBI for BBI, the calculus is simple, sound, complete, and enjoys cut-elimination. We show that all the structural rules in LS_BBI can be localised around applications of certain logical rules, based on which we demonstrate a free variable calculus that deals with the structural rules lazily in a constraint system. We propose a heuristic method to quickly solve certain constraints, and show some experimental results to confirm that our approach is feasible for proof search. Based on LS_BBI, we develop a modular proof theory for various PASLs using cut-free labelled sequent calculi. We first extend LS BBI to handle Calcagno et al.'s original logic of separation algebras by adding rules for partial-determinism and cancellativity. We prove the completeness of our calculus via an intermediate calculus that enables us to construct counter-models from the failure to find a proof. We then capture other PASLs by adding rules for other properties in separation theory. We present a theorem prover based on our labelled calculi for these logics. For concrete heap semantics, we consider Reynolds's SL with all logical connectives but without arbitrary predicates. This logic is not recursively enumerable but is very useful in practice. We give a sound labelled sequent calculus LS_SL for this logic. We illustrate the subtle deficiencies of some existing proof calculi for SL, and show that our rules repair these problems. We extend LS SL with rules for linked lists and binary trees, giving a sound, complete and terminating proof system for a popular fragment called symbolic heaps. Our prover shows comparable results with Smallfoot on valid formulae and on formulae extracted from program verification examples, but it is not competitive on large invalid formulae. However, our prover handles the largest fragment of logical connectives in SL.
49
Saravia, Andrés Román. "Cálculo de tableaux para fórmulas elementales en lógicas de separación." Bachelor's thesis, 2020. http://hdl.handle.net/11086/15302.
Full textAbstract:
Tesis (Lic. en Cs. de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2020.En este trabajo final investigamos métodos computacionales de razonamiento para lenguajes modales dinámicos. Por lenguajes dinámicos nos referimos a formalismos que permitan cambiar la estructura subyacente a medida que se evalúa una fórmula. En particular, estudiaremos lenguajes que combinan operadores de la lógica modal, con operadores dinámicos de las lógicas de separación llamados lógicas modales de separación (MSL). Nos centraremos en el desarrollo de un cálculo de tableaux etiquetado para una lógica que combina el operador modal <> clásico, la conjunción de separación * y la constante 'emp'. Para dicho desarrollo, nos basaremos en las llamadas 'fórmulas elementales', un conjunto de fórmulas que describen propiedades básicas sobre la estructura de los modelos, y que son más fáciles de manipular. Gracias a que el lenguaje de las fórmulas elementales es lógicamente equivalente a la MSL mencionada antes, el cálculo obtenido es también completo para esta lógica.
In this work we investigate computational reasoning methods for dynamic modal languages. By dynamic languages we mean formalisms that allow the underlying structure to change as a formula is being evaluated. In particular, we will study languages that combine operators from modal logic with operators from separation logic. The obtained family of logics is called modal separation logic (MSL). We will focus on developing a labeled tableaux calculus for a logic that combines the classic modal <> operator, the conjunction of separation * and the constant 'emp'. This fragment is denoted by MSL(<>,*). For this development, we will base ourselves on the so-called 'elementary formulas', a set of formulas that describe basic properties on the structure of the models. These formulas are easier to manipulate. Since the language of the elementary formulas is logically equivalent to the aforementioned fragment MSL(<>,*), the calculus obtained is also complete for this logic.
Fil: Saravia, Andrés Román. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina.
50
Rearte, Lucas Agustín. "Analizando la forma de estructuras de datos no lineales en memoria dinámica con Separation Logic." Bachelor's thesis, 2017. http://hdl.handle.net/11086/5838.
Full textAbstract:
Tesis (Lic. en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2017.Presentamos un shape analysis con garantı́as de terminación para programas que manipulan estructuras de datos no lineales como árboles binarios. El análisis se basa en una ejecución simbólica de los programas sobre estados abstractos compuestos por fórmulas de un conjunto restringido de la Separation Logic. Dada una precondición, calcula automáticamente una postcondición e invariantes concisos para los ciclos del programa. El uso de un nivel de relevancia para las variables según el tipo de manipulación que sufren permite lograr un balance entre precisión y abstracción en las fórmulas. Mostramos los resultados obtenidos por un prototipo que implementa nuestro análisis sobre una variedad de ejemplos.
We present a terminating shape analysis for programs manipulating non- linear data structures such as binary trees. The analysis is based on symbolic execution of programs over abstract states composed by formulæ of a restricted subset of Separation Logic. Given a precondition, it automatically calculates concise postconditions and invariants for program loops. The use of relevan- ce level of program variables depending on the manipulations applied on them gives us a balance between precision and abstraction in the formulæ. We re- port experimental results obtained from running a prototype implementing our analysis on a variety of examples.