@TechReport{rc07, 
	Author = {Rusu, V. and Clavel, M.},
	Title = {Theorem proving for Maude's Rewriting Logic},
	Number = {1873},
	Institution = {Irisa},
	Year = {2007}
} 


@article{ieee-tse, 
	Author = {Constant, C. and Jéron, T. and Marchand, H. and Rusu, V.},
	Title = {Integrating formal verification and conformance testing for reactive systems},
	Journal = {IEEE Transactions on Software Engineering},
	Volume = {	 33},
	Number = {8},
	Pages = {558--574},
	Month = {August},
	Year = {2007}
} 


@InProceedings{JJR-FMCO-06, 
	Author = {Jeannet, B. and Jéron, T. and Rusu, V.},
	Title = {Model-based test selection for infinite state reactive systems},
	BookTitle = {{Formal Methods of Components and Objects - FMCO 2006, Amsterdam, Netherlands, Revised Lectures}},
	Volume = {	 4709},
	Pages = {47--69},
	Series = {LNCS},
	Publisher = {Springer},
	Year = {2007}
} 


@InProceedings{ifm2007, 
	Author = {Oostdijk, M. and Rusu, V. and Tretmans, J. and de Vries, R. and Willemse, T.},
	Title = {Integrating verification, testing, and learning for cryptographic protocols},
	BookTitle = {Integrated Formal Methods (IFM'07)},
	Series = {Lecture Notes in Computer Science},
	Publisher = {Springer Verlag},
	Year = {2007}
} 


@InCollection{book-chap-react-systems, 
	Author = {Constant, C. and Jéron, T. and Marchand, H. and Rusu, V.},
	Title = {Validation of Reactive Systems},
	BookTitle = {Modeling and Verification of Real-TIME Systems - Formalisms and software Tools},
	editor = {Merz, S. and Navet, N.},
	Chapter= {2},
	Pages = {51--76},
	Publisher = {Hermès Science},
	Month = {January},
	Year = {2008}
} 


@InProceedings{RusuC09, 
	Author = {Rusu, V. and Clavel, M.},
	Title = {Vérification d'invariants pour des systèmes spécifiés en logique de réécriture},
	BookTitle = {Vingtièmes Journées Francophones des Langages Applicatifs, JFLA 2009},
	editor = {Schmitt, A.},
	Volume = {7.2},
	Pages = {317--350},
	Series = {Studia Informatica Universalis},
	Address = {Saint Quentin sur Isère, France},
 	Month = {February},
	Year = {2009}
} 


@InProceedings{RusuC09b, 
	Author = {Rusu, Vlad},
	Title = {Formal Executable Semantics for Conformance in the MDE Framework},
	BookTitle = {UML and FM workshop},
	Address = {Rio de Janeiro, Brazil},
 	Month = {December},
	Year = {2009}
} 


@article{Rusu10b, 
	Author = {Egea, M. and Rusu, V.},
	Title = {Formal Executable Semantics for Conformance in the MDE Framework},
	Journal = {Innovations in Systems and Software Engineering},
	Volume = {	 6},
	Pages = {73--81},
	Year = {2010}
} 


@InProceedings{r10, 
	Author = {Rusu, V.},
	Title = {Combining narrowing and theorem proving for rewriting-logic specifications},
	BookTitle = {4th International Conference on Tests and Proofs (Tap'10)},
	Volume = {6143},
	Pages = {135--150},
	Series = {LNCS},
	Publisher = {Springer},
	Month = {July},
	Year = {2010}
} 


@InProceedings{grr10, 
	Author = {Gamatié, A. and Rusu, V. and Rutten, E.},
	Title = {Operational Semantics of the Marte Repetitive Structure Modeling Concepts for Data-Parallel Applications Design},
	BookTitle = {9th International Symposium on Parallel and Distributed Computing (ISPDC'10)},
	Pages = {25--32},
	Publisher = {IEEE Computer Society Press},
	Month = {July},
	Year = {2010}
} 


@article{gr10, 
	Author = {Genet, Th. and Rusu, V.},
	Title = {Equational Approximations for Tree Automata Completion},
	Journal = {Journal of Symbolic Computation},
	Volume = {	 45},
	Number = {5},
	Pages = {574--597},
	Month = {May},
	Year = {2010}
} 


@InProceedings{jeron2003, 
	Author = {Jéron, T. and Marchand, H. and Rusu, V. and Tschaen, V.},
	Title = {Synthèse de contrôleurs pour une relation de conformité},
	BookTitle = {4ième Colloque Francophone sur la Modélisation des Systèmes Réactifs, MSR'03},
	Address = {Metz, France},
 	Month = {October},
	Year = {2003}
} 


@InProceedings{jeron2003b, 
	Author = {Jéron, T. and Marchand, H. and Rusu, V. and Tschaen, V.},
	Title = {Ensuring the conformance of reactive discrete-event systems using supervisory control},
	BookTitle = {42nd IEEE Conference on Decision and Control},
	Address = {Hawaii, USA},
 	Month = {December},
	Year = {2003}
} 


@article{rusu03a, 
	Author = {Rusu, V.},
	Title = {Combining formal verification and conformance testing for validating reactive systems},
	Journal = {Journal of Software Testing, Verification, and Reliability},
	Volume = {13},
	Number = {3},
	Month = {September},
	Year = {2003}
} 


@InProceedings{rusu03b, 
	Author = {Rusu, V.},
	Title = {Compositional verification of an ATM protocol},
	BookTitle = {Formal Methods Europe (FME'03)},
	Year = {2003}
} 


@TechReport{jeannet04c, 
	Author = {Jeannet, B. and Jéron, T. and Rusu, V. and Zinovieva, E.},
	Title = {Symbolic test selection using approximate analysis},
	Number = {1649},
	Institution = {IRISA},
	Month = {October},
	Year = {2004}
} 


@article{jeron04a, 
	Author = {Jéron, T. and Marchand, H. and Rusu, V. and Tschaen, V.},
	Title = {Ensuring the conformance of reactive discrete-event systems by means of supervisory control},
	Journal = {International Journal of Production Research},
	Volume = {42},
	Number = {14},
	Pages = {2809--2826},
	Year = {2004}
} 


@TechReport{rusu04a, 
	Author = {Rusu, V.},
	Title = {Verifying an ATM Protocol Using a Combination of Formal Techniques},
	Number = {5089},
	Institution = {INRIA},
	Month = {January},
	Year = {2004}
} 


@InProceedings{rusu04b, 
	Author = {Rusu, V. and Marchand, H. and Tschaen, V. and Jéron, T. and Jeannet, B.},
	Title = {From Safety Verification to Safety Testing},
	BookTitle = {The 16th IFIP International Conference on Testing of Communicating Systems (TestCom04). Volume 2978 of LNCS},
	Publisher = {Springer-Verlag},
	Address = {Oxford, UK},
 	Month = {March},
	Year = {2004}
} 


@InProceedings{rusu04c, 
	Author = {Cachera, D. and Jensen, T. and Pichardie, D. and Rusu, V.},
	Title = {Extracting a data flow analyser in constructive logic},
	BookTitle = {European Symposium on Programming,ESOP'04. Volume 2986 of LNCS},
	Pages = {385--400},
	Publisher = {Springer-Verlag},
	Month = {February},
	Year = {2004}
} 


@TechReport{rusu04d, 
	Author = {Rusu, V. and Marchand, H. and Jéron, T.},
	Title = {Verification and Symbolic Test Generation for Safety Properties},
	Number = {1640},
	Institution = {IRISA},
	Month = {August},
	Year = {2004}
} 


@article{cachera05a, 
	Author = {Cachera, D. and Jensen, T. and Pichardie, D. and Rusu, V.},
	Title = {Extracting a data flow analyser in constructive logic},
	Journal = {Theoretical Computer Science},
	Volume = {	 342},
	Number = {1},
	Pages = {56--78},
	Month = {September},
	Year = {2005}
} 


@InProceedings{jeannet05a, 
	Author = {Jeannet, B. and Jéron, T. and Rusu, V. and Zinovieva, E.},
	Title = {Symbolic Test Selection based on Approximate Analysis},
	BookTitle = {11th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05)},
	Volume = {	 3440},
	Pages = {349--364},
	Series = {LNCS},
	Address = {Edinburgh (Scottland)},
 	Month = {April},
	Year = {2005}
} 


@TechReport{pichardie05a, 
	Author = {Pichardie, D. and Rusu, V.},
	Title = {Defining and Reasoning About General Recursive Functions in Type Theory: a Practical Method},
	Number = {1766},
	Institution = {Irisa},
	Month = {November},
	Year = {2005}
} 


@InProceedings{rusu05a, 
	Author = {Rusu, Vlad and Marchand, Hervé and Jéron, Thierry},
	Title = {Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems},
	BookTitle = {Formal Methods 2005 (FM05)},
	editor = {Fitzgerald, John and Tarlecki, Andrzej and Hayes, Ian},
	Volume = {	 3582},
	Pages = {189--204},
	Series = {LNCS},
	Publisher = {Springer},
	Month = {July},
	Year = {2005}
} 


@PhdThesis{Rusu06-hdr, 
	Author = {Rusu, V.},
	Title = {Formal verification and conformance testing for reactive systems},
	School = {Université de Rennes 1},
	Month = {December},
	Year = {2006}
	type = {Habilitation à diriger les recherches}, 
 } 


@TechReport{pass, 
	Author = {Breunesse, C. and Hubbers, E. and Koopman, P. and Mostowski, W. and Oostdijk, M. and Rusu, V. and de Vries, R. and van Weelden, A. and Wichers Schreur, R. and Willemse, T.},
	Title = {Testing the Dutch e-passport},
	Institution = {Radboud University, Nijmegen, The Netherlands},
	Year = {2006}
} 


@article{rusu-computer-journal, 
	Author = {Rusu, v.},
	Title = {Verifying an ATM Protocol Using a Combination of Formal Techniques},
	Journal = {Computer Journal},
	Volume = {49},
	Number = {6},
	Pages = {710--730},
	Month = {November},
	Year = {2006}
} 


@InCollection{I2C-constant-jeron-marchand-rusu-06, 
	Author = {Constant, C. and Jéron, T. and Marchand, H. and Rusu, V.},
	Title = {Combinaison entre vérification et test pour la validation de systèmes réactifs},
	BookTitle = {Traité I2C. Systèmes Temps Réel: Techniques de Description et de Vérification - Théorie et Outils},
	Volume = {1},
	Chapter= {2},
	Pages = {59--88},
	Publisher = {Hermès Science},
	Year = {2006}
} 


@InProceedings{flop-barthe-forest-pichardie-rusu-06, 
	Author = {Barthe, G. and Forest, J. and Pichardie, D. and Rusu, V.},
	Title = {Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant},
	BookTitle = {Functional and LOgic Programming Systems (FLOPS'06)},
	Volume = {3945},
	Pages = {114--129},
	Series = {LNCS},
	Address = {Fuji Susono, Japan},
 	Month = {April},
	Year = {2006}
} 


@TechReport{jeron-marchand-rusu-pi-deter-06, 
	Author = {Jéron, T. and Marchand, H. and Rusu, V.},
	Title = {Symbolic Determinisation of Extended Automata},
	Number = {1176},
	Institution = {IRISA},
	Month = {February},
	Year = {2006}
} 


@InProceedings{jeron-marchand-rusu-tcs-deter-06, 
	Author = {Jéron, T. and Marchand, H. and Rusu, V.},
	Title = {Symbolic Determinisation of Extended Automata},
	BookTitle = {4th IFIP International Conference on Theoretical Computer Science},
	Pages = {197--212},
	Series = {IFIP book series},
	Publisher = {Springer Science and Business Media},
	Address = {Stantiago, Chile},
 	Month = {August},
	Year = {2006}
} 


@InProceedings{bgl+00, 
	Author = {Bensalem, S. and Ganesh, V. and Lakhnech, Y. and Munoz, C. and Owre, S. and Russ, H. and Rushby, J. and Rusu, V. and Saidi, H. and Shankar, N. and Singerman, E. and Tiwari, A.},
	Title = {An Overview of SAL},
	BookTitle = {LFM 2000: Fifth NASA Langley Formal Methods Workshop},
	Pages = {187--196},
	Year = {2000}
} 


@InProceedings{rbj00, 
	Author = {Rusu, V. and du Bousquet, L. and Jéron, T.},
	Title = {An approach to symbolic test generation},
	BookTitle = {International Conference on Integrating Formal Methods (IFM'00)},
	Pages = {338--357},
	Series = {LNCS 1945},
	Publisher = {Springer Verlag},
	Month = {November},
	Year = {2000}
} 


@InProceedings{cjrz01a, 
	Author = {Clarke, D. and Jéron, T. and Rusu, V. and Zinovieva, E.},
	Title = {Automated Test and Oracle Generation for Smart-Card Applications},
	BookTitle = {International Conference on Research in Smart Cards (e-Smart'01), Volume 2140 of LNCS},
	Pages = {58--70},
	Year = {2001}
} 


@InProceedings{cjrz01b, 
	Author = {Clarke, D. and Jéron, T. and Rusu, V. and Zinovieva, E.},
	Title = {STG : A Tool for Generating Symbolic Test Programs and Oracles from Operational Specifications},
	BookTitle = {Joint 8th European Software Engineering Conference (ESEC) and 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-9)},
	Year = {2001}
} 


@InProceedings{r01a, 
	Author = {Rusu, V.},
	Title = {Verifying that Invariants are Context-Inductive},
	BookTitle = {Theorem Proving in Higher-Order Logics (TPHOLs'01),, Category B paper, University of Edinburgh research Report EDI-INF-RR-0046},
	Pages = {337--351},
	Year = {2001}
} 


@InProceedings{r01b, 
	Author = {Rusu, V.},
	Title = {Verifying a Sliding-Window Protocol using PVS},
	BookTitle = {Formal Description Techniques (FORTE'01)},
	Pages = {251--266},
	Year = {2001}
} 


@TechReport{rusu01, 
	Author = {Rusu, V.},
	Title = {Analyzing Automata with Presburger Arithmetic and Uninterpreted Function Symbols},
	Number = {4100},
	Institution = {INRIA},
	Year = {2001}
} 


@article{rz01, 
	Author = {Rusu, V. and Zinovieva, E.},
	Title = {Analyzing Automata with Presburger Arithmetic and Uninterpreted Function Symbols},
	Journal = {Electronic Notes in Theoretical Computer Science},
	Volume = {50},
	Number = {4},
	Year = {2001}
} 


@InProceedings{clarke02a, 
	Author = {Clarke, D. and Jéron, T. and Rusu, V. and Zinovieva, E.},
	Title = {STG: a Symbolic Test Generation tool},
	BookTitle = {(Tool paper) Tools and Algorithms for the Construction and Analysis of Systems (TACAS'02). Volume 2280 of LNCS},
	Publisher = {Springer-Verlag},
	Year = {2002}
} 


@InProceedings{rusu02a, 
	Author = {Rusu, V.},
	Title = {Verification using test generation techniques},
	BookTitle = {Formal Methods Europe (FME'02)},
	Year = {2002}
} 


@InProceedings{rzc02, 
	Author = {Rusu, V. and Zinovieva, E. and Clarke, D.},
	Title = {Verifying Invariants More Automatically},
	BookTitle = {Verification and Computatoiional Logic, VCL'02},
	Year = {2002}
} 


@InProceedings{burgueno97, 
	Author = {Burgueno, A. and Rusu, V.},
	Title = {Task-system analysis using slope-parametric hybrid automata},
	BookTitle = {Proceedings of the European Conference on Parallelism (EuroPar'97) Volume 1300 of LNCS},
	Pages = {1262--1273},
	Address = {Passau (Germany)},
 	Year = {1997}
} 


@InProceedings{rusu97, 
	Author = {Rusu, V.},
	Title = {Verifying periodic task-control systems},
	BookTitle = {International Workshop on Hybrid and Real-Time Systems (HART'97), Volume 1201 of LNCS},
	Pages = {63--69},
	Address = {Grenoble, France},
 	Year = {1997}
} 


@InProceedings{boniol97, 
	Author = {Boniol, F. and Burgueno, A. and Roux, O. and Rusu, V.},
	Title = {Analysis of slope-parametric hybrid automata},
	BookTitle = {International Workshop on Hybrid and Real-Time Systems (HART'97), Volume 1201 of LNCS},
	Pages = {75--81},
	Address = {Grenoble, France},
 	Year = {1997}
} 


@InProceedings{hr98, 
	Author = {Henzinger, T.A. and Rusu, V.},
	Title = {Reachability verification for hybrid automata},
	BookTitle = {International Workshop on Hybrid Systems: Computation and Control},
	Pages = {190--204},
	Series = {LNCS 1386},
	Publisher = {Springer Verlag},
	Address = {Berkeley, California, USA},
 	Year = {1998}
} 


@InProceedings{rr99, 
	Author = {Rusu, V. and Singerman, E.},
	Title = {On proving safety properties by integrating static analysis, theorem proving and abstraction},
	BookTitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS'99)},
	Pages = {178--192},
	Series = {LNCS 1579},
	Publisher = {Springer Verlag},
	Year = {1999}
} 


@article{rrc99, 
	Author = {Roux, O and Rusu, V. and Cassez, F.},
	Title = {Hybrid verifications of reactive programs},
	Journal = {Formal Aspects of Computing},
	Volume = {11},
	Number = {4},
	Pages = {448--471},
	Year = {1999}
} 


@TechReport{rs99, 
	Author = {Rusu, V. and Singerman, E.},
	Title = {Interactive abstractions: proving safety property by integrating static analysis, theorem proving, and abstraction},
	Number = {1256},
	Institution = {IRISA},
	Month = {July},
	Year = {1999}
} 


@article{roux94, 
	Author = {Roux, O. and Rusu, V.},
	Title = {Translating from GRAFCET to the reactive language ELECTRE},
	Journal = {Automatique, Productique et Informatique Industrielle},
	Volume = {28},
	Number = {2},
	Pages = {131--158},
	Year = {1994}
} 


@InProceedings{roux96, 
	Author = {Roux, O. and Rusu, V.},
	Title = {Deciding time-bounded properties for ELECTRE reactive programs with stopwatch automata},
	BookTitle = {International workshop on Hybrid Systems and Autonomous Control (WHSAC'94), Volume 999 of LNCS},
	Pages = {405--416},
	Address = {Cornell University, Ithaca (New York, USA)},
 	Year = {1996}
} 


@PhdThesis{rusu96, 
	Author = {Rusu, V.},
	Title = {Vérification temporelle de programmes ELECTRE},
	School = {Ecole Centrale de Nantes, Laboratoire d'Automatique de Nantes},
	Month = {January},
	Year = {1996}
}