Publications

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

Theodoros Kasampalis, Dwight Guth, Brandon Moore, Traian Ș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

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

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

CSF 2018, IEEE, pp 204-217. 2018
PDF, KEVM, CSF 2018, BIB

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

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

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

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

Technical Report, 2019
PDF

Towards a Verified Model of the Algorand Consensus Protocol in Coq

Cornell cs.CR, 2019
PDF

Runtime Verification Past Experiences and Future Projection

Springer, 2019
PDF

Matching mu-Logic

Xiaohong Chen and Grigore Roșu
LICS'19, 2019
PDF, Matching Logic, LICS'19, BIB

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

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

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

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

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

Grigore Roșu and Andrei Ștefănescu
OOPSLA'12, ACM, pp 555-574. 2012
PDF, Matching Logic, DOI, OOPSLA'12, BIB

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

Jose Meseguer and Grigore Roșu
J. of TCS, Volume 373(3), pp 213-237. 2007
PDF, J.TCS

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)

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

Traian Șerbănuță and Grigore Roșu
WRLA'10, Springer, pp 104-122. 2010
PDF, K, DOI, WRLA'10, BIB

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

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

Theodoros Kasampalis, Dwight Guth, Brandon Moore, Traian Șerbănuță, Daniele Filaretti, Grigore Roșu and Ralph Johnson
Technical Report http://hdl.handle.net/2142/100320, July 2018
PDF, IELE, DOI, BIB