Journal Articles
-
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
-
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
-
François Pessaux. FoCaLiZe: Inside an F-IDE, 1st Workshop on Formal Integrated
Development Environment (F-IDE 2014), Satellite workshop of ETAPS 2014,
Electronic Proceedings in Theoretical in Computer Science 149, pp 64-78. 2014.
Pdf
-
Mathieu Jaume and Théo Laurent. Teaching formal methods and discrete mathematics, 1st Workshop on Formal Integrated Development Environment (F-IDE 2014), Satellite workshop of ETAPS 2014, Electronic Proceedings in Theoretical in Computer Science 149, pp 30-43. 2014.
Pdf
-
ML Dependency Analysis for Assessors.
Philippe Ayrault, Vincent Benayoun, Catherine Dubois and François Pessaux.
SEFM 2012 - Thessaloniki (Greece), October 2012.
Pdf
-
Damien Doligez, Mathieu Jaume and Renaud Rioboo. Development of
secured systems by mixing programs, specifications and proofs in an
object-oriented programming environment. ACM SIGPLAN Seventh Workshop
on Programming Languages and Analysis for Security (PLAS 2012) pages
80-91, ACM Digital Library. 2012. Pdf
-
Mathieu Jaume, and Renaud Rioboo. Développement de systèmes
sécurisés avec l'atelier Focalize. 23èmes Journées
Francophones des Langages Applicatifs (JFLA 2012), 2012.
-
Renaud Rioboo. Compiler les polynômes en FoCaLiZe ? Journée
SSURF, 29th June 2012
Pdf
-
David Delahaye, Catherine Dubois, Pierre-Nicolas
Tollitte. Génération de code fonctionnel certifié
à partir de spécifications dans l'environnement
FoCaLiZe. Journée SSURF, 29th June 2012
Pdf
-
Development of a generic voter under FoCaL.
Philippe Ayrault, Thérèse Hardin and François Pessaux.
In TAP2009 - Zurich, July 2009.
Pdf, 2012.
-
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
-
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
-
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
-
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
-
Philippe Ayrault. Développement de logiciels critiques en
Focalize. Méthodologie et outils pour l'évaluation de
conformité. Thèse de doctorat, April 2011.
Pdf
-
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:
Wednesday, October 1st, 2014 on host dhcpuei9.ensta.fr
by user didou.
Copyright
© 2005 - 2014 INRIA & LIP6, 2012 -
2014 ENSTA ParisTech, all rights reserved.