# Andrei Stefanescu

Email: stefane1@illinois.edu.

Office: 2109 Siebel Center, 201 N. Goodwin Ave, Urbana, IL 61801.

I am a PhD student in the Computer Science Department University of Illinois at Urbana-Champaign. I work with Prof. Grigore Rosu in the Formal Systems group. I also collaborate with Prof. Madhusudan Parthasarathy. Before joining UIUC, I received a BSc in computer science from University "Politechnica" Bucharest.

My work on Matching Logic is aimed at verifying programs directly based on the operational semantics of a language (without any Hoare Logics). To this end, I have implemented MatchC, and efficient automated verifier for a C fragment. MatchC derives program properties from an operational semantics of the C fragment (defined in the K Framework) using the Matching Logic proof system.

I am also involved in Dryad, an extension of first-order logic with recursive definition. Dryad allows for efficient verification of a large class of program properties by using formula abstraction and SMT solvers.

I am on the job market. Here my CV , Research Statement , and Teaching Statement .

Publications |
---|

*KEVM: A Complete Semantics of the Ethereum Virtual Machine*- Everett Hildenbrandt and Manasvi Saxena and Xiaoran Zhu and Nishant Rodrigues and Philip Daian and Dwight Guth and Brandon Moore and Yi Zhang and Daejun Park and
**Andrei Stefanescu**and Grigore Rosu, IEEE, pp 204-217. 2018**CSF 2018**

PDF, KEVM, CSF 2018, BIB *Semantics-Based Program Verifiers for All Languages***Andrei Stefanescu**and Daejun Park and Shijiao Yuwen and Yilong Li and Grigore Rosu, ACM, pp 74-91. 2016**OOPSLA'16**

PDF, Slides(PDF), Matching Logic, DOI, OOPSLA'16, BIB*Language Definitions as Rewrite Theories*- Vlad Rusu and Dorel Lucanu and Traian Florin Serbanuta and Andrei Arusoaie and
**Andrei Stefanescu**and Grigore Rosu, Volume 85(1, Part 1), pp 98-120. 2016**J.LAMP**

PDF, project, DOI, J.LAMP, BIB *KJS: A Complete Formal Semantics of JavaScript*- Daejun Park and
**Andrei Stefanescu**and Grigore Rosu, ACM, pp 346-356. 2015**PLDI'15**

PDF, Slides(PDF), Semantics, DOI, PLDI'15, BIB *All-Path Reachability Logic***Andrei Stefanescu**and Stefan Ciobaca and Radu Mereuta and Brandon Moore and Traian Florin Serbanuta and Grigore Rosu, LNCS 8560, pp 425-440. 2014**RTA'14**

PDF, Slides(PPTX), Matching Logic, DOI, RTA'14, BIB*Language Definitions as Rewrite Theories*- Andrei Arusoaie and Dorel Lucanu and Vlad Rusu and Traian Florin Serbanuta and
**Andrei Stefanescu**and Grigore Rosu, LNCS 8663, pp 97-112. 2014**WRLA'14**

PDF, K, DOI, WRLA'14, BIB *Natural Proofs for Structure, Data, and Separation*- Xiaokang Qiu and Pranav Garg and
**Andrei Stefanescu**and Parthasarathy Madhusudan, ACM, pp 231-242. 2013**PLDI'13**

PDF, Slides(PPTX), Dryad, DOI, PLDI'13, BIB *One-Path Reachability Logic*- Grigore Rosu and
**Andrei Stefanescu**and Stefan Ciobaca and Brandon Moore, IEEE, pp 358-367. 2013**LICS'13**

PDF, Slides(PPTX), Reachability Logic, LICS'13, BIB *Low-Level Program Verification using Matching Logic Reachability*- Dwight Guth and
**Andrei Stefanescu**and Grigore Rosu. 2013**LOLA'13**

PDF, Slides(PDF), Matching Logic, LOLA'13, BIB *Checking Reachability using Matching Logic*- Grigore Rosu and
**Andrei Stefanescu**, ACM, pp 555-574. 2012**OOPSLA'12**

PDF, Slides(PPTX), Slides(PDF), Matching Logic, DOI, OOPSLA'12, BIB *From Hoare Logic to Matching Logic Reachability*- Grigore Rosu and
**Andrei Stefanescu**, LNCS 7436, pp 387-402. 2012**FM'12**

PDF, Slides(PPTX), Slides(PDF), Matching Logic, DOI, FM'12, BIB *Reachability Logic*- Grigore Rosu and
**Andrei Stefanescu**and Stefan Ciobaca and Brandon Moorehttp://hdl.handle.net/2142/32952, Jul 2012**Technical Report**

PDF, Reachability Logic, DOI, BIB *Towards a Unified Theory of Operational and Axiomatic Semantics*- Grigore Rosu and
**Andrei Stefanescu**, LNCS 7392, pp 351-363. 2012**ICALP'12**

PDF, Slides(PPTX), Slides(PDF), Matching Logic, DOI, ICALP'12, BIB *Recursive Proofs for Inductive Tree Data-Structures*- Parthasarathy Madhusudan and Xiaokang Qiu and
**Andrei Stefanescu**, ACM, pp 123-136. 2012**POPL'12**

PDF, Dryad, DOI, POPL'12, BIB *MatchC: A Matching Logic Reachability Verifier Using the K Framework***Andrei Stefanescu**, ENTCS 304. 2011**K'11**

PDF, Matching Logic, DOI, BIB*Matching Logic: A New Program Verification Approach (NIER Track)*- Grigore Rosu and
**Andrei Stefanescu**, ACM, pp 868-871. 2011**ICSE'11**

PDF, Slides(PPTX), Slides(PDF), Matching Logic, DOI, ICSE'11, BIB *Matching Logic: A New Program Verification Approach*- Grigore Rosu and
**Andrei Stefanescu**. 2010**UV'10**

Slides(PPTX), Slides(PDF), Matching Logic, UV'10