Formal Methods in Software Engineering

Publications

2023

Capturing constrained constructor patterns in matching logic Journal

Xiaohong Chen, Dorel Lucanu, Grigore Rosu

2022

Proof-Carrying Parameters in Certified Symbolic Execution: The Case Study of Antiunification Conference

Dorel Lucanu, Andrei Arusoaie

Supporting Algorithm Analysis with Symbolic Execution in Alk. Conference

A Matching Logic Foundation for Alk Conference

Alexandru Lungu, Dorel Lucanu

Careful Autonomous Agents in Environments With Multiple Common Resources Conference

Rodica Condurache, Et al.

Malware in the SGX Supply Chain: Be Careful When Signing Enclaves! Journal

Vlad Craciun, Andrei Mogage, Et al.

2021

Matching logic explained Journal

Xiaohong Chen, Dorel Lucanu, Grigore Rosu

Rational Synthesis in the Commons with Careless and Careful Agents Conference

Rodica Condurache, Et al.

Building Deobfuscated Applications from Polymorphic Binaries Conference

Vlad Craciun, Andrei Mogage

2020

Connecting Constrained Constructor Patterns and Matching Logic Unpublished

Xiaohong Chen, Dorel Lucanu, Grigore Rosu

2019

Unification in Matching Logic Conference

Andrei Arusoaie, Dorel Lucanu

Matching Logic Explained Conference

Dynamic Multi-Agent Systems: Conceptual Framework, Automata-Based Modelling and Verification Conference

Rodica Condurache, Et al.

2018

Unification Modulo Builtins Conference

Stefan Ciobaca, Andrei Arusoaie, Dorel Lucanu

Unification Modulo Builtins Conference

Stefan Ciobaca, Andrei Arusoaie, Dorel Lucanu

A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems Conference

Stefan Ciobaca, Dorel Lucanu

A Comparison of Open-Source Static Analysis Tools for Vulnerability Detection in C/C++ Code (SYNASC 2017 post-proceedings, to appear) Conference

Andrei Arusoaie, Stefan Ciobaca, Vlad Craciun, Dragos Gavrilut, Dorel Lucanu

Semantics-Parametric Program Equivalence (work-in-progress) - talk Talk

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

Andrei Arusoaie, David Nowak, Vlad Rusu, Dorel Lucanu

Proving Reachability Properties by Coinduction Talk

Trends in Design of Ransomware Viruses Conference

Vlad Craciun, Andrei Mogage

2017

A generic framework for symbolic execution: A coinductive approach Journal

Dorel Lucanu, Vlad Rusu, Andrei Arusoaie

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

Vlad Rusu, Andrei Arusoaie

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

Andrei Arusoaie, David Nowak, Vlad Rusu, Dorel Lucanu

A Comparison of Open-Source Static Analysis Tools for Vulnerability Detection in C/C++ Code (SYNASC 2017 pre-proceedings) Conference

Andrei Arusoaie, Stefan Ciobaca, Vlad Craciun, Dragos Gavrilut, Dorel Lucanu

2016

Language definitions as rewrite theories Journal

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

Proving Reachability-Logic Formulas Incrementally Conference

Vlad Rusu, Andrei Arusoaie

2015

K-Java: A Complete Semantics of Java Unpublished

Denis Bogdanas, Grigore Rosu

Model checking recursive programs interacting via the heap Journal

Irina Asavoae, Frank de Boer, Marcello Bonsangue, Dorel Lucanu, Jurriann Rot

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

Andrei Arusoaie, Dorel Lucanu, David Nowak, Vlad Rusu

A Complete Semantics of Java Unpublished

Program equivalence by circular reasoning Journal

Dorel Lucanu, Vlad Rusu

Verifying Reachability-Logic Properties on Rewriting-Logic Specifications Conference

Dorel Lucanu, Vlad Rusu, Andrei Arusoaie, David Nowak

Symbolic execution based on language transformation Journal

Andrei Arusoaie, Dorel Lucanu, Vlad Rusu

Symbolic execution based on language transformation Journal

Andrei Arusoaie, Dorel Lucanu, Vlad Rusu

2014

Behavioral Rewrite Systems and Behavioral Productivity Conference

Grigore Rosu, Dorel Lucanu

On Automation of OTS/CafeOBJ Method Conference

Daniel Gaina, Dorel Lucanu, Kazuhiro Ogata, Kokichi Futatsugi

On the Complexity of Stream Equality Journal

Joerg Endrullis, Dimitri Hendriks, Rena Bakhshi, Grigore Rosu

A Generic Framework for Symbolic Execution: Theory and Applications Book

Andrei Arusoaie

All-Path Reachability Logic Conference

Andrei Stefanescu, Stefan Ciobaca, Radu Mereuta, Brandon Moore, Traian Serbanuta, Grigore Rosu

Language Definitions as Rewrite Theories Conference

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

A Language-Independent Proof System for Mutual Program Equivalence Conference

Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu

Program equivalence by circular reasoning Journal

Dorel Lucanu, Vlad Rusu

2013

An Overview of Java Semantics Implementation Talk

Maximal Causal Models for Sequentially Consistent Systems Conference

Traian Serbanuta, Feng Chen, Grigore Rosu

K Framework Talk

Automatic equivalence proofs for non-deterministic coalgebras Journal

Marcello Bonsangue, Georgiana Caltais, Eugen Goriac, Dorel Lucanu, Jan Rutten, Alexandra Silva

From Small-step Semantics to Big-step Semantics, Automatically Conference

One-Path Reachability Logic Conference

Grigore Rosu, Andrei Stefanescu, Stefan Ciobaca, Brandon Moore

Programming Language Semantics using K --- true concurrency through term-graph rewriting --- Talk

Traian Serbanuta

Symbolic Execution in the K Framework: Support and Applications Talk

Andrei Arusoaie, Dorel Lucanu, Vlad Rusu

Program Equivalence by Circular Reasoning Conference

Dorel Lucanu, Vlad Rusu

A Generic Framework for Symbolic Execution Conference

Andrei Arusoaie, Dorel Lucanu, Vlad Rusu

Language-Independent Program Verification Using Symbolic Execution Report

Andrei Arusoaie, Dorel Lucanu, Vlad Rusu

Engineering Hoare Logic-based Program Verification in K Framework Conference

Andrei Arusoaie

CinK - an exercise on how to think in K Report

Dorel Lucanu, Traian Serbanuta

K: Overview and SIMPLE Case Study Conference

Grigore Rosu, Traian Serbanuta

The K Primer (version 3.2) Conference

Traian Serbanuta, Andrei Arusoaie, Unknown, Chucky Ellison, Dorel Lucanu, Grigore Rosu

Rewriting Semantics and Analysis of Concurrency Features for a C-like Language Conference

Traian Serbanuta

The Rewriting Logic Semantics Project: A Progress Report Journal

Jose Meseguer, Grigore Rosu

One-Path Reachability Logic Conference

Grigore Rosu, Andrei Stefanescu, Stefan Ciobaca, Brandon Moore

From Small-step Semantics to Big-step Semantics, Automatically Conference

2012

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

Vlad Rusu, Dorel Lucanu

Making Maude Definitions more Interactive Conference

Andrei Arusoaie, Traian Serbanuta, Chucky Ellison, Grigore Rosu

The K Framework Distilled Conference

Dorel Lucanu, Grigore Rosu, Traian Serbanuta

From Hoare Logic to Matching Logic Reachability Conference

Grigore Rosu, Andrei Stefanescu

K Definitions as Push-down Specifications Talk

Towards a Unified Theory of Operational and Axiomatic Semantics Conference

Grigore Rosu, Andrei Stefanescu

Executing Formal Semantics with the K Tool Conference

Unknown, Andrei Arusoaie, Traian Serbanuta, Chucky Ellison, Radu Mereuta, Dorel Lucanu, Grigore Rosu

Automating Abstract Syntax Tree construction for Context Free Grammars Conference

Unknown, Andrei Arusoaie

Semantics-Based WCET Analysis Unpublished

Label-Based Programming Language Semantics in K Framework with SDF Conference

K Semantics for Abstractions Unpublished

Program Equivalence by Circular Coinduction Unpublished

Dorel Lucanu, Vlad Rusu

A Generic Approach to Symbolic Execution Report

Andrei Arusoaie, Dorel Lucanu, Vlad Rusu

Interacting via the Heap in the Presence of Recursion Conference

Jurriann Rot, Irina Asavoae, Frank de Boer, Marcello Bonsangue, Dorel Lucanu

Bounded Model Checking of Recursive Programs with Pointers in K Conference

Irina Asavoae, Frank de Boer, Marcello Bonsangue, Dorel Lucanu, Jurriann Rot

A Truly Concurrent Semantics for the K Framework Based on Graph Transformations Conference

Traian Serbanuta, Grigore Rosu

Checking Reachability using Matching Logic Conference

Grigore Rosu, Andrei Stefanescu

K Tutorial Talk

Dorel Lucanu, Traian Serbanuta

2011

A decision procedure for bisimilarity of generalized regular expressions Conference

Marcello Bonsangue, Georgiana Caltais, Eugen Goriac, Dorel Lucanu, Jan Rutten, Alexandra Silva

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

Vlad Rusu, Dorel Lucanu

Context transformers in K Framework Conference

Andrei Arusoaie, Traian Serbanuta

Contributions to the K framework Talk

An Introduction to K Framework by Examples Talk

Circular Behavioral Reasoning Talk

Dorel Lucanu, Grigore Rosu

An example based introduction to K Talk

CIRC prover: an overview Talk

Using the Executable Semantics for CFG Extraction and Unfolding Conference

Mihail Asavoae, Irina Asavoae

Parsing K definitions Unpublished

Radu Mereuta, Gheorghe Grigoras

K Semantics for Domain Specific Modelling Languages Talk

Dorel Lucanu, Vlad Rusu

2010

Automating Coinduction with Case Analysis Conference

Eugen Goriac, Dorel Lucanu, Grigore Rosu

Path Directed Symbolic Execution in the K Framework Conference

Irina Asavoae, Mihail Asavoae, Dorel Lucanu

Collecting Semantics under Predicate Abstraction in the K Framework Conference

Irina Asavoae, Mihail Asavoae

2009

Rewriting Logic-Based Semantics of P Systems and the Maximal Concurrency Journal

Circular Coinduction with Special Contexts Conference

Dorel Lucanu, Grigore Rosu

Circular Coinduction -- A Proof Theoretical Foundation Conference

Grigore Rosu, Dorel Lucanu

CIRC : A Behavioral Verification Tool based on Circular Coinduction Conference

Dorel Lucanu, Eugen Goriac, Georgiana Caltais, Grigore Rosu

Model-based Testing and Analysis of Coordinated Components Journal

Gabriel Ciobanu, Dorel Lucanu

Strategy-Based Rewrite Semantics for Membrane Systems Preserves Maximal Concurrency of Evolution Rule Actions Journal

Patterns for Maude Metalanguage Applications Conference

Eugen Goriac, Georgiana Caltais, Dorel Lucanu, Oana Andrei, Gheorghe Grigoras

Automated Proving of the Behavioral Attributes Conference

Gheorghe Grigoras, Dorel Lucanu, Georgiana Caltais, Eugen Goriac

Strategy-Based Proof Calculus for Membrane Systems Conference

Oana Andrei, Dorel Lucanu

On Complexity of the Behavioral Properties Talk

Dorel Lucanu, Grigore Rosu

2008

A Rewrite Stack Machine for ROC! Conference

Georgiana Caltais, Eugen Goriac, Dorel Lucanu, Gheorghe Grigoras

Regular Strategies as Proof Tactics for CIRC Journal

Dorel Lucanu, Grigore Rosu, Gheorghe Grigoras

Circular Coinduction-based Techniques for Proving Behavioral Properties Talk

2007

Circ: A Circular Coinductive Prover Conference

Dorel Lucanu, Grigore Rosu

A rewriting logic framework for operational semantics of membrane systems Journal

Oana Andrei, Gabriel Ciobanu, Dorel Lucanu

Proving Behavioral Commutativity with CIRC Conference

However, what is the semantics of OWL? Talk

Proving coinductive properties with {CIRC} Talk

Integrated Semantics for OWL Ontologies Talk

2006

Structural Operational Semantics of P Systems Conference

Oana Andrei, Gabriel Ciobanu, Dorel Lucanu

Expressing Control Mechanisms of Membranes by Rewriting Strategies. Conference

Oana Andrei, Gabriel Ciobanu, Dorel Lucanu

RDF Framework Institutions Journal

Dorel Lucanu, Y.F. Li, Jing Song Dong

Operational Semantics and Rewriting Logic in Membrane Computing Journal

Oana Andrei, Dorel Lucanu, Gabriel Ciobanu

A specification language for coordinated objects Journal

Gabriel Ciobanu, Dorel Lucanu

Logic programming viewpoints on web ontologies Talk

Institution-independent logic programming paradigms Talk

Semantic Web Languages - Towards an Institutional Perspective Conference

Dorel Lucanu, Y.F. Li, Jing Song Dong

2005

Institution Morphisms for Relating OWL and Z Conference

Dorel Lucanu, Y.F. Li, Jing Song Dong

Specification of Coordinated Objects and Verification of Their Temporal Properties Conference

Mihai Danes, Gabriel Ciobanu, Dorel Lucanu

Executable Specifications of the P Systems Conference

Oana Andrei, Gabriel Ciobanu, Dorel Lucanu

Communicating Concurrent Objects in HiddenCCS Journal

Gabriel Ciobanu, Dorel Lucanu

Institution Morphisms for Relating OWL and Z Conference

Dorel Lucanu, Y.F. Li, Jing Song Dong

Soundness proof of Z semantics of OWL using institutions Conference

Dorel Lucanu, Y.F. Li, Jing Song Dong

On Logical Foundation of the Semantic Web Talk

On Logical Foundation of the Semantic Web. An Institution-based Approach Talk

An Institutional Perspective of Semantic Web Stack Talk

2004

Specification and Verification of Synchronizing Concurrent Objects Conference

Gabriel Ciobanu, Dorel Lucanu

Specification and Verification of Synchronizing Concurrent Objects Conference

Gabriel Ciobanu, Dorel Lucanu

Model Checking for Object Specifications in Hidden Algebra Conference

Dorel Lucanu, Gabriel Ciobanu

2003

Relaxed Models for Rewriting Logic Journal

Software Engineering using Algebraic Specification Talk

2002

Initial Logic and Induction in Algebraic Specification Journal

2000

Mixed Relations as Enriched Semiringal Categories Journal

Unknown, Dorel Lucanu, Gheorghe Stefanescu

1999

Axiomatization of the Coherence Property for Categories of Symmetries Conference

1997

Understanding CafeOBJ by examples Talk