Publications of Vlad Rusu

Load the BibTeX file

Academic Journals

1. M. Egea, V. Rusu. Formal Executable Semantics for Conformance in the MDE Framework. Innovations in Systems and Software Engineering, 6:73-81, 2010.
2. Th. Genet, V. Rusu. Equational Approximations for Tree Automata Completion. Journal of Symbolic Computation, 45(5):574-597, May 2010.
3. 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.
4. v. Rusu. Verifying an ATM Protocol Using a Combination of Formal Techniques. Computer Journal, 49(6):710-730, November 2006.
5. 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.
6. 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.
7. V. Rusu. Combining formal verification and conformance testing for validating reactive systems. Journal of Software Testing, Verification, and Reliability, 13(3), September 2003.
8. 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.
9. O Roux, V. Rusu, F. Cassez. Hybrid verifications of reactive programs. Formal Aspects of Computing, 11(4):448-471, 1999.
10. O. Roux, V. Rusu. Translating from GRAFCET to the reactive language ELECTRE. Automatique, Productique et Informatique Industrielle, 28(2):131-158, 1994.

Book Chapters

1. C. Constant, T. Jéron, H. Marchand, V. Rusu. Validation of Reactive Systems. In Modeling and Verification of Real-TIME Systems - Formalisms and software Tools, S. Merz, N. Navet (eds.), Chap. 2, pp. 51-76, Hermès Science, January 2008.
2. C. Constant, T. Jéron, H. Marchand, V. Rusu. Combinaison entre vérification et test pour la validation de systèmes réactifs. In Traité I2C. Systèmes Temps Réel: Techniques de Description et de Vérification - Théorie et Outils, Vol. 1, Chap. 2, pp. 59-88, Hermès Science, 2006.

International Conferences

1. V. Rusu. Combining narrowing and theorem proving for rewriting-logic specifications. In 4th International Conference on Tests and Proofs (Tap'10), LNCS, Volume 6143, Pages 135-150, July 2010.
2. A. Gamatié, V. Rusu, E. Rutten. Operational Semantics of the Marte Repetitive Structure Modeling Concepts for Data-Parallel Applications Design. In 9th International Symposium on Parallel and Distributed Computing (ISPDC'10), Pages 25-32, July 2010.
3. Vlad Rusu. Formal Executable Semantics for Conformance in the MDE Framework. In UML and FM workshop, Rio de Janeiro, Brazil, December 2009.
4. B. Jeannet, T. Jéron, V. Rusu. Model-based test selection for infinite state reactive systems. In Formal Methods of Components and Objects - FMCO 2006, Amsterdam, Netherlands, Revised Lectures, LNCS, Volume 4709, Pages 47-69, 2007.
5. M. Oostdijk, V. Rusu, J. Tretmans, R. de Vries, T. Willemse. Integrating verification, testing, and learning for cryptographic protocols. In Integrated Formal Methods (IFM'07), Lecture Notes in Computer Science, 2007.
6. T. Jéron, H. Marchand, V. Rusu. Symbolic Determinisation of Extended Automata. In 4th IFIP International Conference on Theoretical Computer Science, IFIP book series, Pages 197-212, Stantiago, Chile, August 2006.
7. G. Barthe, J. Forest, D. Pichardie, V. Rusu. Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant. In Functional and LOgic Programming Systems (FLOPS'06), LNCS, Volume 3945, Pages 114-129, Fuji Susono, Japan, April 2006.
8. Vlad Rusu, Hervé Marchand, Thierry Jéron. Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems. In Formal Methods 2005 (FM05), John Fitzgerald, Andrzej Tarlecki, Ian Hayes (eds.), LNCS, Volume 3582, Pages 189-204, July 2005.
9. B. Jeannet, T. Jéron, V. Rusu, E. Zinovieva. Symbolic Test Selection based on Approximate Analysis. In 11th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05), LNCS, Volume 3440, Pages 349-364, Edinburgh (Scottland), April 2005.
10. V. Rusu, H. Marchand, V. Tschaen, T. Jéron, B. Jeannet. From Safety Verification to Safety Testing. In The 16th IFIP International Conference on Testing of Communicating Systems (TestCom04). Volume 2978 of LNCS, Oxford, UK, March 2004.
11. D. Cachera, T. Jensen, D. Pichardie, V. Rusu. Extracting a data flow analyser in constructive logic. In European Symposium on Programming,ESOP'04. Volume 2986 of LNCS, Pages 385-400, February 2004.
12. V. Rusu. Compositional verification of an ATM protocol. In Formal Methods Europe (FME'03), (postscript, and PVS files), 2003.
13. T. Jéron, H. Marchand, V. Rusu, V. Tschaen. Ensuring the conformance of reactive discrete-event systems using supervisory control. In 42nd IEEE Conference on Decision and Control, Hawaii, USA, December 2003.
14. D. Clarke, T. Jéron, V. Rusu, E. Zinovieva. STG: a Symbolic Test Generation tool. In (Tool paper) Tools and Algorithms for the Construction and Analysis of Systems (TACAS'02). Volume 2280 of LNCS, 2002.
15. V. Rusu. Verification using test generation techniques. In Formal Methods Europe (FME'02), 2002. download
16. V. Rusu, E. Zinovieva, D. Clarke. Verifying Invariants More Automatically. In Verification and Computatoiional Logic, VCL'02, 2002. download
17. D. Clarke, T. Jéron, V. Rusu, E. Zinovieva. Automated Test and Oracle Generation for Smart-Card Applications. In International Conference on Research in Smart Cards (e-Smart'01), Volume 2140 of LNCS, Pages 58-70, 2001.
18. D. Clarke, T. Jéron, V. Rusu, E. Zinovieva. STG : A Tool for Generating Symbolic Test Programs and Oracles from Operational Specifications. In Joint 8th European Software Engineering Conference (ESEC) and 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-9), 2001.
19. V. Rusu. Verifying that Invariants are Context-Inductive. In Theorem Proving in Higher-Order Logics (TPHOLs'01),, Category B paper, University of Edinburgh research Report EDI-INF-RR-0046, Pages 337-351, 2001.
20. V. Rusu. Verifying a Sliding-Window Protocol using PVS. In Formal Description Techniques (FORTE'01), Pages 251-266, 2001.
21. S. Bensalem, V. Ganesh, Y. Lakhnech, C. Munoz, S. Owre, H. Russ, J. Rushby, V. Rusu, H. Saidi, N. Shankar, E. Singerman, A. Tiwari. An Overview of SAL. In LFM 2000: Fifth NASA Langley Formal Methods Workshop, Pages 187-196, 2000. download
22. V. Rusu, L. du Bousquet, T. Jéron. An approach to symbolic test generation. In International Conference on Integrating Formal Methods (IFM'00), LNCS 1945, Pages 338-357, November 2000.
23. V. Rusu, E. Singerman. On proving safety properties by integrating static analysis, theorem proving and abstraction. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS'99), LNCS 1579, An improved version appeared as INRIA research report 3726, available at http://www.inria.fr/rrrt/rr-3726.html, Pages 178-192, 1999.
24. T.A. Henzinger, V. Rusu. Reachability verification for hybrid automata. In International Workshop on Hybrid Systems: Computation and Control, LNCS 1386, Pages 190-204, Berkeley, California, USA, 1998.
25. A. Burgueno, V. Rusu. Task-system analysis using slope-parametric hybrid automata. In Proceedings of the European Conference on Parallelism (EuroPar'97) Volume 1300 of LNCS, Pages 1262-1273, Passau (Germany), 1997.
26. V. Rusu. Verifying periodic task-control systems. In International Workshop on Hybrid and Real-Time Systems (HART'97), Volume 1201 of LNCS, Pages 63-69, Grenoble, France, 1997.
27. F. Boniol, A. Burgueno, O. Roux, V. Rusu. Analysis of slope-parametric hybrid automata. In International Workshop on Hybrid and Real-Time Systems (HART'97), Volume 1201 of LNCS, Pages 75-81, Grenoble, France, 1997.
28. O. Roux, V. Rusu. Deciding time-bounded properties for ELECTRE reactive programs with stopwatch automata. In International workshop on Hybrid Systems and Autonomous Control (WHSAC'94), Volume 999 of LNCS, Pages 405-416, Cornell University, Ithaca (New York, USA), 1996.

National Conferences

1. V. Rusu, M. Clavel. Vérification d'invariants pour des systèmes spécifiés en logique de réécriture. In Vingtièmes Journées Francophones des Langages Applicatifs, JFLA 2009, A. Schmitt (ed.), Studia Informatica Universalis, Volume 7.2, Pages 317-350, Saint Quentin sur Isère, France, February 2009.
2. T. Jéron, H. Marchand, V. Rusu, V. Tschaen. Synthèse de contrôleurs pour une relation de conformité. In 4ième Colloque Francophone sur la Modélisation des Systèmes Réactifs, MSR'03, Metz, France, October 2003.

Research Reports

1. V. Rusu, M. Clavel. Theorem proving for Maude's Rewriting Logic. Research Report Irisa, No 1873, 2007.
2. C. Breunesse, E. Hubbers, P. Koopman, W. Mostowski, M. Oostdijk, V. Rusu, R. de Vries, A. van Weelden, R. Wichers Schreur, T. Willemse. Testing the Dutch e-passport. Research Report Radboud University, Nijmegen, The Netherlands, 2006.
3. T. Jéron, H. Marchand, V. Rusu. Symbolic Determinisation of Extended Automata. Research Report IRISA, No 1176, February 2006.
4. D. Pichardie, V. Rusu. Defining and Reasoning About General Recursive Functions in Type Theory: a Practical Method. Research Report Irisa, No 1766, November 2005.
5. B. Jeannet, T. Jéron, V. Rusu, E. Zinovieva. Symbolic test selection using approximate analysis. Research Report IRISA, No 1649, October 2004.
6. V. Rusu, H. Marchand, T. Jéron. Verification and Symbolic Test Generation for Safety Properties. Research Report IRISA, No 1640, August 2004.
7. V. Rusu. Verifying an ATM Protocol Using a Combination of Formal Techniques. Research Report INRIA, No 5089, January 2004.
8. V. Rusu. Analyzing Automata with Presburger Arithmetic and Uninterpreted Function Symbols. Research Report INRIA, No 4100, 2001.
9. V. Rusu, E. Singerman. Interactive abstractions: proving safety property by integrating static analysis, theorem proving, and abstraction. Research Report IRISA, No 1256, July 1999.

Thesis

1. V. Rusu. Formal verification and conformance testing for reactive systems. Habilitation à diriger des recherches Université de Rennes 1, December 2006.
2. V. Rusu. Vérification temporelle de programmes ELECTRE. PhD Thesis Ecole Centrale de Nantes, Laboratoire d'Automatique de Nantes, January 1996.

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