Français Anglais
Accueil Annuaire Plan du site
Home > Groups > Research groups > Formal Testing and System Exploration (ForTesSE)
Formal Testing and System Exploration (ForTesSE)

Page no more maintained

as of 30 September 2013
please refer to the new team

The research of the ForTesSE team lies at the heart of formal methods, namely their application to the formal verification and systematic test of software systems.

Group Members
  Group leader
    WOLFF Burkhart

Research activities
  Formal Methods for Software Engineering

  "Evry Val d'Essonne" University
  University of Malaga
  Équipe de Logique Mathématique Université Paris Diderot Paris 7

Recent Ph.D. dissertations & faculty habilitations
  Semantics-Based Testing for Circus
  Symbolic Testing of Composite Web Services
  Test Generation and Animation Based on Object-Oriented Specifications

Tests selection for concurrent systems, and traces refinement
Ana Cavalcanti and Marie-Claude Gaudel
4 December 2012 14h30

Conformance relations for testing concurrent systems
Hernán Ponce de León
11 May 2012 14h00

Generation of test sequences for web-services in HOL-TestGen
Achim Brucker
2 May 2012 14h00

Extending temporal logics in practice: model checking and applications
Radu Mateescu
22 March 2012 10h30

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

Translating Z
Petra Malik
21 October 2011 15h00

Freedom Before Commitment – A Lightweight Type System for Object Initialization
Peter Muller
14 October 2011 11h00

Exploiting SMT counterexamples for constraint solving in Isabelle
Matthias Krieger
6 September 2011 14h00

Realizability of Choreographies using Process Algebra Encodings
Gwen Salaün
28 March 2011 15h45

Formal testing of probabilistic processes: Two different perspectives
Manuel Nunez
14 April 2010 14h00

Testing a probabilistic FSM using interval estimation
Iksoon Hwang
18 March 2010 14h00

SMT and Isabelle/HOL, Bat. I INRIA
Sascha Böhme (TU München)
9 September 2009 14h00

Testing for Refinement in Circus
Ana Calvacanti
29 April 2009 14h00

Test Purpose Concretization through Symbolic Action Refinement
Christophe Gaston
24 September 2008 14h00

Critères de couverture pour les programmes Lustre
Virginia Papailiopoulou
9 July 2008 14h00

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

Test-Sequence Generation with HOL-TestGen, with an Application to Firewall Testing
Burkhart Wolff
17 January 2008 14h30

Résultats majeurs

2 March 2009
Achim Brucker and Burkhart Wolff. Acta Informatica, 2009.

A new dichotomic algorithm for the uniform random generation of words in regular languages
16 August 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
8 August 2012

An Extensible Encoding of Object-oriented Data Models in HOL with an Application to IMP++.
20 October 2008
In: Journal of Automated Reasoning (JAR), 2008.

Coverage-biased random explo-ration of large models and application to testing
27 March 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 March 2012

HOL-Boogie - An Interactive Prover-Backend for the Verified C Compiler
1 February 2010
The paper describes a combined proof-environment for verification conditions generated for annotated C using automated and interactive proof techniques.

Model-Based Adaptation of Behavioral Mismatching Components
1 September 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 January 2012
HOL-TestGen is a specification and test case generation environment extending the interactive theorem prover Isabelle/HOL. It allows for unit- sequence- and reactive sequence test in a uniform framework.

One step forward: Linking wireless self-organizing network validation techniques with formal testing approaches
1 January 2011

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

Uniform trace sampling in very large models
6 November 2007
A new algorithm makes it possible to draw traces uniformly at random in very large models of concurrent systems.

Software & patents