Matching logic: a new program verification approach. - Grigore Rosu; Andrei Stefanescu (ICSE, 2011)

MatchC: A Matching Logic Reachability Verifier Using the K Framework. - Andrei Stefanescu (K, 2011)

From Hoare Logic to Matching Logic Reachability. - Grigore Rosu; Andrei Stefanescu (FM, 2012)

Towards a Unified Theory of Operational and Axiomatic Semantics. - Grigore Rosu; Andrei Stefanescu (ICALP (2), 2012)

Checking reachability using matching logic. - Grigore Rosu; Andrei Stefanescu (OOPSLA, 2012)

Recursive proofs for inductive tree data-structures. - Parthasarathy Madhusudan; Xiaokang Qiu; Andrei Stefanescu (POPL, 2012)

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

Natural proofs for structure, data, and separation. - Xiaokang Qiu; Pranav Garg 001; Andrei Stefanescu; Parthasarathy Madhusudan (PLDI, 2013)

KJS: a complete formal semantics of JavaScript. - Daejun Park 001; Andrei Stefanescu; Grigore Rosu (PLDI, 2015)

Semantics-based program verifiers for all languages. - Andrei Stefanescu; Daejun Park 001; Shijiao Yuwen; Yilong Li; Grigore Rosu (OOPSLA, 2016)

Language definitions as rewrite theories. - Vlad Rusu; Dorel Lucanu; Traian-Florin Serbanuta; Andrei Arusoaie; Andrei Stefanescu; Grigore Rosu (J. Log. Algebraic Methods Program., 2016)

Toward language-independent program verification - Andrei Stefanescu (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)

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

A Constructor-Based Reachability Logic for Rewrite Theories. - Stephen Skeirik; Andrei Stefanescu; José Meseguer 001 (Fundam. Informaticae, 2020)

Verified Cryptographic Code for Everybody. - Brett Boston; Samuel Breese; Joey Dodds; Mike Dodds; Brian Huffman; Adam Petcher; Andrei Stefanescu (CAV (1), 2021)

A type system for extracting functional specifications from memory-safe imperative programs. - Paul He; Eddy Westbrook; Brent Carmer; Chris Phifer; Valentin Robert; Karl Smeltzer; Andrei Stefanescu; Aaron Tomb; Adam Wick; Matthew Yacavone; Steve Zdancewic (Proc. ACM Program. Lang., 2021)

Macaw: A Machine Code Toolbox for the Busy Binary Analyst. - Ryan G. Scott; Brett Boston; Benjamin Davis; Iavor S. Diatchki; Mike Dodds; Joe Hendrix; Daniel Matichuk; Kevin Quick; Tristan Ravitch; Valentin Robert; Benjamin Selfridge; Andrei Stefanescu; et al. (CoRR, 2024)