D. Cachera, T. Jensen. D. Pichardie, and V. Rusu Extracting a data-flow analyser in constructive logic. Theoretical Computer Science , 342(1):56-78, September 2005.
T. Jeron, H. Marchand, V. Rusu, and 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.
V. Rusu. Combining formal verification and conformance testing for validating reactive systems. Journal of Software Testing, Verification, and Reliability 13(3), pp. 157-180, 2003.
V. Rusu and E. Zinovieva. Analizing automata with Presburger arithmetic and uninterpreted function symbols. Electronic Notes in Theoretical Computer Science , 50(4), 2001.
O. Roux, V. Rusu and F. Cassez. Hybrid verifications of reactive programs. Formal Aspects of Computing, 11(4):448-471, 1999.
O. Roux and V. Rusu. Translating from GRAFCET to the reactive language ELECTRE. Automatique, Productique et Informatique Industrielle, 28(2):131-158, 1994.
V. Rusu, H. Marchand, T. Jéron. Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems . Formal Methods (FM'05)
B. Jeannet, T. Jéron, V. Rusu, E. Zinovieva, Symbolic Test Selection based on Approximate Analysis. 11th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems, Edinburgh (TACAS'05), LNCS.
D. Cachera, T. Jensen, D. Pichardie, and V. Rusu. Extracting a data flow analyser in constructive logic. European Symposium on Programming (ESOP'04), LNCS.
V. Rusu, H. Marchand, V. Tschaen, T. Jéron, and B. Jeannet. From safety verification to safety testing. IFIP International Conference on Testing of Communicating Systems (TestCom'04), LNCS.
V. Rusu. Compositional verification of an ATM protocol. In Formal Methods (FM'03). Abstract, postscript, and PVS files.
T. Jéron, H. Marchand, V. Rusu and V. Tschaen. Ensuring the conformance of reactive discrete-event systems using supervisory control. In 42nd IEEE Conference on Decision and Control (CDC'03). Abstract, postscript.
T. Jéron, H. Marchand, V. Rusu, et V. Tschaen. Synthèse de contrôleurs pour une relation de conformité. In Modélisation des systèmes réactifs, (MSR'03). Abstract, postscript.
V. Rusu, E. Zinovieva, and D. Clarke. Verifying Invariants More Automatically. In Wokshop on Verification and Computational Logic, VCL'02. Abstract, postscript
V. Rusu. Verification using test generation techniques. In Formal Methods Europe (FME'02), pp. 252-271. LNCS 2391. Abstract, postscript, PVS, and STG scripts.
D. Clarke, T. Jéron, V. Rusu, and E. Zinovieva. STG: a Symbolic Test Generation tool. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS'02), pp. 470-475. LNCS 2280. Abstract, postscript.
V. Rusu. Verifying a sliding-window protocol using PVS. In Formal Techniques for Networked and Distributed Systems (FORTE'01) , pp 251-266, 2001. Abstract, postscript, and PVS files
D. Clarke, T. Jéron, V. Rusu, and E. Zinovieva. Automated test and oracle generation for Smart-Card applications. In International Conference on Research in Smart Cards (e-Smart'01) , pp. 58-70, 2001. LNCS 2140. Abstract, postscript
V. Rusu. Verifying that Invariants are Context-Inductive. In Theorem Proving in Higher-Order Logics (TPHOLs'01,) emergind trends paper. University of Edinburgh, Informatics Research Report EDI-INF-RR-0046, pp 337-351, 2001. Abstract, postscript
D. Clarke, T. Jéron, V. Rusu, and 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) , pp. 301-302, 2001.
V. Rusu, L. du Bousquet, and T. Jéron. An approach to symbolic test generation. In International Conference on Integrating Formal Methods (IFM'00), Dagstuhl (Germany), pp 338-357, 2000. LNCS 1945. Abstract, postscript.
S. Bensalem, V. Ganesh, Y. Lakhnech, Cesar Munoz, S. Owre, H. Ruess, J. Rushby, V. Rusu, H. Saidi, N. Shankar, E. Singerman, and A. Tiwari. An Overview of SAL. In Fifth NASA Langley Formal Methods Workshop (LFM'00) , pp 187--196, 2000. Abstract, postscript.
V. Rusu and 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), Amsterdam (Netherlands), pp 178-192, 1999. LNCS 1579. An improved version appeared as IRISA research report 1256. Abstract, postscript of report.
T.A. Henzinger and V. Rusu. Reachability verification for hybrid automata. In International Workshop on Hybrid Systems: Computation and Control, Berkeley (California, USA), pp 190-204, 1998, LNCS 1386. Abstract, postscript.
A. Burgueño and V. Rusu. Task-system analysis using slope-parametric hybrid automata. In Proceedings of the European Conference on Parallelism (EuroPar'97), pp 1262-1273, Passau (Germany), 1997. LNCS 1300. Distinguished Paper. Abstract, postscript.
V. Rusu. Verifying periodic task-control systems. In International Workshop on Hybrid and Real-Time Systems (HART'97), pp 63-69, Grenoble (France), 1997. LNCS 1201. Abstract, postscript.
F. Boniol, A. Burgueño, O. Roux, and V. Rusu. Analysis of slope-parametric hybrid automata. In International Workshop on Hybrid and Real-Time Systems (HART'97), pages 75-81, Grenoble (France), 1997. LNCS 1201. Abstract, postscript.
O. Roux and V. Rusu. Uniformity for the decidability of hybrid automata. In International Static Analysis Symposium (SAS'96), pp 301-316, Aachen (Germany), 1996. LNCS 1145. Abstract, postscript.
O. Roux and V. Rusu. Deciding time-bounded properties for ELECTRE reactive programs with stopwatch automata. In International workshop on Hybrid Systems and Autonomous Control (WHSAC'94), pp 405-416, Cornell University, Ithaca (New York, USA), 1994. LNCS 999. Abstract.
Symbolic Test Selection based on Approximate Analysis. Bertand Jeannet, Thierry Jéron, Vlad Rusu, Elena Zinovieva.
Verification and Symbolic Test Generation for Safety Properties. Vlad Rusu, Hervé Marchand, Thierry Jéron.
Verifying an ATM Protocol Using a Combination of Formal Techniques. Vlad Rusu
Interactive Abstractions: Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction. Vlad Rusu, Eli Singerman.
V. Rusu. Vérification temporelle de programmes ELECTRE. PhD, Ecole Centrale de Nantes, Laboratoire d'Automatique de Nantes, january 1996. Abstract published in Bulletin of the European Association for Theoretical Computer Science (EATCS) no. 59 (june 1996) pp. 439-441.