Journal Articles
-
Mathieu Jaume and Charles Morisset. Un cadre sémantique pour le
contrôle d'accès.
Technique et Science Informatique, TSI 27(8):951-976, 2008.
Pdf
-
Julien Blond and Charles Morisset. Un moniteur de référence
sûr d'une base de données.
TSI (Technique et Science Informatiques), 2007.
Pdf
-
Mathieu Jaume and Charles Morisset. A formal approach to implement
access control models. Journal of Information Assurance and
Security, Volume 2, pp 137-148. June 2006.
Pdf
- Bibtex
-
Catherine Dubois and Thérèse Hardin and
Véronique Viguié Donzeau Gouge.
Building certified components within FOCAL.
Trends in Functional Programming, Volume 5, pp 33-48. February 2006.
-
David Delahaye, Mathieu Jaume and Virgile Prevosto. Coq, un outil
pour l'enseignement. Une expérience avec les étudiants du DESS
Développement de logiciels sûrs. Technique et Science Informatique, 24(9):1139-1160,
2005. (in French)
Pdf -
Bibtex
-
Thérèse Hardin and Renaud Rioboo. Les Objets des
Mathématiques. RSTI - L'objet, October 2004.
Postscript
- Bibtex
- Virgile Prevosto and Damien Doligez. Algorithms and proof
inheritance in the foc language. Journal of Automated Reasoning,
29(3-4):337-363, December 2002.
Postscript
- Bibtex
Communications, Conference
-
P. Ayrault, M. Carlier, D. Delahaye, C. Dubois, D. Doligez,
L. Habib, T. Hardin, M. Jaume, C. Morisset, F. Pessaux, R. Rioboo and P. Weis.
Trusted Software within FoCaL. C&ESAR 2008 - Trusting Trusted Computing?,
Rennes, December 2008.
Pdf
-
Lionel Habib, Mathieu Jaume and Charles Morisset.
A formal comparison of the Bell & LaPadula and RBAC models.
Fourth International Conference on Information Assurance and Security,
IAS'2008, Naples, Italy, September 2008, IEEE CS Press.
Pdf
-
Matthieu Carlier and Catherine Dubois. Functional Testing in the Focal
environment. In Test and Proof, volume 4966/2008
of LNCS.
Pages 84-98. Springer, 2008.
Pdf
-
Charles Morisset and Anderson Santana de Oliveira.
Automated Detection of Information Leakage in Access Control.
Security and Rewriting Techniques, SecReT 2007.
Pdf
-
Mathieu Jaume and Charles Morisset. Contrôler le contrôle d'accès
: Approches formelles. Approches Formelles dans l'Assistance au
Développement de Logiciels (AFADL'07), Namur (Belgium), June 2007.
Pdf
-
Frédéric Blanqui, Thérèse Hardin and Pierre Weis. On the
implementation of construction functions for non-free concrete data
types. ESOP07 (European Symposium on Programming), LNCS 4421, 2007.
Pdf
-
Eric Jaeger and Catherine Dubois. Why Would You Trust B?.
Conference on Logic Programming Artificial Intelligence and
Reasoning, LPAR 2007, LNCS.
Pdf
-
David Delahaye, Jean-Frédéric
Étienne, and Véronique Viguié Donzeau-Gouge.
Reasoning about Airport Security Regulations using the Focal Environment. In
International Symposium on
Leveraging Applications of Formal
Methods, Verification and
Validation (ISoLA), pages 36--44, Paphos (Cyprus), November
2006.
-
Mathieu Jaume and Charles Morisset. Towards a formal specification
of access control. Workshop on Foundations of Computer Security and
Automated Reasoning for Security Protocol Analysis
(FCS-ARSPA'06),Seattle, August
2006.
Pdf
- Bibtex
-
David Delahaye, Jean-Frédéric
Étienne, and Véronique Viguié Donzeau-Gouge.
Certifying Airport Security Regulations using the Focal Environment. In
Formal Methods (FM), volume
4085 of LNCS, pages 48--63,
Hamilton, Ontario (Canada), August
2006. Springer.
Pdf
-
Thérèse Hardin, Mathieu Jaume and Charles Morisset. Access control
and rewrite systems. Workshop on Security and Rewriting Techniques,
Venice, July
2006
Postscript -
Bibtex
-
David Delahaye, Jean-Frédéric
Étienne, and Véronique Viguié Donzeau-Gouge. Modeling Airport
Security Regulations in Focal. In Regulation Modelling and their Validation &
Verification (REMO2V), pages 806--812, Luxembourg, June
2006. Presses Universitaires de Namu.
-
Julien Blond and Charles Morisset. Formalisation et implantation
d'une politique de sécurité d'une base de données.
Journées Francophones des Langages Applicatifs (JFLA) 2006, Pauillac,
France.
Pdf
- Bibtex
-
Mathieu Jaume and Charles Morisset. Formalisation and
Implementation of Access control models, Information Assurance and
Security IAS, International Conference on Information Technology
ITCC'2005, Las Vegas, NV USA, pp 703-708, IEEE CS Press,
2005.
Postscript
-
Bibtex
-
Virgile Prevosto and Sylvain Boulmé. Proof contexts with late binding.
In Typed Lambda Calculi and Applications, volume 3461 of
LNCS, pages 324-338. Springer, April 2005
Pdf-
Bibtex
-
Virgile Prevosto. Certified mathematical hierarchies: the FoCal
system. in Mathematics,
Algorithms, Proofs, Dagstuhl Seminar Proceedings. IBFI Schloss Dagstuhl,
2005.
Pdf
-
Bibtex
-
Manuel Maarek and Virgile Prevosto. FoCDoC: the documentation
system of FoC. Proceedings of
Calculemus 03. September
2003.
Postscript-
Bibtex
-
Virgile Prevosto and Mathieu Jaume. Making proofs in a hierarchy
of mathematical structures. Proceedings of Calculemus 03. September
2003.
Postscript-
Bibtex
-
Virgile Prevosto, Damien Doligez, and Thérèse Hardin. Algebraic
structures and dependent records. In Sofiène Tahar,
César Muñoz and Víctor Carreño, editors,
Proceedings of TPHOLs 02. Springer-Verlag, August 2002.
Postscript-
Bibtex
-
Stéphane Fechter. An object-oriented model for the certified
computer algebra library. Paper presented at FMOODS 2002 PhD workshop, March
2002.
Postscript-
Bibtex
-
Sylvain Boulmé, Thérèse Hardin, and Renaud Rioboo.
Some hints for polynomials in the Foc project.
In Calculemus 2001 Proceedings, June 2001.
Postscript-
Bibtex
-
Virgile Prévosto. Prototype d'interface utilisateur de la
librairie foc. In
Actes des Journées Francophones des Langages Applicatifs,
2001.
Postscript-
Bibtex
-
Sylvain Boulmé. Opérateurs de raffinement sur les structures
algébriques. In
Actes des Journées Francophones des Langages Applicatifs,
2000.
Postscript-
Bibtex
-
S. Boulmé, T. Hardin, D. Hirschkoff, V. Ménissier-Morain, and
R. Rioboo. On the way to certify computer algebra systems.
In Proceedings of the Calculemus workshop of FLOC'99 (Federated
Logic Conference, Trento, Italie), volume 23 of ENTCS. Elsevier,
1999.
Postscript-
Bibtex
-
S. Boulmé, T. Hardin, and R. Rioboo. Modules, objets et calcul formel.
In Actes des Journées Francophones des Langages Applicatifs,
1999.
Postscript-
Bibtex
PhD/Master Thesis
-
Mathieu Jaume. Descriptions formelles : Comprendre, corriger,
implanter, réutiliser. Application au contrôle
d'accès. Habilitation à Diriger des Recherches, November 2008.
Pdf
-
Charles Morisset. Sémantique des systèmes de
contrôle d'accès. PhD thesis, September 2007.
Pdf
-
Stéphane Fechter. Sémantique des traits orientés objet de
Focal.
Thèse de doctorat, Université Paris 6, Juillet
2005.
Postscript-
Pdf -
Bibtex
-
Virgile Prevosto. Conception et implantation du langage FoC pour le
développement de logiciels certifiés. Thèse de
doctorat, Université
Paris 6, 2003.
Postscript-
Bibtex
- Sylvain Boulmé.
Spécification d'un environnement dédié
à la programmation certifiée de bibliothèques de
Calcul Formel. Thèse de doctorat,
Université Paris 6, 2000.
Postscript-
Bibtex
-
Lionel Habib. Formalisation, comparaison et implantation d'un
modèle de contrôle d'accès à base de
rôles. Master thesis, September 2007.
Pdf
-
Charles Morisset. Formalisation et implantation d'un modèle de
contrôle d'accès dans l'atelier Focal. Rapport de D.E.A.,
Université Paris 6, September 2004.
Postscript-
Bibtex
-
Olivier Bonnet. Implémentation d'un algorithme de PGCD modulaire
au sein du projet FOC. Rapport de stage d'option scientifique, École
Polytechnique, juillet 2003.
-
Jérôme Grandguillot. Réutilisation de preuves: une
étude pour le système foc. rapport de stage de D.E.A,
Université d'Évry Val d'Essone, 2002.
Bibtex
-
Manuel Maarek. Conception d'une librarie OMDoc pour FoC.
Rapport de stage de D.E.A, Université Paris 6, 2002.
-
Violaine Ruffié. Extensions de FOC par Camlp4. Projet de maîtrise,
Université Paris 6, juin 2002.
-
Stéphane Fechter. Une sémantique pour foc. Rapport de
D.E.A., Université Paris 6, September 2001.
Postscript-
Bibtex
-
Manuel Maarek. Ecriture d'un parser pour Foc en Camlp4. Travail
d'initiation à la recherche, Université Paris 6, Juin 2001.
Postscript-
Bibtex
-
Louis Mandel. Factorisation de polynômes sur les corps finis.
Rapport de magistère, Université Paris 6, 2001.
Postscript-
Bibtex
- V. Prevosto. Vers une interface utilisateur pour foc. Rapport
de D.E.A., Université Paris 6, September 2000.
Postscript-
Bibtex
-
S. Boulmé. Vers la spécification formelle d'une preuve d'un
algorithme non trivial de calcul formel. Stage de D.E.A, Université de
Paris 6, 1997.
Postscript-
Bibtex
Research Reports
-
Sylvain Boulmé. Specifying in coq inheritance used in computer
algebra. Research report, LIP6, 2000.
Postscript-
Bibtex
-
Sylvain Boulmé, Thérèse Hardin, and Renaud
Rioboo. Polymorphic data types, objects, modules and functors: is it
too much? Research report, LIP6, 2000.
Postscript-
Bibtex
- Projet FoC. État d'avancement du projet FoC au printemps
1998. Research report, LIP6, June 1998.
Bibtex
Last modification date:
Friday, May 22, 2009 on host deby.inria.fr
by user weis.
Copyright
© 2005 - 2010 INRIA & LIP6, all rights reserved.