Publications logoPublications

Runtime Verification Inc. is fueled by people. We are pioneers and leaders in the runtime verification community, with hundreds of publications that shaped the field. This is just a short, curated list. More papers and articles can be read here.

IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain

IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain

Theodoros Kasampalis, Dwight Guth, Brandon Moore, Traian Șerbănuță, Virgil Șerbănuță, Yi Zhang, Daniele Filaretti, Ralph Johnson and Grigore Roșu

FM 2019, pp 593-610. 2019.

PDF, IELE, BIB
A Complete Formal Semantics of x86-64 User-Level Instruction Set Architecture

A Complete Formal Semantics of x86-64 User-Level Instruction Set Architecture

Sandeep Dasgupta, Daejun Park, Theodoros Kasampalis, Vikram S. Adve and Grigore Roșu

PLDI 2019, ACM, pp 1133-1148. 2019

PDF, Semantics, DOI, PLDI, BIB
P4K: A Formal Semantics of P4 and Applications

P4K: A Formal Semantics of P4 and Applications

Ali Kheradmand and Grigore Roșu

Technical Report https://arxiv.org/abs/1804.01468, April 2018

PDF, P4K, DOI, BIB
KEVM: A Complete Semantics of the Ethereum Virtual Machine

KEVM: A Complete Semantics of the Ethereum Virtual Machine

Everett Hildenbrandt, Manasvi Saxena, Xiaoran Zhu, Nishant Rodrigues, Philip Daian, Dwight Guth, Brandon Moore, Yi Zhang, Daejun Park, Andrei Ștefănescu and Grigore Roșu

CSF 2018, IEEE, pp 204-217. 2018

PDF, KEVM, CSF 2018, BIB
Defining the Undefinedness of C

Defining the Undefinedness of C

Chris Hathhorn, Chucky Ellison and Grigore Roșu

PLDI'15, ACM, pp 336-345. 2015

PDF, C Semantics, DOI, PLDI'15, BIB
KJS: A Complete Formal Semantics of JavaScript

KJS: A Complete Formal Semantics of JavaScript

Daejun Park, Andrei Ștefănescu and Grigore Roșu

PLDI'15, ACM, pp 346-356. 2015

PDF, Semantics, DOI, PLDI'15, BIB
K-Java: A Complete Semantics of Java

K-Java: A Complete Semantics of Java

Denis Bogdănaș and Grigore Roșu

POPL'15, ACM, pp 445-456. 2015

PDF, K-Java, DOI, POPL'15, BIB
An Executable Formal Semantics of C with Applications

An Executable Formal Semantics of C with Applications

Chucky Ellison and Grigore Roșu

POPL'12, ACM, pp 533-544. 2012

PDF, Semantics, DOI, POPL'12, BIB
A Formal Executable Semantics of Verilog

A Formal Executable Semantics of Verilog

Patrick Meredith, Michael Katelman, Jose Meseguer and Grigore Roșu

MEMOCODE'10, IEEE, pp 179-188. 2010

PDF, IEEE, MEMOCODE'10
Formalizing Correct-By-Construction Casper in Coq

Formalizing Correct-By-Construction Casper in Coq

Elaine Li, Traian Șerbănuță, Denisa Diaconescu, Grigore Roșu and Vlad Zamfir

Technical Report, 2019

PDF
Towards a Verified Model of the Algorand Consensus Protocol in Coq

Towards a Verified Model of the Algorand Consensus Protocol in Coq

Musab Alturki, Jing Chen, Victor Luchangco, Brandon Moore, Karl Palmskog, Lucas Pena and Grigore Roșu

Cornell cs.CR, 2019

PDF
Statistical Model Checking of RANDAO\u2019s Resilience AgainstPre-computed Reveal Strategies

Statistical Model Checking of RANDAO\u2019s Resilience AgainstPre-computed Reveal Strategies

Musab Alturki and Grigore Roșu

FMBC, 2019. To appear

PDF
Runtime Verification Past Experiences and Future Projection

Runtime Verification Past Experiences and Future Projection

Klaus Havelund, Giles Reger and Grigore Roșu

Springer, 2019

PDF
Matching mu-Logic

Matching mu-Logic

Xiaohong Chen and Grigore Roșu

LICS'19, 2019

PDF, Matching Logic, LICS'19, BIB
Program Verification by Coinduction

Program Verification by Coinduction

Brandon Moore, Lucas Pena and Grigore Roșu

ESOP'18, Springer, pp 589-618. 2018

PDF, Matching Logic, DOI, ESOP'18, BIB
Matching Logic

Matching Logic

Grigore Roșu

LMCS, Volume 13(4), pp 1-61. 2017

PDF, DOI, LMCS, BIB
A Language-Independent Proof System for Full Program Equivalence

A Language-Independent Proof System for Full Program Equivalence

Ștefan Ciobaca, Dorel Lucanu, Vlad Rusu and Grigore Roșu

J.FAOC, Volume 28(3), pp 469-497. 2016

PDF, Matching Logic, DOI, J.FAOC, BIB
Language Definitions as Rewrite Theories

Language Definitions as Rewrite Theories

Vlad Rusu, Dorel Lucanu, Traian Șerbănuță, Andrei Arusoaie, Andrei Ștefănescu and Grigore Roșu

J.LAMP, Volume 85(1, Part 1), pp 98-120. 2016

PDF, project, DOI, J.LAMP, BIB
Term-Generic Logic

Term-Generic Logic

Andrei Popescu and Grigore Roșu

Journal of Theoretical Computer Science, Volume 577(1), pp 1-24. 2015

PDF, DOI, Journal of Theoretical Computer Science, BIB
All-Path Reachability Logic

All-Path Reachability Logic

Andrei Ștefănescu, Ștefan Ciobaca, Radu Mereuță, Brandon Moore, Traian Șerbănuță and Grigore Roșu

RTA'14, LNCS 8560, pp 425-440. 2014

PDF, Matching Logic, DOI, RTA'14, BIB
On the Complexity of Stream Equality

On the Complexity of Stream Equality

Joerg Endrullis, Dimitri Hendriks, Rena Bakhshi and Grigore Roșu

Journal of Functional Programming, Volume 24(2-3), pp 166-217. 2014

PDF, CIRC, DOI, Journal of Functional Programming, BIB
One-Path Reachability Logic

One-Path Reachability Logic

Grigore Roșu, Andrei Ștefănescu, Ștefan Ciobaca and Brandon Moore

LICS'13, IEEE, pp 358-367. 2013

PDF, Reachability Logic, LICS'13, BIB
Checking Reachability using Matching Logic

Checking Reachability using Matching Logic

Grigore Roșu and Andrei Ștefănescu

OOPSLA'12, ACM, pp 555-574. 2012

PDF, Matching Logic, DOI, OOPSLA'12, BIB
From Hoare Logic to Matching Logic Reachability

From Hoare Logic to Matching Logic Reachability

Grigore Roșu and Andrei Ștefănescu

FM'12, LNCS 7436, pp 387-402. 2012

PDF, Matching Logic, DOI, FM'12, BIB
Towards a Unified Theory of Operational and Axiomatic Semantics

Towards a Unified Theory of Operational and Axiomatic Semantics

Grigore Roșu and Andrei Ștefănescu

ICALP'12, LNCS 7392, pp 351-363. 2012

PDF, Matching Logic, DOI, ICALP'12, BIB
A Semantic Approach to Interpolation

A Semantic Approach to Interpolation

Andrei Popescu, Traian Șerbănuță and Grigore Roșu

J. of TCS, Volume 410(12-13), pp 1109-1128. 2009

PDF, J.TCS, DOI, BIB
The Rewriting Logic Semantics Project

The Rewriting Logic Semantics Project

Jose Meseguer and Grigore Roșu

J. of TCS, Volume 373(3), pp 213-237. 2007

PDF, J.TCS
K - A Semantic Framework for Programming Languages and Formal Analysis Tools

K - A Semantic Framework for Programming Languages and Formal Analysis Tools

Grigore Roșu

Marktoberdorf'16, NATO Science for Peace and Security. 2017

PDF, K, BIB
From Rewriting Logic, to Programming Language Semantics, to Program Verification

From Rewriting Logic, to Programming Language Semantics, to Program Verification

Grigore Roșu

Meseguer's Festschrift, LNCS 9200, pp 598-616. 2015

PDF, K, DOI, Meseguer's Festschrift, BIB
Executing Formal Semantics with the K Tool

Executing Formal Semantics with the K Tool

David Lazar, Andrei Arusoaie, Traian Șerbănuță, Chucky Ellison, Radu Mereuță, Dorel Lucanu and Grigore Roșu

FM'12, LNCS 7436, pp 267-271. 2012

PDF, K, DOI, FM'12, BIB
The K Primer (version 3.3)

The K Primer (version 3.3)

Traian Șerbănuță, Andrei Arusoaie, David Lazar, Chucky Ellison, Dorel Lucanu and Grigore Roșu

K'11, ENTCS 304, pp 57-80. 2014

PDF, K, DOI, K11, BIB
K-Maude: A Rewriting Based Tool for Semantics of Programming Languages

K-Maude: A Rewriting Based Tool for Semantics of Programming Languages

Traian Șerbănuță and Grigore Roșu

WRLA'10, Springer, pp 104-122. 2010

PDF, K, DOI, WRLA'10, BIB
A Formal Verification Tool for Ethereum VM Bytecode

A Formal Verification Tool for Ethereum VM Bytecode

Daejun Park, Yi Zhang, Manasvi Saxena, Philip Daian and Grigore Roșu

ESEC/FSE'18, ACM. 2018.

PDF, Formally Verified Smart Contracts, ESEC/FSE'18, BIB
Semantics-Based Program Verifiers for All Languages

Semantics-Based Program Verifiers for All Languages

Andrei Ștefănescu, Daejun Park, Shijiao Yuwen, Yilong Li and Grigore Roșu

OOPSLA'16, ACM, pp 74-91. 2016

PDF, Matching Logic, DOI, OOPSLA'16, BIB
Test-Case Reduction for C Compiler Bugs

Test-Case Reduction for C Compiler Bugs

John Regehr, Yang Chen, Pascal Cuoq, Eric Eide, Chucky Ellison and Xuejun Yang

PLDI'12, ACM, pp 335-346. 2012

PDF, C-Reduce, DOI, PLDI'12, BIB
IELE: An Intermediate-Level Blockchain Language Designed and Implemented Using Formal Semantics

IELE: An Intermediate-Level Blockchain Language Designed and Implemented Using Formal Semantics

Theodoros Kasampalis, Dwight Guth, Brandon Moore, Traian Șerbănuță, Virgil Șerbănuță, Daniele Filaretti, Grigore Roșu and Ralph Johnson

Technical Report http://hdl.handle.net/2142/100320, July 2018

PDF, IELE, DOI, BIB
End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract

End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract

Daejun Park, Yi Zhang and Grigore Roșu

CAV, 2020

PDF