Vlad Rusu

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