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
[connexion sécurisée]
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
    EL HAMADI Abdelhay
    FELIACHI Abderrahmane
    KHEFIFI Rania
    KRIEGER Matthias
    NGUYEN Huu Nghia
    WENZEL Markus

  Stagiaires
    GABRIEL Roven

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

Contrats en cours
  PIMI
  Paral-ITP

Logiciels et brevets
  AuGuSTe : Test statistique de programmes C
  Isabelle/HOL : Isabelle/HOL
  HOL-TestGen : Un generateur pour des donnees de test sur base de HOL
  HOL-OCL : Un systeme de preuve pour UML/OCL
  Le Système HOL-Z : Un système de preuve pour la MĂ©thode Z
  RUKIA : 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 symbolique de services Web composites
  Test Generation and Animation Based on Object-Oriented Specifications
  Multi-Agent Systems Verification by Means of Simulation Analysis
Séminaires
Translating Z
Petra Malik
Ven. 21 octobre 2011 - 15h00

Freedom Before Commitment – A Lightweight Type System for Object Initialization
Peter Muller
Ven. 14 octobre 2011 - 11h00

Exploiting SMT counterexamples for constraint solving in Isabelle
Matthias Krieger
Mar. 06 septembre 2011 - 14h00

Realizability of Choreographies using Process Algebra Encodings
Gwen SalaĂĽn
Lun. 28 mars 2011 - 15h45

Formal testing of probabilistic processes: Two different perspectives
Manuel Nunez
Mer. 14 avril 2010 - 14h00

Testing a probabilistic FSM using interval estimation
Iksoon Hwang
Jeu. 18 mars 2010 - 14h00

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.

Coverage-biased random explo-ration of large models and application to testing
27 mars 2011
A. Denise, M.-C. Gaudel, S.-D. Gouraud, R. Lassaigne, J. Oudinet S. Peyronnet, STTT: Int. Jal on SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, DOI: 10.1007/s10009-011-0190-1

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.

On Theorem Prover-based Testing
10 janvier 2012
Achim D. Brucker and Burkhart Wolff

One step forward: Linking wireless self-organizing network validation techniques with formal testing approaches
01 janvier 2011
Aline Carneiro Viana, Stephane Maag, Fatiha Zaidi. ACM Computing Surveys (CSUR),Volume 43 Issue 2, January 2011.

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