Academic Journals


  1. Nathalie Bertrand, Axel Legay, Sophie Pinchinat, Raclet Jean-Baptiste. Modal event-clock specifications for timed component-based design. Science of Computer Programming, 77:1212-1234, 2012. details doi pdf
  2. F. Cassez, J. Dubreil, H. Marchand. Synthesis of Opaque Systems with Static and Dynamic Masks. Formal Methods in System Design, 40(1):88-115, 2012. details doi pdf
  3. Y. Falcone, J-C Fernandez, T. Jéron, H. Marchand, L. Mounier. More Testable Properties. STTT: Software Tools for Technology Transfer, (Extension of the ICTSS'10 paper), 14(2):403-437, 2012. details doi pdf
  4. Y. Falcone, L. Mounier, Fernandez J.-C, J.-L. Richier. Runtime enforcement monitors: composition, synthesis, and enforcement abilities. Formal Methods in System Design, available as online first, 2012. details doi pdf
  5. G. Kalyon, T. Le Gall, H. Marchand, T. Massart. Symbolic Supervisory Control of Infinite Transition Systems under Partial Observation using Abstract Interpretation. Discrete Event Dynamic Systems : Theory and Applications, 22(2):121-161, 2012. details doi pdf
  6. Philippe Darondeau, Stephane Demri, Roland Meyer, Christophe Morvan. Petri Net Reachability Graphs: Decidability Status of First Order Properties. Logical Methods in Computer Science, 8(4):1-28, October 2012. details doi pdf
  7. C. Baier, M. Grösser, N. Bertrand. Probabilistic w-automata. Journal of the ACM, 59(1), February 2012. details doi


  1. G. Kalyon, T. Le Gall, H. Marchand, T. Massart. Decentralized Control of Infinite Systems. Discrete Event Dynamic Systems : Theory and Applications, 21(3):359-393, September 2011. details doi pdf


  1. M. Egea, V. Rusu. Formal Executable Semantics for Conformance in the MDE Framework. Innovations in Systems and Software Engineering, 6:73-81, 2010. details doi pdf
  2. J. Dubreil, Ph. Darondeau, H. Marchand. Supervisory Control for Opacity. IEEE Transactions on Automatic Control, 55(5):1089-1100, May 2010. details doi
  3. Th. Genet, V. Rusu. Equational Approximations for Tree Automata Completion. Journal of Symbolic Computation, 45(5):574-597, May 2010. details doi pdf


  1. Eric Rutten, Hervé Marchand. Automatic generation of safe handlers for multi-task systems. Journal of Embedded Computing, 3(4):255-276, 2009. details doi pdf


  1. J. Komenda, J. van Schuppen, B. Gaudin, H. Marchand. Supervisory Control of Modular Systems with Global Specification Languages. Automatica, 44(4):1127-1134, April 2008. details doi pdf


  1. B. Gaudin, H. Marchand. An Efficient Modular Method for the Control of Concurrent Discrete Event Systems: A Language-Based Approach. Discrete Event Dynamic System, 17(2):179-209, 2007. details doi pdf
  2. C. Constant, T. Jéron, H. Marchand, V. Rusu. Integrating formal verification and conformance testing for reactive systems. IEEE Transactions on Software Engineering, 33(8):558-574, August 2007. details doi pdf
  3. S. Pickin, C. Jard, T. Jéron, J-M Jézéquel, Y. Le Traon. Test Synthesis from UML Models of Distributed Software. IEEE Transactions on Software Engineering, 33(4):252-269, April 2007. details doi pdf


  1. T. Le Gall, B. Jeannet, H. Marchand. Contrôle de systèmes symboliques, discrets ou hybrides. Technique et Science Informatiques (TSI), 25(3):293-319, 2006. details doi pdf
  2. v. Rusu. Verifying an ATM Protocol Using a Combination of Formal Techniques. Computer Journal, 49(6):710-730, November 2006. details doi


  1. D. Cachera, T. Jensen, D. Pichardie, V. Rusu. Extracting a data flow analyser in constructive logic. Theoretical Computer Science, 342(1):56-78, September 2005. details doi pdf


  1. B. Gaudin, H Marchand. Supervisory Control of Product and Hierarchical Discrete Event Systems. European Journal of Control, Special issue of European Control Conference, ECC 2003, 10(2), 2004. details doi pdf
  2. T. Jéron, H. Marchand, V. Rusu, V. Tschaen. Ensuring the conformance of reactive discrete-event systems by means of supervisory control. International Journal of Production Research, 42(14):2809-2826, 2004. details doi pdf
  3. N. Bertrand, I. Charon, O. Hudry, A. Lobstein. Identifying and Locating-Dominating Codes on Chains and Cycles. European Journal of Combinatorics, 25(7):969-987, October 2004. details download pdf
  4. C. Jard, T. Jéron. TGV: theory, principles and algorithms, A tool for the automatic synthesis of conformance test cases for non-deterministic reactive systems. Software Tools for Technology Transfer (STTT), 6, October 2004. details pdf


  1. V. Rusu. Combining formal verification and conformance testing for validating reactive systems. Journal of Software Testing, Verification, and Reliability, 13(3), September 2003. details
  2. B. Jeannet. Dynamic Partitioning In Linear Relation Analysis. Application To The Verification Of Reactive Systems. Formal Methods in System Design, available at, 23(1):5-37, July 2003. details


  1. T. Jéron. TGV: théorie, principes et algorithmes. Techniques et Sciences Informatiques, numéro spécial Test de Logiciels, (21), 2002. details
  2. H. Marchand, O. Boivineau, S. Lafortune. On Optimal Control of a class of partially-Observed Discrete Event Systems. Automatica, 38(11):1935-1943, October 2002. details doi pdf


  1. V. Rusu, E. Zinovieva. Analyzing Automata with Presburger Arithmetic and Uninterpreted Function Symbols. Electronic Notes in Theoretical Computer Science, To appear also in proc. ICALP 2001 Workshop on Verification of Parameterized Systems (VEPAS'01), 50(4), 2001. details
  2. H. Marchand, E. Rutten, M. Le Borgne, M. Samaan. Formal Verification of programs specified with SIGNAL : Application to a Power Transformer Station Controller. Science of Computer Programming, 41(1):85-104, August 2001. details doi pdf


  1. C. Jard, T. Jéron. An educational case study in protocol verification and distributed observation. Journal of Computer Science Education, ECASP Special Issue, 10(3), 2000. details ps
  2. H Marchand, O. Boivineau, S. Lafortune. On the Synthesis of Optimal Schedulers in Discrete Event Control Problems with Multiple Goals. SIAM Journal on Control and Optimization, 39(2):512-532, 2000. details doi pdf
  3. H. Marchand, P. Bournai, M. Le Borgne, P. Le Guernic. Synthesis of Discrete-Event Controllers based on the Signal Environment. Discrete Event Dynamic System: Theory and Applications, 10(4):325-346, October 2000. details doi pdf
  4. H. Marchand, M. Samaan. Incremental Design of a Power Transformer Station Controller using Controller Synthesis Methodology. IEEE Transaction on Software Engineering, 26(8):729-741, August 2000. details doi pdf
  5. S. Ramangalahy, P. Le Gall, T. Jéron. Une application de la théorie des jeux au test de conformité. Revue Electronique sur les Réseaux et l'Informatique Répartie (RERIR), 9(0):3-23, May 2000. details ps
  6. Y. Le Traon, T. Jéron, J.-M. Jézéquel, P. Morel. Efficient OO Integration and Regression Testing. IEEE Transactions on Reliability, 49(1):12-25, March 2000. details
  7. M. Bozga, J.-C. Fernandez, L. Ghirvu, C. Jard, T. Jéron, A. Kerbrat, P. Morel, L. MounierS. Gnesi, J. R. Cuellor, D. Latella. Verification and test generation for the SSCOP protocol. Journal of Science of Computer Programming, special issue on Formal Methods in Industry, 36(1):27-52, January 2000. details pdf


  1. O Roux, V. Rusu, F. Cassez. Hybrid verifications of reactive programs. Formal Aspects of Computing, 11(4):448-471, 1999. details
  2. T. Jéron, C. Jard, C. Viho, B. Caillaud, H. Kahlouche, P. Morel, J.-C. Fernandez, A. Kerbrat, M. Bozga. Génération automatique de tests pour les protocoles: l'exemple de l'approche formelle de TGV. Revue de l'Electricité et de l'Eléctronique (REE), 3, March 1999. details


  1. H. Ben-Abdallah, J.Y. Choi, D. Clarke, Y.S. Kim, I. Lee. A Process Algebraic Approach to the Schedulability Analysis of Real-Time Systems. Real-Time Systems, 15(3):189-219, November 1998. details
  2. E. Marchand, E. Rutten, H. Marchand, F. Chaumette. Specifying and verifying active vision-based robotic systems with the Signal environment. Int. Journal of Robotics Research, 17(4):418-432, April 1998. details doi pdf


  1. J.-C. Fernandez, C. Jard, T. Jéron, G. Viho. An Experiment in Automatic Generation of Conformance Test Suites for Protocols with Verification Technology. Science of Computer Programming, 29:123-146, 1997. details download


  1. O. Roux, V. Rusu. Translating from GRAFCET to the reactive language ELECTRE. Automatique, Productique et Informatique Industrielle, 28(2):131-158, 1994. details


  1. T. Jéron, C. Jard. Testing for Unboundedness of Fifo Channels. Theoretical Computer Science, 113:93-117, 1993. details ps


  1. J.-C. Fernandez, C. Jard, T. Jéron, L. Mounier. On-the-fly Verification of Finite Transition Systems. Formal Methods in System Design, 1(2):251-273, 1992. details

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
This page is automatically generated by bib2html v216, © INRIA 2002-2007, Projet Lagadic

| VerTeCs | Team | Publications | New Results | Softwares |
Irisa - Inria - Copyright 2005 © Projet VerTeCs