IF Papers

General

Tools and Applications II: The IF Toolset.
Marius Bozga, Susanne Graf, Ileana Ober, Iulian Ober and Joseph Sifakis.
In Flavio Corradinni and Marco Bernanrdo, editors, Proceedings of SFM'04 (Bertinoro, Italy), September, 2004
LNCS vol. 3185, Springer-Verlag
[pdf, postscript, slides]

IF-2.0: A validation environment for Component-Based Real-Time Systems.
Marius Bozga, Susanne Graf and Laurent Mounier.
In Ed Brinksma, K.G. Larsen, editors, Proceedings of CAV'02 (Copenhagen, Denmark), July, 2002
LNCS vol. 2404, Springer-Verlag
[postscript, slides]

Automated validation of distributed software using the IF environment.
Marius Bozga, Susanne Graf, and Laurent Mounier.
In Scott D. Stoller and Willem Visser, editors, Workshop on Software Model-Checking, associated with CAV'01 (Paris, France) July 2001
Volume 55 of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers.
[pdf, postscript, slides]

IF: A Validation Environment for Timed Asynchronous Systems.
M. Bozga, J.Cl. Fernandez, L. Ghirvu, S. Graf, J.P. Krimm, L. Mounier.
Proceedings of CAV'00 (Chicago, USA) July 2000
[postscript, slides]

IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems.
M. Bozga, J.Cl. Fernandez, L. Ghirvu, S. Graf, J.P. Krimm, L. Mounier.
Proceedings of FM'99 (Toulouse, France) September 1999.
[postscript, slides]

Real-Time SDL and UML

Model-checking UML models via a mapping to communicating extended timed automata.
Susanne Graf, Ileana Ober and Iulian Ober.
In Susanne Graf and Laurent Mounier, editors, Proceedings of SPIN'04 (Barcelona, Spain), April, 2004.
[pdf, slides]

Timed Extensions for SDL.
M. Bozga, S. Graf, L. Mounier, I. Ober, J-L. Roux, D. Vincent.
Proceedings of SDL-Forum'01 (Copenhagen, Denmark) June 2001.
[postscript, slides]

SDL for Real Time : What is Missing ?
M.Bozga, S.Graf, A. Kerbrat, L. Mounier, I. Ober, D. Vincent.
Proceedings of SAM'00 (Grenoble, France) June 2000.
[postscript, slides]

IF: An Intermediate Representation for SDL and its Applications.
M. Bozga, J.Cl. Fernandez, L. Ghirvu, S. Graf, J.P. Krimm, L. Mounier, J. Sifakis.
Proceedings of SDL-Forum'99 (Montreal, Canada) June 1999.
[postscript, slides]

Verification and Testing

Testing conformance of real-time software by auto;atic generation of observers.
Saddek Bensalem, Marius Bozga, Moez Krichen and Stavros Tripakis.
In Proceedings of RV'04 (Barcelona, Spain), April, 2004
[postscript, slides]

Compositional State Space Generation with Partial Order Reductions for Asynchronous Communicating Systems.
J.P. Krimm, L. Mounier.
Proceedings of TACAS'00 (Berlin Germany) April 2000.
[postscript, slides]

Static Analysis

Using Static Analysis to Improve Automatic Test Generation.
M. Bozga, J.Cl. Fernandez, L. Ghirvu.
Proceedings of TACAS'00 (Berlin, Germany) April 2000.
[postscript, slides].

State Space Reduction based on Live Variable Analysis.
M. Bozga, J.Cl. Fernandez, L. Ghirvu.
Proceedings of SAS'99 (Venetia, Italy) September 1999.
[postscript, slides]

Case Studies

Experiment on Verification of a Planetary Rover Controller
Anahita Akhavan, Saddek BEnsalem, Marius Bozga and Eleni Orfanidou.
In Proceedigs of IWPSS'04 (Darmstadt, Germany), June, 2004.
[pdf, slides]

Model-Checking Ariane-5 Flight Program
M. Bozga, D. Lesens, and L. Mounier.
In Proceedings of FMICS'01 (Paris, France), pages 211-227. INRIA, 2001.
[postscript, slides]

Verification experiments on the MASCARA protocol.
Susanne Graf and Guoping Jia.
In Proceedings of SPIN Workshop '01 (Toronto, Canada) January 2001.
[postscript, slides]