Verifying Time-bounded Properties for ELECTRE Reactive Programs with Stopwatch Automata. - Olivier F. Roux; Vlad Rusu (Hybrid Systems, 1994)

Uniformity for the Decidability of Hybrid Automata. - Olivier F. Roux; Vlad Rusu (SAS, 1996)

Task-System Analysis Using Slope-Parametric Hybrid Automata. - Augusto Burgueño; Vlad Rusu (Euro-Par, 1997)

Analysis of Slope-Parametric Hybrid Automata. - Frédéric Boniol; Augusto Burgueño; Olivier F. Roux; Vlad Rusu (HART, 1997)

Verifying Periodic Task-Control Systems. - Vlad Rusu (HART, 1997)

Reachability Verification for Hybrid Automata. - Thomas A. Henzinger; Vlad Rusu (HSCC, 1998)

On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction. - Vlad Rusu; Eli Singerman (TACAS, 1999)

Hybrid Verifications of Reactive Programs. - Olivier F. Roux; Vlad Rusu; Franck Cassez (Formal Aspects Comput., 1999)

An Approach to Symbolic Test Generation. - Vlad Rusu; Lydie du Bousquet; Thierry Jéron (IFM, 2000)

Automated Test and Oracle Generation for Smart-Card Applications. - Duncan Clarke; Thierry Jéron; Vlad Rusu; Elena Zinovieva 001 (E-smart, 2001)

Verifying a Sliding Window Protocol using PVS. - Vlad Rusu (FORTE, 2001)

STG: a tool for generating symbolic test programs and oracles from operational specifications. - Duncan Clarke; Thierry Jéron; Vlad Rusu; Elena Zinovieva 001 (ESEC / SIGSOFT FSE, 2001)

Analyzing Automata with Presburger Arithmetic and Uninterpreted Function Symbols. - Vlad Rusu; Elena Zinovieva 001 (VEPAS, 2001)

Verification Using Test Generation Techniques. - Vlad Rusu (FME, 2002)

STG: A Symbolic Test Generation Tool. - Duncan Clarke; Thierry Jéron; Vlad Rusu; Elena Zinovieva 001 (TACAS, 2002)

Ensuring the conformance of reactive discrete-event systems using supervisory control. - Thieny Eron; Hervé Marchand; Vlad Rusu; Valéry Tschaen (CDC, 2003)

Compositional Verification of an ATM Protocol. - Vlad Rusu (FME, 2003)

Combining formal verification and conformance testing for validating reactive systems. - Vlad Rusu (Softw. Test. Verification Reliab., 2003)

From Safety Verification to Safety Testing. - Vlad Rusu; Hervé Marchand; Valéry Tschaen; Thierry Jéron; Bertrand Jeannet (TestCom, 2004)

Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems. - Vlad Rusu; Hervé Marchand; Thierry Jéron (FM, 2005)

Symbolic Test Selection Based on Approximate Analysis. - Bertrand Jeannet; Thierry Jéron; Vlad Rusu; Elena Zinovieva 001 (TACAS, 2005)

Extracting a data flow analyser in constructive logic. - David Cachera; Thomas P. Jensen; David Pichardie; Vlad Rusu (Theor. Comput. Sci., 2005)

Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant. - Gilles Barthe; Julien Forest; David Pichardie; Vlad Rusu (FLOPS, 2006)

Model-Based Test Selection for Infinite-State Reactive Systems. - Bertrand Jeannet; Thierry Jéron; Vlad Rusu (FMCO, 2006)

Symbolic Determinisation of Extended Automata. - Thierry Jéron; Hervé Marchand; Vlad Rusu (IFIP TCS, 2006)

Verifying an ATM Protocol Using a Combination of Formal Techniques. - Vlad Rusu (Comput. J., 2006)

Integrating Verification, Testing, and Learning for Cryptographic Protocols. - Martijn Oostdijk; Vlad Rusu; Jan Tretmans; René G. de Vries; Tim A. C. Willemse (IFM, 2007)

Integrating formal verification and conformance testing for reactive systems. - Camille Constant; Thierry Jéron; Hervé Marchand; Vlad Rusu (IEEE Trans. Software Eng., 2007)

Vérification d'invariants pour des systèmes spécifiés en logique de réécriture. - Vlad Rusu; Manuel Clavel (Stud. Inform. Univ., 2009)

Operational Semantics of the Marte Repetitive Structure Modeling Concepts for Data-Parallel Applications Design. - Abdoulaye Gamatié; Vlad Rusu; Éric Rutten (ISPDC, 2010)

Combining Theorem Proving and Narrowing for Rewriting-Logic Specifications. - Vlad Rusu (TAP@TOOLS, 2010)

Formal executable semantics for conformance in the MDE framework. - Marina Egea; Vlad Rusu (Innov. Syst. Softw. Eng., 2010)

Equational approximations for tree automata completion. - Thomas Genet; Vlad Rusu (J. Symb. Comput., 2010)

A Generic Tool for Tracing Executions Back to a DSML's Operational Semantics. - Benoît Combemale; Laure Gonnord; Vlad Rusu (ECMFA, 2011)

A K-Based Formal Framework for Domain-Specific Modelling Languages. - Vlad Rusu; Dorel Lucanu (FoVeOOS, 2011)

Towards a K Semantics for OCL. - Andrei Arusoaie; Dorel Lucanu; Vlad Rusu (K, 2011)

A Generic Framework for Symbolic Execution. - Andrei Arusoaie; Dorel Lucanu; Vlad Rusu (SLE, 2013)

Embedding domain-specific modelling languages in Maude specifications. - Vlad Rusu (Softw. Syst. Model., 2013)

A Language-Independent Proof System for Mutual Program Equivalence. - Stefan Ciobaca; Dorel Lucanu; Vlad Rusu; Grigore Rosu (ICFEM, 2014)

A Theoretical Foundation for Programming Languages Aggregation. - Stefan Ciobaca; Dorel Lucanu; Vlad Rusu; Grigore Rosu (WADT, 2014)

Verifying Reachability-Logic Properties on Rewriting-Logic Specifications. - Dorel Lucanu; Vlad Rusu; Andrei Arusoaie; David Nowak (Logic, Rewriting, and Concurrency, 2015)

Symbolic execution based on language transformation. - Andrei Arusoaie; Dorel Lucanu; Vlad Rusu (Comput. Lang. Syst. Struct., 2015)

Program equivalence by circular reasoning. - Dorel Lucanu; Vlad Rusu (Formal Aspects Comput., 2015)

Proving Reachability-Logic Formulas Incrementally. - Vlad Rusu; Andrei Arusoaie (WRLA, 2016)

A language-independent proof system for full program equivalence. - Stefan Ciobaca; Dorel Lucanu; Vlad Rusu; Grigore Rosu (Formal Aspects Comput., 2016)

Language definitions as rewrite theories. - Vlad Rusu; Dorel Lucanu; Traian-Florin Serbanuta; Andrei Arusoaie; Andrei Stefanescu; Grigore Rosu (J. Log. Algebraic Methods Program., 2016)

A Certified Procedure for RL Verification. - Andrei Arusoaie; David Nowak; Vlad Rusu; Dorel Lucanu (SYNASC, 2017)

Executing and verifying higher-order functional-imperative programs in Maude. - Vlad Rusu; Andrei Arusoaie (J. Log. Algebraic Methods Program., 2017)

A generic framework for symbolic execution: A coinductive approach. - Dorel Lucanu; Vlad Rusu; Andrei Arusoaie (J. Symb. Comput., 2017)

Proving partial-correctness and invariance properties of transition-system models. - Vlad Rusu; Gilles Grimaud; Michaël Hauspie (Sci. Comput. Program., 2020)

Guest Editor's foreword. - Vlad Rusu (J. Log. Algebraic Methods Program., 2021)

(Co)inductive proof systems for compositional proofs in reachability logic. - Vlad Rusu; David Nowak (J. Log. Algebraic Methods Program., 2021)

Defining Corecursive Functions in Coq Using Approximations. - Vlad Rusu; David Nowak (ECOOP, 2022)

A Formal Correctness Proof for an EDF Scheduler Implementation. - Florian Vanhems; Vlad Rusu; David Nowak; Gilles Grimaud (RTAS, 2022)

Defining Corecursive Functions in Coq Using Approximations (Artifact). - Vlad Rusu; David Nowak (Dagstuhl Artifacts Ser., 2022)

While Loops in Coq. - David Nowak; Vlad Rusu (FROM, 2023)

Formal definitions and proofs for partial (co)recursive functions. - Horatiu Cheval; David Nowak; Vlad Rusu (J. Log. Algebraic Methods Program., 2024)