Composition de l'équipe
  Responsable
    WOLFF Burkhart

Activités de recherche
  Vérification
  Méthodes Formelles de Génie Logiciel

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
  La generation de tests pour des spécifications de logiciels écrites sous circus
  Test symbolique de services Web composites
  Test Generation and Animation Based on Object-Oriented Specifications

Tests selection for concurrent systems, and traces refinement
Ana Cavalcanti and Marie-Claude Gaudel
Mar. 04 décembre 2012 - 14h30

Conformance relations for testing concurrent systems
Hernán Ponce de León
Ven. 11 mai 2012 - 14h00

Generation of test sequences for web-services in HOL-TestGen
Achim Brucker
Mer. 02 mai 2012 - 14h00

Extending temporal logics in practice: model checking and applications
Radu Mateescu
Jeu. 22 mars 2012 - 10h30

Specifying and Verifying a Self-configuration Protocol for Distributed Applications in the Cloud using LNT and CADP
Gwen Salaün
Lun. 19 mars 2012 - 14h00

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

A new dichotomic algorithm for the uniform random generation of words in regular languages
16 août 2012
Johan Oudinet, Alain Denise, Marie-Claude Gaudel, Theoretical Computer Science (2012), DOI 10.1016/j.tcs.2012.07.025

Adaptation of Service Protocols Using Process Algebra and On-the-Fly Reduction Techniques
08 août 2012
Radu Mateescu, Pascal Poizat, Gwen Salaun. IEEE Transactions on Software Engineering 38(4), 2012.

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

Cubicle: A Parallel SMT-based Model Checker for Parameterized Systems
22 mars 2012
Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout, Fatiha Zaïdi, CAV 2012

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. Journal of Formal Apsects of Computing (FAOC).

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.