Bio

I am Research Scientist at Facebook in Menlo Park. I am broadly interested in programming languages and formal methods, with focus on program analysis, program verification, and automated reasoning.

Previously, I received a PhD in Computer Science from University of Illinois at Urbana-Champaign (UIUC), advised by Prof. Grigore Rosu. My results include techniques for automatically building efficient correct-by-construction program verifiers directly from the operational semantics of the programming languages. I implemented these techniques in the K verification infrastructure, which together with existing operational semantics yielded automatic program verifiers for C, Java, and JavaScript. Throughout, I was a core developer of the K Framework, a domain specific language for defining operational semantics of programming languages. I also developed techniques for automated reasoning about heap-manipulating programs implementing complex data-structures. See a (slightly outdated) research statement for a more extensive summary of my work.

Before joining UIUC, I received a BSc in Computer Science from University “Politechnica” Bucharest. Before that, I won three silver medals at the International Mathematical Olympiad (IMO).

Publications

Conference Papers

Semantics-Based Program Verifiers for All Languages
Andrei Stefanescu, Daejun Park, Shijiao Yuwen, Yilong Li, Grigore Rosu
OOPSLA ’16 • pdf • project • doi

KJS: A Complete Formal Semantics of JavaScript
Daejun Park, Andrei Stefanescu, and Grigore Rosu
PLDI ’15 • pdf • project • doi

All-Path Reachability Logic
Andrei Stefanescu, Stefan Ciobaca, Radu Mereuta, Brandon Moore, Traian Florin Serbanuta, and Grigore Rosu
RTA-TLCA ’14 • pdf • presentation • doi

One-Path Reachability Logic
Grigore Rosu, Andrei Stefanescu, Stefan Ciobaca, and Brandon Moore
LICS ’13 • pdf • doi

Natural Proofs for Structure, Data, and Separation
Xiaokang Qiu, Pranav Garg, Andrei Stefanescu, and Parthasarathy Madhusudan
PLDI ’13 • pdf • doi

Checking Reachability using Matching Logic
Grigore Rosu and Andrei Stefanescu
OOPSLA ’12 • pdf • presentation • project • doi

From Hoare Logic to Matching Logic Reachability
Grigore Rosu and Andrei Stefanescu
FM ’12 • pdf • presentation • doi

Towards a Unified Theory of Operational and Axiomatic Semantics
Grigore Rosu and Andrei Stefanescu
ICALP ’12 • pdf • doi

Recursive Proofs for Inductive Tree Data-Structures
Parthasarathy Madhusudan, and Xiaokang Qiu, and Andrei Stefanescu
POPL ’12 • pdf • doi

Matching Logic: A New Program Verification Approach
Grigore Rosu and Andrei Stefanescu
ICSE/NIER ’11 • pdf • doi

Journal Articles

Language Definitions as Rewrite Theories
Vlad Rusu, Dorel Lucanu, Traian Florin Serbanuta, Andrei Arusoaie, Andrei Stefanescu, and Grigore Rosu
J.LAMP ’15 • pdf • doi

Workshop Papers

Language Definitions as Rewrite Theories
Andrei Arusoaie, Dorel Lucanu, Vlad Rusu, Traian Florin Serbanuta, Andrei Stefanescu, and Grigore Rosu
WRLA ’14 • pdf • doi

Low-Level Program Verification using Matching Logic Reachability
Dwight Guth, Andrei Stefanescu, and Grigore Rosu
LOLA ’13 • pdf

MatchC: A Matching Logic Reachability Verifier Using the K Framework
Andrei Stefanescu
K ’11 • pdf • doi

PhD Thesis

Toward Language-Independent Program Verification
Andrei Stefanescu
University of Illinois at Urbana-Champaign ’16 • pdf • presentation • doi