Grigore Rosu | Formal Methods in Software Engineering

Language definitions as rewrite theories

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

Elsevier BIB

K-Java: A Complete Semantics of Java

Denis Bogdanas and Grigore Rosu

PDF BIB

Behavioral Rewrite Systems and Behavioral Productivity

Grigore Rosu and Dorel Lucanu

PDF Futatsugi Festschrift 2014 BIB

All-Path Reachability Logic

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

PDF BIB

Language Definitions as Rewrite Theories

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

WRLA14 BIB

A Language-Independent Proof System for Mutual Program Equivalence

Stefan Ciobaca and Vlad Rusu and Grigore Rosu and Dorel Lucanu

ICFEM2014 BIB

On the Complexity of Stream Equality

Joerg Endrullis and Rena Bakhshi and Dimitri Hendriks and Grigore Rosu

FSL BIB

The Rewriting Logic Semantics Project: A Progress Report

Jose Meseguer and Grigore Rosu

FSL BIB

One-Path Reachability Logic

Andrei Stefanescu and Brandon Moore and Stefan Ciobaca and Grigore Rosu

One-Path Reachability Logic BIB

One-Path Reachability Logic

Andrei Stefanescu and Brandon Moore and Stefan Ciobaca and Grigore Rosu

PDF BIB

Maximal Causal Models for Sequentially Consistent Systems

Feng Chen and Traian Serbanuta and Grigore Rosu

PDF RV BIB

K: Overview and SIMPLE Case Study

Traian Serbanuta and Grigore Rosu

K11 BIB

The K Primer (version 3.2)

David Lazar and Chucky Ellison and Traian Serbanuta and Grigore Rosu and Andrei Arusoaie and Dorel Lucanu

K11 BIB

K Framework

Grigore Rosu

POPL2013 BIB

The K Framework Distilled

Traian Serbanuta and Grigore Rosu and Dorel Lucanu

PDF WRLA2012 BIB

From Hoare Logic to Matching Logic Reachability

Andrei Stefanescu and Grigore Rosu

See it on FSL-UIUC web page BIB

Checking Reachability using Matching Logic

Andrei Stefanescu and Grigore Rosu

See it on FSL-UIUC web page BIB

Towards a Unified Theory of Operational and Axiomatic Semantics

Andrei Stefanescu and Grigore Rosu

See it on FSL-UIUC web page BIB

Executing Formal Semantics with the K Tool

David Lazar and Chucky Ellison and Radu Mereuta and Traian Serbanuta and Grigore Rosu and Andrei Arusoaie and Dorel Lucanu

FM12 BIB

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

Traian Serbanuta and Grigore Rosu

PDF ICGT BIB

Making Maude Definitions more Interactive

Chucky Ellison and Traian Serbanuta and Grigore Rosu and Andrei Arusoaie

PDF WRLA2012 BIB

Circular Behavioral Reasoning

Grigore Rosu and Dorel Lucanu

PDF CWI BIB

Automating Coinduction with Case Analysis

Grigore Rosu and Eugen Goriac and Dorel Lucanu

ICFEM2010 BIB

On Complexity of the Behavioral Properties

Grigore Rosu and Dorel Lucanu

PDF IC0701 BIB

Circular Coinduction — A Proof Theoretical Foundation

Grigore Rosu and Dorel Lucanu

PDF CALCO BIB

CIRC : A Behavioral Verification Tool based on Circular Coinduction

Grigore Rosu and Georgiana Caltais and Eugen Goriac and Dorel Lucanu

CALCO BIB

Circular Coinduction with Special Contexts

Grigore Rosu and Dorel Lucanu

ICFEM2009 BIB

Regular Strategies as Proof Tactics for CIRC

Grigore Rosu and Gheorghe Grigoras and Dorel Lucanu

ENTCS BIB

Circ: A Circular Coinductive Prover

Grigore Rosu and Dorel Lucanu

CALCO07 BIB

Last News

Publications

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007