Model-based verification techniques

Books

  1. 11th International SPIN Workshop on Model Checking of Software, 2004. Susanne Graf, Laurent Mounier (eds.), Lecture Notes in Computer Science, 2004. (more) download

Academic Journals

  1. Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu, Claude Jard, Thierry Jéron, Alain Kerbrat, Pierre Morel, Laurent Mounier. Verification and test generation for the SSCOP protocol. Sci. Comput. Program, 36(1):27-52, 2000. (more) doi pdf
  2. Marius Bozga, Jean-Claude Fernandez, Alain Kerbrat, Laurent Mounier. Protocol Verification with the Aldebaran Toolset. Software Tools for Technology Transfer, 1(1):166-183, December 1997. (more) pdf
  3. Hubert Garavel, Laurent Mounier. Specification and Verification of various Distributed Leader Election Algorithms for Unidirectional Ring Networks. Science of Computer Programming, Special issue on Industrially Relevant Applications of Formal Analysis Techniques. Full version available as INRIA Research Report 2986, 1996. (more) pdf
  4. Jean-CLaude Fernandez, Claude Jard, Thierry Jéron, Laurent Mounier. `On the Fly'' Verification of Finite Transition Systems. Formal Methods in System Design, 1992. (more) pdf

Book Chapters

  1. Marius Bozga, Susanne Graf, Laurent Mounier, Iulian Ober. La bo\^ite à outils IF pour la modélisation et la vérification de systèmes temps réel. In Systèmes temps réel : Techniques de description et de vérification, Vol. 1, Chap. 9, Traité IC2, série Informatique et systèmes d'information, Hermes, Lavoisier, 2006. (more)

International Conferences

  1. Dominique Borrione, Menouer Boubekeur, Laurent Mounier, Marc Renaudin, Antoine Sirianni. Validation of asynchronous circuit specifications using IF/CADP. In IFIP Intl. Conference on VLSI, Darmstadt, Germany, December 2003. (more) pdf
  2. Menouer Boubekeur, Dominique Borrione, Laurent Mounier, Marc Renaudin, Antoine Sirianni. Modelling CHP descriptions in Labelled Transition Systems for an efficient formal validations of asynchronous circuit specifications. In Forum on Specification and Design Language (FDL'03), Frankfurt, Germany, September 2003. (more) pdf
  3. Marius Bozga, Susanne Graf, Laurent Mounier. IF-2.0: A Validation Environment for Component-Based Real-Time Systems. In Proceedings of CAV'02 (Copenhagen, Denmark), K.G. Larsen Ed Brinksma (ed.), LNCS, Volume 2404, Pages 343-348, July 2002. (more) pdf
  4. Marius Bozga, David Lesens, Laurent Mounier. Model-Checking Ariane-5 Flight Program. In Proceedings of FMICS'01 (Paris, France), Pages 211-227, 2001. (more) pdf
  5. Marius Bozga, Susanne Graf, Laurent Mounier. Automated validation of distributed software using the IF environment. In 2001 IEEE International Symposium on Network Computing and Applications (NCA 2001), 2001. (more) pdf
  6. Marius Bozga, Susanne Graf, Laurent Mounier. Automated validation of distributed software using the IF environment. In Workshop on Software Model-checking, associated with CAV 2001, Paris, Scott D. Stoller, Willem Visser (eds.), Electronic Notes in Theoretical Computer Science, Volume 55, July 2001. (more) pdf
  7. Jean-Pierre Krimm, Laurent Mounier. Compositional State Space Generation with Partial Order Reductions for Asynchronous Communicating Systems. In Proceedings of TACAS'00, Pages 266-282, 2000. (more) pdf
  8. Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu, Susanne Graf, Jean-Pierre Krimm, Laurent Mounier, Joseph Sifakis. IF: An Intermediate Representation for SDL and its Applications. In Proceedings of SDL FORUM'99 (Montreal, Canada), R. Dssouli, G. Bochmann, Y. Lahav (eds.), Pages 423-440, June 1999. (more) pdf
  9. Jean-Pierre Krimm, Laurent Mounier. Compositional State Space Generation from Lotos Programs. In Proceedings of TACAS'97 (Tools and Algorithms for the Construction and Analysis of Systems), Enschede, The Netherlands, Ed Brinksma (ed.), LNCS, Extended version with proofs available as Research Report VERIMAG RR97-01, April 1997. (more) pdf
  10. Ghassan Chehaibar, Hubert Garavel, Laurent Mounier, Nadia Tawbi, Ferruccio Zulian. Specification and Verification of the PowerScale Bus Arbitration Protocol: An Industrial Experiment with LOTOS. In Proceedings of the Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification FORTE/PSTV'96 (Kaiserslautern, Germany), Reinhard Gotzhein, Jan Bredereke (eds.), Full version available as INRIA Research Report 2958, October 1996. (more) pdf
  11. J.C. Fernandez, A. Kerbrat, L. Mounier. Symbolic Equivalence Checking. In Proceedings of the 5th Workshop on Computer-Aided Verification (Heraklion, Greece), C. Courcoubetis (ed.), LNCS, Volume 697, June 1993. (more) pdf
  12. Jean-Claude Fernandez, Hubert Garavel, Laurent Mounier, Anne Rasse, Carlos Rodr\'\iguez, Joseph Sifakis. A Toolbox for the Verification of LOTOS Programs. In Proceedings of the 14th International Conference on Software Engineering ICSE'14 (Melbourne, Australia), Lori A. Clarke (ed.), Pages 246-259, May 1992. (more) pdf
  13. Jean-Claude Fernandez, Hubert Garavel, Laurent Mounier, Anne Rasse, Carlos Rodr\'\iguez, Joseph Sifakis. Une boîte à outils pour la vérification de programmes LOTOS. In Actes du Colloque Francophone pour l'Ingénierie des Protocoles CFIP'91 (Pau, France), Omar Rafiq (ed.), Pages 479-500, September 1991. (more) pdf
  14. Jean-Claude Fernandez, Laurent Mounier. A Tool Set for Deciding Behavioral Equivalences. In Proceedings of CONCUR'91 (Amsterdam, The Netherlands), August 1991. (more) pdf
  15. Jean-Claude Fernandez, Laurent Mounier. ``On the Fly'' Verification of Behavioural Equivalences and Preorders. In Proceedings of the 3rd Workshop on Computer-Aided Verification (Aalborg, Denmark), K. G. Larsen (ed.), July 1991. (more) pdf
  16. Jean-Claude Fernandez, Laurent Mounier. Verifying Bisimulations ``On the Fly''. In Proceedings of the 3rd International Conference on Formal Description Techniques FORTE'90 (Madrid, Spain), Juan Quemada, José Manas, Enrique V\'azquez (eds.), November 1990. (more) pdf

Misc

  1. Marius Bozga, Susanne Graf, Laurent Mounier, Iulian Ober. IF Tutorial. Presented at the 9th SPIN'04 Workshop on Model-Checking of Software, Barcelona, Spain, April 2004. (more) pdf