Recherche
De l'interprétation algorithmique du blason
Preuves et Programmes
Certification et Logiciel critique
- Bruno Pagano, Olivier Andrieu, Thomas Moniot, Benjamin Canou,
Emmanuel Chailloux, Philippe Wang, Pascal Manoury and Jean-Louis
Colaço, Experience Report: Using Objective Caml to Develop
Safety-Critical Embedded Tools in a Certification Framework, In
International Conference on Functional Programming 2009. Proceedings
of the 14th ACM SIGPLAN international conference on Functional
programming, pp. 215-220.
http://doi.acm.org/10.1145/1596550.1596582
- P. Manoury, P. Baufreton, J.-L. Dufour, E. Prun,
E. Chailloux, G. Henry, F. Thibord, Ph. Wang, E. Millon
Certification de l’assemblage de composants AFADL, 2014. (AFADL2014)
- P. Baufreton, E. Chailloux, J.-L. Dufour, G. Henry,
P. Manoury, E. Prun, F. Thibord, P. Wang Compositional
certification: the CERCLES2 project ERTS2, 2014 (ERTSs2014).
Terminaison de fonctions récursives
Le problème étudié est celui de la recherche
automatique de preuve de terminaison de fonctions définies par
un système d'équations récursives.
Nous restreignons la recherche à une certaine classe
d'équations (grossièment : des fonctions définies
par filtrage exhaustif sur ses arguments, sans utilisation du
jocker (caractère _) Nous pouvons définir
alors la notion d'arbre de distribution (grossièment :
un arbre de filtrage dont chaque noeud est interprété
comme l'application d'une règle de récurence structurelle)
-
Automatizing termination proof of recursively
defined functions(P. Manoury, M. Simonot, TCS 135, 1995)
Article un peu,et parfois trop, technique reprenant l'essentiel du
travail de notre thèse.
-
A Users's friendly Syntax to Define Recursive
Functions as Typed lambda-terms (P. Manoury, Proceedings of Type
for Proofs and Programs, LNCS 996, 1995) Ce papier contient une description
plus intuitive de notre méthode de preuve ainsi qu'une
discussion de son application dans le cadre du système d'aide
à la preuve Coq développé à l'INRIA.
Le fichier
Recursive-Definition.ps.gz
contient une brève description de la commande Recursive
Definition implantée en Coq.
-
A family of recursive schemas
(P. Manoury, M. Simonot, INTAS worshop 99, Tbilisi) Nous y proposons une
caractérisation de notre méthode de recherche de preuves
en terme de schémas de définitions. L'algorithme
suggéré par cette caractérisation met en oeuvre
le filtrage du second ordre.
-
P.-L. Begay, P. Manoury, I. Rakotonirina \textit{Une
mesure ordinale pour les preuves de terminaison en Coq} Journées
Francophone des Langages Applicatifs, 2016 (JFLA2016, script COQ).
Le travail de thèse de
Sylvain BARO
a porté sur la Conception et implémentation d'un
systéme d'aide à la spécification et à la
preuve de programmes ML. Il y traite en particulier du
problème de la terminaison.
Etudes de cas
L'art de la preuve de programme assistée par ordinateur a
autant besoin de mise en pratique que d'investigation
théorique. Il existe de multiples systèmes d'aide
à la preuve basés sur divers formalismes : calcul des
prédicats, théorie des types, réécriture,
etc. Ces formalismes induisent autant des particularités des
langage de spécification qu'ils proposent. Leur
intégration dans un systéme d'aide à la preuve
formelle offrent plus ou moins de souplesse dans la conduite ou le
langage de preuve.
Il faut considérer cette diversité comme celle qui existe
dans les langages de programmation. Un langage de spécification
et le systéme de preuve associé ne doivent pas primer
sur les concepts à mettre en oeuvre dans la
modélisation. De même qu'un algorithme n'est pas tout
à fait son implantation, une spécification doit
être conçue à un niveau plus abstrait que celui de
son codage dans tel ou tel formalisme. Par exemple : un
prédicat, un type ou un ensemble sont des notions
similaires. Toute spécification doit pouvoir être
formulée en langue mathématique naturelle avant
d'ètre formalisée pour tel ou tel système
d'aide à la preuve.
-
Preuves et Programmes. Un cas d'école :
preuve de correction de programmes fonctionnels de tris dans le
système Coq (P. Manoury, rapport IBP 96/22, 1996) Ce
rapport contient la description de la spécification et de la
preuve de correction de l'implantation fonctionnelle de divers
algorithmes de tri. Les fonctions de tri sont toutes décrites
en utilisant la clause Recursive Definition Quelques
commentaires sur la notion d'invariant accompagnent les
diverses preuves.
-
Une preuve sous Raffalli's AF2(P. Manoury,
note, 1998) Cette courte note contient la présentation de la preuve
d'un petit théorème du calcul des propositions
formalisée dans le système AF2 développé
par
Christophe RAFFALLI
Ce résultat a été proposé comme
"challenge" lors du workshop sur l'induction de CADE98. Le
résultat proposé est :
On se place dans le fragment du calcul des propositions ne
comprenant que le seul connecteur <-> (l'équivalence) que nous
appellerons "fragment ssi". On a alors que:
si, dans une proposition du fragment ssi, chaque variable
propositionnelle a un nombre pair d'occurences alors cette
proposition est une tautologie.
-
Script de la preuve de correction opérationnelle
de la fonction d'insertion d'un élément dans un tas: préservation de la structure.
Communication aux JFLA 2008: P. Manoury,
Vérification formelle du tri par tas - étude opérationnelle.
Programmation, typage, lambda-calcul
- E. Chailloux, P. Manoury, B. Pagano, Type behind the mirror : a proposal for type
reconstruction at runtime in Type in Compilation, Juin 97, Amsterdam. (TIC97)
- G. Henry, M. Mauny, E. Chailloux, P. Manoury
Typing unmarshalling without marshalling types, ICFP, 2011. (ICFP2011)
- B. P. Serpette, E. Chailloux, P. Manoury
Unification des couleurs dans un lambda-calcul
polychrome Journées Francophone des Langages Applicatifs, 2014 (JFLA2014).
Collaborations ou contrats industriels
- Contrat d'étude: P. Manoury, L. Pierre, Une spécification algébrique du calcul de répartition dans
l'approximant du courant continu, DER-EDF (1997-98).
Preuve développée avec le Larch Prover.
Communication: Toward a joint use of Algebraic Specifications and Program
Syntethis, IASTED international Conference, Artificial Intelligence and Soft
Computing, May 27-30, 1998.
- Rapport d'étude: Vers la modélisation formelle de la spécification SA-RT du système de
[...] en vue de sa sécurisation, Spécification vérifiée en Coq de l'invariant de réglage
du mode automatique, D.R. Renault (1995)
- Rapports d'étude:
- P. Manoury, Correction de la transformation Li->t->LiGF, R&D Servantec-Surlog
(1997)
- P. Manoury, Simplification des programmes normaux, R&D Servantec-Surlog (1997)
- Rapport d'étude: P. Manoury Spécification et preuve d'éléments de Mini MLFI, LEXIFI (2007).
Réalisé avec l'outil PAF! initié par S. Baro.
- Contrat d'étude: E. Chailloux, P. Manoury, B. Pagano, Traçabilité de la compilation et couverture du code O'Caml dans la
perspective DO-178B. Esterel technologies (2008).
TICE
- A. Brygoo et al., Un céderom Pour Scheme, Chacun son entraîneur, un entraîneur pour tous,
Colloque Internationnal sur les T.I.C.E. d'ingénieur et de l'industrie. Nov. 2002.
- Anne Brygoo, Titou Durand, Pascal Manoury, Christian Queinnec,
Michèle Soria Experiment around a training engine IFIP 2002
- World Computer Congress, 2002.
Livres
- E. Chailloux, P. Manoury, B. Pagano, Développement d'applications avec Objective Caml, O'Reilly France, 2000.
- P. Manoury Programmation de doite à gauche, et vice-versa
Paracamplus, 2011.
Page initiale Maison