Previous Up Next

Lot 4 : technologie de modélisation

Sous-lot 1 : modélisation compositionnelle

Disponible
  • Vérification compositionnelle des p-automates ps pdf

Les fournitures suivantes sont annulées et compensées par le renforcement du sous-lot 2, contributions LSV F4.2.2 et F4.2.3

  • méthodes de construction des formules quotients dans le cadre étendu
  • méthodes de résolution de contraintes temporelles dans le cadre étendu

Sous-lot 2 : probabilités

Disponible
  • étude de cas d'une modélisation probabiliste d'un système temps réel : vérification du protocole CSMA/CD sous PRISM ps pdf
  • étude de cas d'une modélisation probabiliste d'un système temps réel : Probabilistic Model Checking of the CSMA/CD protocol using PRISM and APMC ps pdf
  • étude de cas d'une modélisation probabiliste d'un système temps réel : Parametric and Probabilistic Verification of Nicollin-Sifakis-Yovine model of the CSMA/CD protocol ps pdf
  • bibliothèques Coq pour les notions probabilistes élémentaires ps pdf
  • stratégies de réécriture probabiliste dans Elan4 ps pdf
  • étude de cas d'une modélisation probabiliste d'un système temps réel : manipulation de backoff dans CSMA/CA ps pdf
  • application d'une méthode de preuve probabiliste pour prouver la terminaison en temps moyen fini du protocole CSMA/CA 802.11b pdf

Sous-lot 3 : complexité en espace et en temps

Disponible
  • un système de preuve enrichi pour le calcul des constructions inductives ps pdf
  • un système d'analyse pour les programmes fonctionnels du premier ordre ps pdf

Les fournitures suivantes sont annulées et compensées par la conception et l'étude du Calcul de Constructions Congruentes, (PCRI et LORIA)

  • un système de preuve enrichi pour le calcul des constructions avec modules et réécriture
  • un système d'analyse pour les programmes fonctionnels du premier ordre avec références avec application aux systèmes à codes mobiles

Disponible
  • un système de preuve enrichi pour le calcul des constructions congruentes ps pdf

Previous Up Next