Formal Methods in Software Engineering

Vlad Rusu

Institution: Inria Lille, France
Email: vlad.rusu@inria.fr
Status: Collaborator

Publications

2018

A Certified Procedure for RL Verification (SYNASC 2017 post-proceedings, to appear in IEEE Conference Publishing Service )

Andrei Arusoaie, David Nowak, Vlad Rusu, Dorel Lucanu

Unpublished

2017

A generic framework for symbolic execution: A coinductive approach

Dorel Lucanu, Vlad Rusu, Andrei Arusoaie

Journal

Executing and verifying higher-order functional-imperative programs in Maude.

Vlad Rusu, Andrei Arusoaie

Journal

A Certified Procedure for RL Verification (SYNASC 2017 pre-proceedings)

Andrei Arusoaie, David Nowak, Vlad Rusu, Dorel Lucanu

Conference

2016

Language definitions as rewrite theories

Vlad Rusu, Dorel Lucanu, Traian Serbanuta, Andrei Arusoaie, Andrei Stefanescu, Grigore Rosu

Journal

Proving Reachability-Logic Formulas Incrementally

Vlad Rusu, Andrei Arusoaie

Conference

2015

Verifying Reachability-Logic Properties on Rewriting-Logic Specifications (Extended Version)

Andrei Arusoaie, Dorel Lucanu, David Nowak, Vlad Rusu

Report

Program equivalence by circular reasoning

Dorel Lucanu, Vlad Rusu

Journal

Verifying Reachability-Logic Properties on Rewriting-Logic Specifications

Dorel Lucanu, Vlad Rusu, Andrei Arusoaie, David Nowak

Conference

Symbolic execution based on language transformation

Andrei Arusoaie, Dorel Lucanu, Vlad Rusu

Journal

Symbolic execution based on language transformation

Andrei Arusoaie, Dorel Lucanu, Vlad Rusu

Journal

2014

Language Definitions as Rewrite Theories

Andrei Arusoaie, Dorel Lucanu, Vlad Rusu, Traian Serbanuta, Andrei Stefanescu, Grigore Rosu

Conference

A Language-Independent Proof System for Mutual Program Equivalence

Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu

Conference

Program equivalence by circular reasoning

Dorel Lucanu, Vlad Rusu

Journal

2013

Symbolic Execution in the K Framework: Support and Applications

Andrei Arusoaie, Dorel Lucanu, Vlad Rusu

Talk

Program Equivalence by Circular Reasoning

Dorel Lucanu, Vlad Rusu

Conference

A Generic Framework for Symbolic Execution

Andrei Arusoaie, Dorel Lucanu, Vlad Rusu

Conference

Language-Independent Program Verification Using Symbolic Execution

Andrei Arusoaie, Dorel Lucanu, Vlad Rusu

Report

2012

A K-Based Formal Framework for Domain-Specific Modelling Languages

Vlad Rusu, Dorel Lucanu

Conference

Program Equivalence by Circular Coinduction

Dorel Lucanu, Vlad Rusu

Unpublished

A Generic Approach to Symbolic Execution

Andrei Arusoaie, Dorel Lucanu, Vlad Rusu

Report

2011

K Semantics for OCL - a Proposal for a Formal Definition for OCL

Vlad Rusu, Dorel Lucanu

Conference

K Semantics for Domain Specific Modelling Languages

Dorel Lucanu, Vlad Rusu

Talk

Projects

K Semantics for Domain Specific Modelling Languages (DSML)