Thread contracts for safe parallelism. - Rajesh K. Karmani; P. Madhusudan; Brandon M. Moore (PPoPP, 2011)

One-Path Reachability Logic. - Grigore Rosu; Andrei Stefanescu; Stefan Ciobaca; Brandon M. Moore (LICS, 2013)

ROSRV: Runtime Verification for Robots. - Jeff Huang 001; Cansu Erdogan; Yi Zhang; Brandon M. Moore; Qingzhou Luo; Aravind Sundaresan; Grigore Rosu (RV, 2014)

Coinductive program verification - Brandon M. Moore (2016)

KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine. - Everett Hildenbrandt; Manasvi Saxena; Nishant Rodrigues; Xiaoran Zhu; Philip Daian; Dwight Guth; Brandon M. Moore; Daejun Park 001; Yi Zhang; Andrei Stefanescu; Grigore Rosu (CSF, 2018)

Program Verification by Coinduction. - Brandon M. Moore; Lucas Peña; Grigore Rosu (ESOP, 2018)

Towards a Verified Model of the Algorand Consensus Protocol in Coq. - Musab A. Alturki; Jing Chen; Victor Luchangco; Brandon M. Moore; Karl Palmskog; Lucas Peña; Grigore Rosu (FM Workshops (1), 2019)

IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain. - Theodoros Kasampalis; Dwight Guth; Brandon M. Moore; Traian-Florin Serbanuta; Yi Zhang; Daniele Filaretti; Virgil Nicolae Serbanuta; Ralph Johnson; Grigore Rosu (FM, 2019)

All-Path Reachability Logic. - Andrei Stefanescu; Stefan Ciobaca; Radu Mereuta; Brandon M. Moore; Traian-Florin Serbanuta; Grigore Rosu (Log. Methods Comput. Sci., 2019)

VLSM: Validating Labelled State Transition and Message Production Systems. - Vlad Zamfir; Mihai Calancea; Denisa Diaconescu; Brandon M. Moore; Karl Palmskog; Traian-Florin Serbanuta; Michael Stay (CoRR, 2022)