Výsledky vyhledávání - "Logique de hoare"

Dissertation/ Thesis

Génération de codes et d'annotations prouvables d'algorithmes de points intérieurs à destination de systèmes embarqués critiques

Autor: Davy, Guillaume

Dans l'industrie, l'utilisation de l'optimisation est omniprésente. Elle consiste à calculer la meilleure solution tout en satisfaisant un certain nombre de contraintes. Cependant, ce calcul est complexe, long et pas toujours fiable. C'est pourquoi

Externí odkaz: http://www.theses.fr/2018ESAE0034/document

Zobrazit plný text záznamu

Generation of codes and provable annotations of interior-point algorithms for critical embedded systems

Autor: Davy, Guillaume

Publikováno v: Algorithme et structure de données [cs.DS]. Institut Supérieur de l'Aéronautique et de l'Espace (ISAE), 2018. Français

The objective of this thesis is to contribute to the formal verification of such systems. We will focus in particular on the certification of the compilation of the model to the code. In particular, through the annotation generation at the core of th

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::a6824296e56f47c310543e1591b54a7c
https://hal.archives-ouvertes.fr/tel-02190142

Zobrazit plný text záznamu

Dissertation/ Thesis

Modèles hybrides de réseaux de régulation : étude du couplage des cycles cellulaire et circadien

Autor: Behaegel, Jonathan

La modélisation de systèmes biologiques est devenue indispensable pour comprendre les phénomènes complexes et émergents issus d'influences partiellement connues, et pour envisager de contrôler un système altéré dans le but de restaurer un co

Externí odkaz: http://www.theses.fr/2018AZUR4071/document

Zobrazit plný text záznamu

Dissertation/ Thesis

Hoare-like verification of graph transformation

Autor: Brenas, Jon Haël

En informatique comme dans de multiples autres domaines, les graphes peuvent être trouvés partout. Ils sont utilisés pour représenter des données dans des domaines allant de la chimie à l'architecture, en tant que structures abstraites ou que m

Externí odkaz: http://www.theses.fr/2016GREAM066/document

Zobrazit plný text záznamu

Raisonnement sur les transformations de graphes

Autor: Brenas, Jon Haël

Publikováno v: Information Theory [cs.IT]. Université Grenoble Alpes, 2016. English. ⟨NNT : 2016GREAM066⟩

In computer science as well as multiple other fields, graphs have become ubiquitous. They are used to represent data in domains ranging from chemistry to architecture, as abstract structures or as models of the data or its evolution. In all these dom

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=od______2592::3d3929519b4c7d78bb0564bc0364e277
https://tel.archives-ouvertes.fr/tel-01680448

Zobrazit plný text záznamu

Maximal and Compositional Pattern-Based Loop Invariants

Autor: Yannick Moy, Virginia Aponte, Pierre Courtieu, Marc Sango

Publikováno v: FM 2012: Formal Methods ISBN: 9783642327582
FM

We present a novel approach for the automatic generation of inductive loop invariants over non nested loops manipulating arrays. Unlike most existing approaches, it generates invariants containing disjunctions and quantifiers, which are rich enough f

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::36e54b23d63fe79ad480f8af6a0c77e7
https://hal.archives-ouvertes.fr/hal-01126145

Zobrazit plný text záznamu

Des types aux assertions logiques : preuve automatique ou assistée de propriétés sur les programmes fonctionnels

Autor: Régis-Gianas, Yann

Publikováno v: Programming Languages [cs.PL]. Université paris diderot, 2007. English. ⟨NNT : 2007PA077155⟩

This work studies two approaches to improve the safety of computer programs using static analysis.The first one is typing which guarantees that the evaluation of program cannot fail. The functionallanguage ML has a very rich type system and also an a

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::c7ffbcb73db2a3ca6fb8736662e652ff
https://inria.hal.science/tel-01238703

Zobrazit plný text záznamu

From types to logical assertions : automatic or assisted proofs of property about functional programs

Autor: Régis-Gianas, Yann

Publikováno v: Programming Languages [cs.PL]. Université paris diderot, 2007. English. ⟨NNT : 2007PA077155⟩

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=od_______212::c7ffbcb73db2a3ca6fb8736662e652ff
https://hal.inria.fr/tel-01238703/document

Zobrazit plný text záznamu

Dissertation/ Thesis

Validation formelle des langages à parallélisme de données

Autor: Cachera, David

Le calcul massivement parallèle a connu durant ces deux dernières décennies un fort développement. Les efforts dans ce domaine ont d'abord surtout été orientés vers les machines, plutôt qu'à la définition de langages adaptés au parallélis

Externí odkaz: http://tel.archives-ouvertes.fr/tel-00425390
http://tel.archives-ouvertes.fr/docs/00/42/53/90/PDF/these_finale.pdf

Zobrazit plný text záznamu

Proof of Imperative Programs in Type Theory

Autor: Filliatre, Jean-Christophe

Publikováno v: [Research Report] LIP RR-1997-24, Laboratoire de l'informatique du parallélisme. 1997, 2+20p

Proofs of correctness of imperative programs are traditionally done in first order frameworks derived from Hoare logic~\cite{Hoare69}. On the other hand, correctness proofs of purely functional programs are almost always done in higher order logics.

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::a5f187a8a93c1c4afff912fb06644da2
https://hal-lara.archives-ouvertes.fr/hal-02102043

Zobrazit plný text záznamu

Vyhledávací nástroje:

Upřesnit hledání