Besoin Métier
Vous voulez participer à la formalisation en Coq d'un système informatique, afin d'en accroître la sûreté.
Coq pour l'industrie
L'assistant de preuve Coq est un outil de développement formel utilisé dans le cadre académique mais également industriel pour modéliser ou vérifier des programmes. Cette formation de trois jours, orientée vers l'industrie, permet d'initier les apprenants au langage et son écosystème ainsi qu'au développement et à la preuve de programme en utilisant des techniques simples.
Programme de la formation
Introduction
- Présentation de Coq
- Domaines d'application
- Écosystème
- Installation et premiers pas
Le langage fonctionnel
- Le calcul des constructions
- Définitions et commandes
- Arguments implicites
- Sections
- Modules
- Notations
- Documentation
Le langage de preuves
- Définition des propriétés
- Tactiques de base
- Tactiques évoluées
- Le langage Ltac
- L'isomorphisme de Curry-Howard
Cas pratiques
- Un mini langage
- Une politique de contrôle d'accès
OCamlPro
OCamlPro est un bureau d'étude en développement logiciel, créé en 2011 et fort de plus de 20 ingénieurs R&D, avec une expertise unique sur les langages de programmation, aussi bien théorique (plus de 80% de nos ingénieurs ont une thèse en informatique), pratique (participation active au développement de plusieurs compilateurs open-source, prototypage de la blockchain Tezos, etc.), diversifiée (Rust, OCaml, Cobol, Python, Scilab, etc.) et appliquée à de multiples domaines (méthodes formelles, cybersécurité, systèmes distribués, finance, etc.).
Coq pour l'industrie
Durée: 3 jours
Prix: 2500 EUR/pers. HT
Pratique: 50%
Prérequis
- Algorithmique
- Prog. Fonctionnelle
- Mathématiques
Public
- Développeurs
Objectifs Pédagogiques
- Installer Coq
- Programmer en Coq
- Structurer un développement Coq
- Faire des preuves en Coq
- Extraire des programmes
- Produire du matériel certifiable
Indicateurs de résultats
- Note de satisfaction moyenne: 18.5/20
- Taux de réussite: 100%
Version: 14 novembre 2022
Voir les formateurs
Julien Blond (Coq)
Julien est ingénieur R&D chez OCamlPro depuis 2021, après une thèse de doctorat et une longue expérience dans l'industrie. Julien est un développeur OCaml aguérri, mais aussi un expert des méthodes formelles, et en particulier de la vérification et de la certification en utilisant l'assistant de preuve Coq, par exemple pour les Critères Communs en cyber-sécurité.
Informations pratiques
Contact
Vous pouvez nous contacter par le formulaire en haut de page de chaque formation, ou par mail à contact@ocamlpro.com.
Délais d'accès
Nos formations sont organisées à la demande, dans les deux mois suivant la prise de contact. En cas de personnalisation, le délai d'organisation peut être étendu en conséquence, comme négocié au préalable avec les participants.
Modalités d'inscription et déroulement
Nos formations peuvent être réalisées en présentiel ou à distance.
Avant la formation
- Entretien ou questionnaire pour identifier les attentes et besoins.
- Envoi des éléments administratifs : convention, livret d’accueil et règlement intérieur.
- Envoi des ressources et des instructions pour le bon déroulement de la séance.
Pendant la formation
- Le stagiaire se présente à la formation avec son ordinateur personnel.
- Les horaires pour nos formations inter-entreprises
in-situ sont :
- Début de la formation - 9h30
- Pause déjeuner - 12h à 13h
- Fin de la formation - 17h30
- Évaluation tout au long de la formation (mise en situation, quiz, interrogation)
A la fin de la formation
- Remise d’une attestation de formation
- Questionnaire d’auto-évaluation
- Questionnaire de satisfaction permettant d’évaluer la formation
Après la formation
- Questionnaire de satisfaction à froid (à 3 mois de la formation)
Méthodes mobilisées et modalités d'évaluation
Nos formations s'effectuent par groupes d'au plus 10 personnes, avec un ou deux formateurs en fonction de la quantité d'ateliers pratiques inclus dans la formation.
En fonction du niveau des apprenants et de la taille du groupe, plusieurs modalités pédagogiques peuvent être mises en place : ateliers avec exercices pratiques, discussions guidées, le développement collaboratif, etc.
Les formations peuvent inclure des projets à développer en autonomie, avec l'objectif de consolider les connaissances apprises.
Les ressources pédagogiques sont produites par l'équipes OCamlPro en vue des formations. Les documents sont généralement en anglais, mais peuvent être traduits en français à la demande.
L'évaluation des acquis de la formation se fera en séance au travers d'ateliers, d'exercices et/ou de travaux pratiques.
Accessibilité, handicap
Pour toutes nos formations, nous réalisons des études préalables à la formation pour adapter les locaux, les modalités pédagogiques et l’animation de la formation en fonction de la situation de handicap annoncée. Nous sommes à votre écoute pour toute question ou besoin spécifique, contactez-nous à contact@ocamlpro.com
Prises en charge OPCO et CPF
La prise en charge OPCO est possible : OCamlPro a reçu la certification Qualiopi. Les deux conditions suivantes devront alors être réunies :
- la prise en charge doit être totale et couvrir l’ensemble du coût de la formation
- l’accord de prise en charge doit nous parvenir au plus tard 5 jours avant la session de formation
Nos formations ne sont pas qualifiantes ni certifiantes, et ne peuvent donc être prises en charge par le CPF.