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.
Publications
Research that shaped the runtime verification field
Runtime Verification is fueled by people. We are pioneers and leaders in the runtime verification community, with hundreds of publications behind us. What follows is a short, curated list.
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
P4K: A Formal Semantics of P4 and Applications
Ali Kheradmand and Grigore Roșu
Technical Report https://arxiv.org/abs/1804.01468, April 2018
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
Defining the Undefinedness of C
Chris Hathhorn, Chucky Ellison and Grigore Roșu
PLDI'15, ACM, pp 336-345. 2015
KJS: A Complete Formal Semantics of JavaScript
Daejun Park, Andrei Ștefănescu and Grigore Roșu
PLDI'15, ACM, pp 346-356. 2015
An Executable Formal Semantics of C with Applications
Chucky Ellison and Grigore Roșu
POPL'12, ACM, pp 533-544. 2012
A Formal Executable Semantics of Verilog
Patrick Meredith, Michael Katelman, Jose Meseguer and Grigore Roșu
MEMOCODE'10, IEEE, pp 179-188. 2010
Formalizing Correct-By-Construction Casper in Coq
Elaine Li, Traian Șerbănuță, Denisa Diaconescu, Grigore Roșu and Vlad Zamfir
Technical Report, 2019
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
Program Verification by Coinduction
Brandon Moore, Lucas Pena and Grigore Roșu
ESOP'18, Springer, pp 589-618. 2018
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
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
Term-Generic Logic
Andrei Popescu and Grigore Roșu
Journal of Theoretical Computer Science, Volume 577(1), pp 1-24. 2015
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
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
One-Path Reachability Logic
Grigore Roșu, Andrei Ștefănescu, Ștefan Ciobaca and Brandon Moore
LICS'13, IEEE, pp 358-367. 2013
Checking Reachability using Matching Logic
Grigore Roșu and Andrei Ștefănescu
OOPSLA'12, ACM, pp 555-574. 2012
From Hoare Logic to Matching Logic Reachability
Grigore Roșu and Andrei Ștefănescu
FM'12, LNCS 7436, pp 387-402. 2012
Towards a Unified Theory of Operational and Axiomatic Semantics
Grigore Roșu and Andrei Ștefănescu
ICALP'12, LNCS 7392, pp 351-363. 2012
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
The Rewriting Logic Semantics Project
Jose Meseguer and Grigore Roșu
J. of TCS, Volume 373(3), pp 213-237. 2007
K - A Semantic Framework for Programming Languages and Formal Analysis Tools
Marktoberdorf'16, NATO Science for Peace and Security. 2017
From Rewriting Logic, to Programming Language Semantics, to Program Verification
Meseguer's Festschrift, LNCS 9200, pp 598-616. 2015
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
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
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
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
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
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
Working on something that belongs in this list?
Talk to our team