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

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

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

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

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

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

Klaus Havelund, Giles Reger and Grigore Roșu
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

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

Ș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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Daejun Park, Yi Zhang and Grigore Roșu
CAV, 2020
PDF