I've been working together with Lydie du
Bousquet, Duncan Clarke, Thierry
Jéron, and Elena Zinovieva on symbolic test
generation. This paper presented at the Integrated
Formal Methods 2000 conference describes the theory of symbolic test
generation. A prototype tool called STG implements the approach. We've used STG to generate and execute symbolic test cases for a simple
smart-card application: the Common
Electronic Purse System (CEPS). We have presented this
paper at the e-Smart 2001
conference. This short one (in TACAS'02) presents the tool.
I've also been doing some work on deductive verification (a simple example: the sliding-window protocol with PVS, FORTE'01) and how to to it more automatically, cf. same protocol using PVS and supplementary decision procedures (TPHOLs'01), and a larger example : the CEPS (VCL'02).
This paper (initially in Formal Methods Europe (FME'02), extended version to appear in Journal of Software Testing, Verification, and Reliability 13(3) : Sept. 2003) is about integrating symbolic test generation with STG and deductive verification with PVS. This one (to appear in Formal Methods (FM'03)) presents a methodology based on compositionality, abstraction, and theorem-proving (PVS), which was successfully applied to verify a quite large specification of an ATM protocol (details here).
In the Vertecs project we are studying the interactions between verification, control synthesis, and test generation . This paper (in French, to appear in Modélisation des systèmes réactifs, MSR'03) presents our initial results, while this one (in English, to appear in 42nd IEEE Conference on Decision and Control (CDC'03)) takes a more general approach.
An upcoming paper (to appear in TestCom'04) shows how to generate conformance test cases directly from a specification and the safety properties that it satisfies. This allows for an automatic, seamless, and sound validation process between safety requirements, operational specifications, and black-box implementations of finite-state systems.
A collaboration with members of the Lande project of Irisa has resulted in
generating a correct-by-construction dataflow analyser for a relevant subset of JavaCard, using the
Coq proof assistant (paper to appear at ESOP'04).