Français Anglais
Accueil Annuaire Plan du site
Accueil > Thèmes de recherche > Toutes les équipes > Test Formel et Exploration de Systèmes (ForTesSE)
Présentation
Thèmes de recherche
Equipes
Projets associés
Thèmes
Collaborations
Production
Travailler au LRI
Formation
Informations pratiques
Equipe Test Formel et Exploration de Systèmes (ForTesSE)


L'équipe ForTesSe travaille dans le domaine des méthodes formelles appliquées à la vérification formelle et au test systématique de logiciels.

Composition de l'équipe
  Responsable
    WOLFF Burkhart

  Membres permanents
    GAUDEL Marie-Claude
    LONGUET Delphine
    POIZAT Pascal
    VOISIN FrĂ©dĂ©ric
    WOLFF Burkhart
    ZAIDI Fatiha

  Membres non-permanents
    BENTAKOUK Lina
    FELIACHI Abderrahmane
    KRIEGER Matthias
    OUDINET Johan

Thèmes de recherche
  VĂ©rification
  Test de Logiciels
  Model-Checking
  MĂ©thodes Formelles de GĂ©nie Logiciel

Contrats en cours
  WebMov
  Usine Logicielle
  HOL-TestGen XT

Logiciels et brevets
  Test statistique de programmes C
  Un generateur pour des donnees de test sur base de HOL
  Un systeme de preuve pour UML/OCL
  Un système de preuve pour la MĂ©thode Z
  Random Uniform walK In Automata

Collaborations
  UniversitĂ© d'Evry Val d'Essonne
  Universidad de Malaga
  Ă‰quipe de Logique MathĂ©matique UniversitĂ© Paris Diderot Paris 7

Thèses et habilitabions récentes
  Test Ă  partir de spĂ©cifications axiomatiques
  Contributions au test de logiciel basĂ© sur des spĂ©cifications formelles
  Utilisation des Structures Combinatoires pour le Test Statistique
Séminaires
SMT and Isabelle/HOL, Bat. I INRIA
Sascha Böhme (TU München)
Mer 09 septembre 2009 - 14h00

Testing for Refinement in Circus
Ana Calvacanti
Mer 29 avril 2009 - 14h00

Test Purpose Concretization through Symbolic Action Refinement
Christophe Gaston
Mer 24 septembre 2008 - 14h00

Critères de couverture pour les programmes Lustre
Virginia Papailiopoulou
Mer 09 juillet 2008 - 14h00

Intégration d'une approche de génération de tests fonctionnels dans le processus de développement.
Fabrice Bouquet
Mer 13 février 2008 - 14h00

Test-Sequence Generation with HOL-TestGen, with an Application to Firewall Testing
Burkhart Wolff
Jeu 17 janvier 2008 - 14h30
Résultats majeurs
An Extensible Encoding of Object-oriented Data Models in HOL with an Application to IMP++.
20 octobre 2008
Achim Brucker et Burkhart Wolff. Journal of Automated Reasoning (JAR), 2008.

Exploration Uniforme de très grands modèles
06 novembre 2007
Un nouvel algorithme permet de tirer uniformément des traces dans de très grands modeles de systèmes parallèles.

HOL-Boogie - An Interactive Prover-Backend for the Verified C Compiler
01 février 2010
Sascha Böhme, Michal Moskal, Wolfram Schulte, and Burkhart Wolff. J. Autom. Resoning(JAR),2009.

Model-Based Adaptation of Behavioral Mismatching Components
01 septembre 2008
Carlos Canal, Pascal Poizat and Gwen SalaĂĽn. IEEE Transactions on Software Engineering, 34(4):546-563, 2008.

Proving Fairness and Implementation Correctness of a Microkernel Scheduler
05 mai 2009
Matthias Daum , Jan Dörrenbächer et Burkhart Wolff. Journal of Automated Reasoning (JAR), 2009.

Semantics, Calculi, and Analysis for Object-oriented Specifications.
02 mars 2009
Achim Brucker et Burkhart Wolff. Acta Informatica, 2009.
Logiciels et brevets