Vlad Rusu

Orcid: 0000-0002-3495-2232

According to our database1, Vlad Rusu authored at least 56 papers between 1994 and 2023.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

On csauthors.net:

Bibliography

2023
While Loops in Coq.
Proceedings of the Proceedings 7th Symposium on Working Formal Methods, 2023

2022
Defining Corecursive Functions in Coq Using Approximations (Artifact).
Dagstuhl Artifacts Ser., 2022

A Formal Correctness Proof for an EDF Scheduler Implementation.
Proceedings of the 28th IEEE Real-Time and Embedded Technology and Applications Symposium, 2022

Defining Corecursive Functions in Coq Using Approximations.
Proceedings of the 36th European Conference on Object-Oriented Programming, 2022

2021
Guest Editor's foreword.
J. Log. Algebraic Methods Program., 2021

2020
Proving partial-correctness and invariance properties of transition-system models.
Sci. Comput. Program., 2020

2019
(Co)inductive Proof Systems for Compositional Proofs in Reachability Logic.
Proceedings of the Proceedings Third Symposium on Working Formal Methods, 2019

2017
A generic framework for symbolic execution: A coinductive approach.
J. Symb. Comput., 2017

Executing and verifying higher-order functional-imperative programs in Maude.
J. Log. Algebraic Methods Program., 2017

A Certified Procedure for RL Verification.
Proceedings of the 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2017

2016
Language definitions as rewrite theories.
J. Log. Algebraic Methods Program., 2016

A language-independent proof system for full program equivalence.
Formal Aspects Comput., 2016

Proving Reachability-Logic Formulas Incrementally.
Proceedings of the Rewriting Logic and Its Applications - 11th International Workshop, 2016

2015
Program equivalence by circular reasoning.
Formal Aspects Comput., 2015

Symbolic execution based on language transformation.
Comput. Lang. Syst. Struct., 2015

Verifying Reachability-Logic Properties on Rewriting-Logic Specifications.
Proceedings of the Logic, Rewriting, and Concurrency, 2015

2014
A Theoretical Foundation for Programming Languages Aggregation.
Proceedings of the Recent Trends in Algebraic Development Techniques, 2014

A Language-Independent Proof System for Mutual Program Equivalence.
Proceedings of the Formal Methods and Software Engineering, 2014

2013
Embedding domain-specific modelling languages in Maude specifications.
Softw. Syst. Model., 2013

A Generic Framework for Symbolic Execution.
Proceedings of the Software Language Engineering - 6th International Conference, 2013

2011
Towards a K Semantics for OCL.
Proceedings of the Second International Workshop on the K Framework and its Applications, 2011

A K-Based Formal Framework for Domain-Specific Modelling Languages.
Proceedings of the Formal Verification of Object-Oriented Software, 2011

A Generic Tool for Tracing Executions Back to a DSML's Operational Semantics.
Proceedings of the Modelling Foundations and Applications - 7th European Conference, 2011

2010
Equational approximations for tree automata completion.
J. Symb. Comput., 2010

Formal executable semantics for conformance in the MDE framework.
Innov. Syst. Softw. Eng., 2010

Combining Theorem Proving and Narrowing for Rewriting-Logic Specifications.
Proceedings of the Tests and Proofs - 4th International Conference, 2010

Operational Semantics of the Marte Repetitive Structure Modeling Concepts for Data-Parallel Applications Design.
Proceedings of the Ninth International Symposium on Parallel and Distributed Computing, 2010

2009
Vérification d'invariants pour des systèmes spécifiés en logique de réécriture.
Stud. Inform. Univ., 2009

2007
Integrating formal verification and conformance testing for reactive systems.
IEEE Trans. Software Eng., 2007

Integrating Verification, Testing, and Learning for Cryptographic Protocols.
Proceedings of the Integrated Formal Methods, 6th International Conference, 2007

2006
Verifying an ATM Protocol Using a Combination of Formal Techniques.
Comput. J., 2006

Symbolic Determinisation of Extended Automata.
Proceedings of the Fourth IFIP International Conference on Theoretical Computer Science (TCS 2006), 2006

Model-Based Test Selection for Infinite-State Reactive Systems.
Proceedings of the Formal Methods for Components and Objects, 5th International Symposium, 2006

Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant.
Proceedings of the Functional and Logic Programming, 8th International Symposium, 2006

2005
Extracting a data flow analyser in constructive logic.
Theor. Comput. Sci., 2005

Symbolic Test Selection Based on Approximate Analysis.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems.
Proceedings of the FM 2005: Formal Methods, 2005

2004
From Safety Verification to Safety Testing.
Proceedings of the Testing of Communicating Systems, 16th IFIP International Conerence, 2004

2003
Combining formal verification and conformance testing for validating reactive systems.
Softw. Test. Verification Reliab., 2003

Compositional Verification of an ATM Protocol.
Proceedings of the FME 2003: Formal Methods, 2003

Ensuring the conformance of reactive discrete-event systems using supervisory control.
Proceedings of the 42nd IEEE Conference on Decision and Control, 2003

2002
STG: A Symbolic Test Generation Tool.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2002

Verification Using Test Generation Techniques.
Proceedings of the FME 2002: Formal Methods, 2002

2001
Analyzing Automata with Presburger Arithmetic and Uninterpreted Function Symbols.
Proceedings of the Verification of Parameterized Systems, 2001

STG: a tool for generating symbolic test programs and oracles from operational specifications.
Proceedings of the 8th European Software Engineering Conference held jointly with 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering 2001, 2001

Verifying a Sliding Window Protocol using PVS.
Proceedings of the Formal Techniques for Networked and Distributed Systems, 2001

Automated Test and Oracle Generation for Smart-Card Applications.
Proceedings of the Smart Card Programming and Security, 2001

2000
An Approach to Symbolic Test Generation.
Proceedings of the Integrated Formal Methods, Second International Conference, 2000

1999
Hybrid Verifications of Reactive Programs.
Formal Aspects Comput., 1999

On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1999

1998
Reachability Verification for Hybrid Automata.
Proceedings of the Hybrid Systems: Computation and Control, First International Workshop, 1998

1997
Verifying Periodic Task-Control Systems.
Proceedings of the Hybrid and Real-Time Systems, 1997

Analysis of Slope-Parametric Hybrid Automata.
Proceedings of the Hybrid and Real-Time Systems, 1997

Task-System Analysis Using Slope-Parametric Hybrid Automata.
Proceedings of the Euro-Par '97 Parallel Processing, 1997

1996
Uniformity for the Decidability of Hybrid Automata.
Proceedings of the Static Analysis, Third International Symposium, 1996

1994
Verifying Time-bounded Properties for ELECTRE Reactive Programs with Stopwatch Automata.
Proceedings of the Hybrid Systems II, 1994


  Loading...