Enseignements
Année scolaire 2024/25
Programmation impérative (S1 FISE)
Suivre le lien pour accéder à la page du cours.
Programmation raisonnée (S5)
Sémantique des langages de programmation
- Slides
- 1er TD
- 1er TP
- 2e TD
- 2e TP
- Fichier associé imp.ml
- Annales
Preuve formelle mécanisée
Assembleur/Compilation (S3 FISE)
- Polycopié du cours (mise à jour 2021-22)
- TP1 : Assembleur RISC-V
- La question 7 de l'exercice 1 et l'exercice 2 sont à rendre pour le 10 octobre dans le dépôt asco23-tp1 d'exam.ensiie.fr
- TP2 : De Pseudo Pascal à RISC-V
- TP3 : (Ocaml)lex et (Ocaml)yacc
- Annales
Approches formelles pour la vérification de programmes (Master 2 CNS)
- Transparents
- TP1
- TP2
- Logiciels à installer pour les TPs:
- Glucose, à compiler à partir des sources
- Z3, paquets disponibles sous Debian, Ubuntu, binaires sur GitHub
- Alt-Ergo, à installer de préférence via OPAM, ou utiliser la version en ligne
- CVC5, binaires depuis le site
- E, paquet Homebrew ou à compiler à partir des sources
- Coq, à installer de préférence via OPAM
- Frama-C, à installer de préférence via OPAM
- Annales
Intelligence artificielle (S4 FISA)
Années précédentes
Programmation fonctionnelle (S4 FISA)
- Transparents : concepts de base
- TP n°1
- Transparents : types définis par l'utilisateur, listes
- TP n°2
- Transparents : Arbres binaires de recherche
- TP n°3
- TD n°1
- Transparents : Structures de données
- TP n°4
- Projet
- Devoir maison
Preuve, analyse statique et vérification runtime
Cours du parcours CILS du master d'informatique de Paris-Saclay.
- Polycopié de la première partie du cours : introduction, spécification et preuve.
- Énoncé pour la séance sur
machine
- Les fichiers Coq nécessaires pour résoudre le conflit de versions.
- Exercices vus pendant la séance sur machine:
- swap.c
- sum.c
- max.c
- remainder.c avec le script Coq pour la preuve qu'alt-ergo ne sait pas faire :
- fact.c
Conseils pour installer Frama-C :
- Installer OPAM, par
exemple sous Debian
# apt-get install opam
cf. cette page pour les autres distributions. - Préparer OPAM :
# opam init # opam update
- Installer Frama-C et ses dépendances :
# opam install coqide why3 frama-c
Programmation raisonnée
Démonstration automatique :
Langages et systèmes formels (ILSF)
Projet informatique (S2 2016)
- Énoncé
- Fichiers contenant les tables au format CSV
Programmation impérative avancée (S2 2016)
- Diapos du cours
- TDs/TPs
- Examen final
Cours donnés pour le master IST-IE des universités Henri Poincaré et Nancy 2
Les serveurs (2008-09)
Partie sur la standardisation d'Internet
Voici une liste de RFC qui définissent les protocoles vus en cours. Il n'est pas demandé que vous les compreniez tous en détail, mais vous devriez être capable d'en extraire certaines informations.
- Post Office Protocol : RFC 1939
- Internet Message Access Protocol : RFC 3501
- Simple Mail Transfer Protocol : RFC 5321 (à noter : date d'octobre 2008 !)
- HyperText Transfer Protocol : RFC 2616
Mise en oeuvre de serveurs d'application (2007-08)
- Cours
- TDs
