A Quest for Exactness: Program Transformation for Reliable Real Numbers

A Quest for Exactness: Program Transformation for Reliable Real Numbers

Cette thèse présente un algorithme qui élimine les racines carrées et les divi- sions dans des programmes sans boucles, utilisés dans des systèmes embarqués, tout en préservant la sémantique. L'élimination de ces opérations permet d'éviter les erreurs d'arrondis à l'...

Full description

Bibliographic Details
Main Author:	Neron, Pierre
Language:	ENG
Published:	Ecole Polytechnique X 2013
Subjects:	[INFO:INFO_PL] Computer Science/Programming Languages [INFO:INFO_PL] Informatique/Langage de programmation [INFO:INFO_LO] Computer Science/Logic in Computer Science [INFO:INFO_LO] Informatique/Logique en informatique [INFO:INFO_FL] Computer Science/Formal Languages and Automata Theory [INFO:INFO_FL] Informatique/Théorie et langage formel Program Transformation Real Number arithmetic Anti-unification Semantics of Programming Languages Proof Assistant Embedded Systems Quantifier Elimination
Online Access:	http://tel.archives-ouvertes.fr/tel-00924379 http://tel.archives-ouvertes.fr/docs/00/92/43/79/PDF/these.pdf

Similar Items

Spécification et vérification de propriétés quantitatives : expressions, logiques et automates
by: Monmege, Benjamin
Published: (2013)

Conception d'un noyau de vérification de preuves pour le λΠ-calcul modulo
by: Boespflug, Mathieu
Published: (2011)

Propriétés structurelles et calculatoires des pavages
by: Jeandel, Emmanuel
Published: (2011)

Conception et implantation d'un modèle de raisonnement sur les contextes basée sur une théorie des types et utilisant une ontologie de domaine
by: Barlatier, Patrick
Published: (2009)

Etude de la compilation des langages logiques de programmation par contraintes sur les domaines finis: le système clp(FD)
by: Diaz, Daniel
Published: (1995)

Syntaxe et modèles d'une composition non-associative des programmes et des preuves
by: Munch-Maccagnoni, Guillaume
Published: (2013)

Les objets en C++ : sémantique formelle mécanisée et compilation vérifiée
by: Ramananandro, Tahina
Published: (2012)

Modèles d'automates d'arbres étendus pour la vérification de systèmes infinis
by: Jacquemard, Florent
Published: (2011)

Jeux de typage et analyse de lambda-grammaires non-contextuelles
by: Bourreau, Pierre
Published: (2012)

Efficient verification of sequential and concurrent systems
by: Schwoon, Stefan
Published: (2013)

Concurrency in Real-Time Distributed Systems, from Unfoldings to Implementability
by: Chatain, Thomas
Published: (2013)

Development and verification of probability logics and logical frameworks
by: Maksimovic, Petar
Published: (2013)

Développement et Vérification des Logiques Probabilistes et des Cadres Logiques
by: Maksimovic, Petar
Published: (2013)

Tree automata, approximations, and constraints for verification : Tree (Not quite) regular model-checking
by: Hugot, Vincent
Published: (2013)

Automates d'ordres : théorie et applications
by: Hélouët, Loïc
Published: (2013)

Verification based on unfoldings of Petri nets with read arcs
by: Rodríguez, César
Published: (2013)

Développement modulaire de théories et gestion de l'espace de nom pour l'assistant de preuve Coq.
by: Soubiran, Elie
Published: (2010)

Complexité Implicite de Lambda-Calculs Concurrents
by: Madet, Antoine
Published: (2012)

Approche langage au développement logiciel : application au domaine des systèmes d'informatique ubiquitaire
by: Mercadal, Julien
Published: (2011)

Coercions effaçables : une approche unifiée des systèmes de types
by: Cretin, Julien
Published: (2014)

Amélioration des processus de vérification de programmes par combinaison des méthodes formelles avec l'ingénierie dirigée par les modèles
by: Fernandes Pires, A.
Published: (2014)

Développement et vérification des logiques probabilistes et des cadres logiques
by: Maksimović, Petar
Published: (2013)

De nouveaux outils pour calculer avec des inductifs en Coq
by: Boutillier, Pierre
Published: (2014)

Un environnement de simulation pour la validation de spécifications B événementiel
by: Yang, Faqing
Published: (2013)

Ambiguity Detection for Programming Language Grammars
by: Basten, Bas
Published: (2011)

Application-Level Virtual Memory for Object-Oriented Systems
by: Martinez Peck, Mariano
Published: (2012)

ArCo : une Architecture informatique pour un Compagnon Artificiel en interaction avec un utilisateur
by: Jost, Céline
Published: (2013)

Asynchronous Process Calculi for Specification and Verification of Information Hiding Protocols
by: Beauxis, Romain
Published: (2009)

A VPA-based Aspect Language
by: Nguyen, Dong Ha
Published: (2011)

Supporting Integration Activities in Object-Oriented Applications
by: Uquillas-Gomez, Verónica
Published: (2012)

Exploiting Model Structure in CEGAR Verification Method
by: Chucri, Farès
Published: (2012)

Le Débogage à Distance et la Réflexion dans les Dispositifs à Ressources Limitées
by: Papoulias, Nikolaos
Published: (2013)

POLYMORPHISME PARAMTRIQUE POUR LE TRAITEMENT DE DOCUMENTS XML
by: Xu, Zhiwu
Published: (2013)

CONTRIBUTION A LA SPÉCIFICATION DES SYSTÈMES TEMPS RÉELS : L'APPROCHE UML/PNO
by: Delatour, Jérôme
Published: (2003)

Analyse statique par interprétation abstraite de programmes concurrents
by: Miné, Antoine
Published: (2013)

Automatisation de la Certification Formelle de Systèmes Critiques par Instrumentation d'Interpréteurs Abstraits
by: Garnacho, Manuel
Published: (2010)

Le point de vue epistémique de théorie de la concurrence
by: Knight, Sophia
Published: (2013)

Techniques de déduction automatique vues comme recherche de preuve en calcul des séquents
by: Farooque, Mahfuza
Published: (2013)

Type Systems for Distributed Programs: Components and Sessions
by: Dardha, Ornela
Published: (2014)

Terminaison des systèmes de réécriture d'ordre supérieur basée sur la notion de clôture de calculabilité
by: Blanqui, Frédéric
Published: (2012)