Vlad Rusu

Publication Activity (10 Years)

Years Active: 1994-2024
Publications (10 Years): 16

Top Topics

Formal Definitions

Symbolic Execution

Top Venues

J. Log. Algebraic Methods Program.

Formal Aspects Comput.

Publications

Horatiu Cheval, David Nowak, Vlad Rusu
Formal definitions and proofs for partial (co)recursive functions. J. Log. Algebraic Methods Program. 141 (2024)
David Nowak, Vlad Rusu
While Loops in Coq. FROM (2023)
Florian Vanhems, Vlad Rusu, David Nowak, Gilles Grimaud
A Formal Correctness Proof for an EDF Scheduler Implementation. RTAS (2022)
Vlad Rusu, David Nowak
Defining Corecursive Functions in Coq Using Approximations (Artifact). Dagstuhl Artifacts Ser. 8 (2) (2022)
Vlad Rusu, David Nowak
Defining Corecursive Functions in Coq Using Approximations. ECOOP (2022)
Vlad Rusu, David Nowak
(Co)inductive proof systems for compositional proofs in reachability logic. J. Log. Algebraic Methods Program. 118 (2021)
Vlad Rusu
Guest Editor's foreword. J. Log. Algebraic Methods Program. 123 (2021)
Vlad Rusu, Gilles Grimaud, Michaël Hauspie
Proving partial-correctness and invariance properties of transition-system models. Sci. Comput. Program. 186 (2020)
Vlad Rusu, David Nowak
(Co)inductive Proof Systems for Compositional Proofs in Reachability Logic. FROM (2019)
Vlad Rusu, Gilles Grimaud, Michaël Hauspie
Proving Partial-Correctness and Invariance Properties of Transition-System Models. TASE (2018)
Dorel Lucanu, Vlad Rusu, Andrei Arusoaie
A generic framework for symbolic execution: A coinductive approach. J. Symb. Comput. 80 (2017)
Vlad Rusu, Andrei Arusoaie
Executing and verifying higher-order functional-imperative programs in Maude. J. Log. Algebraic Methods Program. 93 (2017)
Andrei Arusoaie, David Nowak, Vlad Rusu, Dorel Lucanu
A Certified Procedure for RL Verification. SYNASC (2017)
Vlad Rusu, Dorel Lucanu, Traian-Florin Serbanuta, Andrei Arusoaie, Andrei Stefanescu, Grigore Rosu
Language definitions as rewrite theories. J. Log. Algebraic Methods Program. 85 (1) (2016)
Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu
A language-independent proof system for full program equivalence. Formal Aspects Comput. 28 (3) (2016)
Vlad Rusu, Andrei Arusoaie
Proving Reachability-Logic Formulas Incrementally. WRLA (2016)
Dorel Lucanu, Vlad Rusu
Program equivalence by circular reasoning. Formal Aspects Comput. 27 (4) (2015)
Dorel Lucanu, Vlad Rusu, Andrei Arusoaie, David Nowak
Verifying Reachability-Logic Properties on Rewriting-Logic Specifications. Logic, Rewriting, and Concurrency (2015)
Andrei Arusoaie, Dorel Lucanu, Vlad Rusu
Symbolic execution based on language transformation. Comput. Lang. Syst. Struct. 44 (2015)
Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu
A Language-Independent Proof System for Mutual Program Equivalence. ICFEM (2014)
Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu
A Theoretical Foundation for Programming Languages Aggregation. WADT (2014)
Andrei Arusoaie, Dorel Lucanu, Vlad Rusu, Traian-Florin Serbanuta, Andrei Stefanescu, Grigore Rosu
Language Definitions as Rewrite Theories. WRLA (2014)
Andrei Arusoaie, Dorel Lucanu, Vlad Rusu
Towards a K Semantics for OCL. Electron. Notes Theor. Comput. Sci. 304 (2014)
Vlad Rusu
Embedding domain-specific modelling languages in Maude specifications. Softw. Syst. Model. 12 (4) (2013)
Andrei Arusoaie, Dorel Lucanu, Vlad Rusu
A Generic Framework for Symbolic Execution. SLE (2013)
Dorel Lucanu, Vlad Rusu
Program Equivalence by Circular Reasoning. IFM (2013)
Vlad Rusu, Dorel Lucanu
A K-Based Formal Framework for Domain-Specific Modelling Languages. FoVeOOS (2011)
Benoît Combemale, Laure Gonnord, Vlad Rusu
A Generic Tool for Tracing Executions Back to a DSML's Operational Semantics. ECMFA (2011)
Vlad Rusu
Embedding domain-specific modelling languages in maude specifications. ACM SIGSOFT Softw. Eng. Notes 36 (1) (2011)
Vlad Rusu
Combining Theorem Proving and Narrowing for Rewriting-Logic Specifications. TAP@TOOLS (2010)
Abdoulaye Gamatié, Vlad Rusu, Éric Rutten
Operational Semantics of the Marte Repetitive Structure Modeling Concepts for Data-Parallel Applications Design. ISPDC (2010)
Thomas Genet, Vlad Rusu
Equational approximations for tree automata completion. J. Symb. Comput. 45 (5) (2010)
Marina Egea, Vlad Rusu
Formal executable semantics for conformance in the MDE framework. Innov. Syst. Softw. Eng. 6 (1-2) (2010)
Vlad Rusu, Manuel Clavel
Vérification d'invariants pour des systèmes spécifiés en logique de réécriture. JFLA (2009)
Vlad Rusu, Manuel Clavel
Vérification d'invariants pour des systèmes spécifiés en logique de réécriture. Stud. Inform. Univ. 7 (2) (2009)
Camille Constant, Thierry Jéron, Hervé Marchand, Vlad Rusu
Integrating formal verification and conformance testing for reactive systems. IEEE Trans. Software Eng. 33 (8) (2007)
Martijn Oostdijk, Vlad Rusu, Jan Tretmans, René G. de Vries, Tim A. C. Willemse
Integrating Verification, Testing, and Learning for Cryptographic Protocols. IFM (2007)
Gilles Barthe, Julien Forest, David Pichardie, Vlad Rusu
Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant. FLOPS (2006)
Bertrand Jeannet, Thierry Jéron, Vlad Rusu
Model-Based Test Selection for Infinite-State Reactive Systems. FMCO (2006)
Thierry Jéron, Hervé Marchand, Vlad Rusu
Symbolic Determinisation of Extended Automata. IFIP TCS (2006)
Vlad Rusu
Verifying an ATM Protocol Using a Combination of Formal Techniques. Comput. J. 49 (6) (2006)
Vlad Rusu, Hervé Marchand, Thierry Jéron
Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems. FM (2005)
Bertrand Jeannet, Thierry Jéron, Vlad Rusu, Elena Zinovieva
Symbolic Test Selection Based on Approximate Analysis. TACAS (2005)
David Cachera, Thomas P. Jensen, David Pichardie, Vlad Rusu
Extracting a data flow analyser in constructive logic. Theor. Comput. Sci. 342 (1) (2005)
David Cachera, Thomas P. Jensen, David Pichardie, Vlad Rusu
Extracting a Data Flow Analyser in Constructive Logic. ESOP (2004)
Vlad Rusu, Hervé Marchand, Valéry Tschaen, Thierry Jéron, Bertrand Jeannet
From Safety Verification to Safety Testing. TestCom (2004)
Vlad Rusu
Compositional Verification of an ATM Protocol. FME (2003)
Vlad Rusu
Combining formal verification and conformance testing for validating reactive systems. Softw. Test. Verification Reliab. 13 (3) (2003)
Thieny Eron, Hervé Marchand, Vlad Rusu, Valéry Tschaen
Ensuring the conformance of reactive discrete-event systems using supervisory control. CDC (2003)
Duncan Clarke, Thierry Jéron, Vlad Rusu, Elena Zinovieva
STG: A Symbolic Test Generation Tool. TACAS (2002)
Vlad Rusu
Verification Using Test Generation Techniques. FME (2002)
Vlad Rusu, Elena Zinovieva
Analyzing Automata with Presburger Arithmetic and Uninterpreted Function Symbols. Electron. Notes Theor. Comput. Sci. 50 (4) (2001)
Duncan Clarke, Thierry Jéron, Vlad Rusu, Elena Zinovieva
STG: a tool for generating symbolic test programs and oracles from operational specifications. ESEC / SIGSOFT FSE (2001)
Vlad Rusu
Verifying a Sliding Window Protocol using PVS. FORTE (2001)
Duncan Clarke, Thierry Jéron, Vlad Rusu, Elena Zinovieva
Automated Test and Oracle Generation for Smart-Card Applications. E-smart (2001)
Vlad Rusu, Lydie du Bousquet, Thierry Jéron
An Approach to Symbolic Test Generation. IFM (2000)
Vlad Rusu, Eli Singerman
On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction. TACAS (1999)
Olivier F. Roux, Vlad Rusu, Franck Cassez
Hybrid Verifications of Reactive Programs. Formal Aspects Comput. 11 (4) (1999)
Thomas A. Henzinger, Vlad Rusu
Reachability Verification for Hybrid Automata. HSCC (1998)
Frédéric Boniol, Augusto Burgueño, Olivier F. Roux, Vlad Rusu
Analysis of Slope-Parametric Hybrid Automata. HART (1997)
Vlad Rusu
Verifying Periodic Task-Control Systems. HART (1997)
Augusto Burgueño, Vlad Rusu
Task-System Analysis Using Slope-Parametric Hybrid Automata. Euro-Par (1997)
Olivier F. Roux, Vlad Rusu
Uniformity for the Decidability of Hybrid Automata. SAS (1996)
Olivier F. Roux, Vlad Rusu
Verifying Time-bounded Properties for ELECTRE Reactive Programs with Stopwatch Automata. Hybrid Systems (1994)