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ță, Virgil Șerbănuță, Yi Zhang, Daniele Filaretti, Ralph Johnson and Grigore RoșuFM 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șuPLDI 2019, ACM, pp 1133-1148. 2019
PDF, Semantics, DOI, PLDI, BIB
P4K: A Formal Semantics of P4 and Applications
Ali Kheradmand and Grigore RoșuTechnical 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șuCSF 2018, IEEE, pp 204-217. 2018
PDF, KEVM, CSF 2018, BIB
Defining the Undefinedness of C
Chris Hathhorn, Chucky Ellison and Grigore RoșuPLDI'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șuPLDI'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șuPOPL'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șuPOPL'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șuMEMOCODE'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 ZamfirTechnical 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șuCornell cs.CR, 2019
PDF
Statistical Model Checking of RANDAO\u2019s Resilience AgainstPre-computed Reveal Strategies
Musab Alturki and Grigore RoșuFMBC, 2019. To appear
PDF
Runtime Verification Past Experiences and Future Projection
Klaus Havelund, Giles Reger and Grigore RoșuSpringer, 2019
PDF
Program Verification by Coinduction
Brandon Moore, Lucas Pena and Grigore RoșuESOP'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șuJ.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șuJ.LAMP, Volume 85(1, Part 1), pp 98-120. 2016
PDF, project, DOI, J.LAMP, BIB
Term-Generic Logic
Andrei Popescu and Grigore RoșuJournal 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șuRTA'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șuJournal 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 MooreLICS'13, IEEE, pp 358-367. 2013
PDF, Reachability Logic, LICS'13, BIB
Checking Reachability using Matching Logic
Grigore Roșu and Andrei ȘtefănescuOOPSLA'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ănescuFM'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ănescuICALP'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șuJ. 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șuJ. 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șuMarktoberdorf'16, NATO Science for Peace and Security. 2017
PDF, K, BIB
From Rewriting Logic, to Programming Language Semantics, to Program Verification
Grigore RoșuMeseguer'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șuFM'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șuK'11, ENTCS 304, pp 57-80. 2014
PDF, K, DOI, K11, BIB
A Formal Verification Tool for Ethereum VM Bytecode
Daejun Park, Yi Zhang, Manasvi Saxena, Philip Daian and Grigore RoșuESEC/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șuOOPSLA'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 YangPLDI'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ță, Virgil Șerbănuță, Daniele Filaretti, Grigore Roșu and Ralph JohnsonTechnical 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șuCAV, 2020
PDF