# Difference between revisions of "Andrei Stefanescu"

Line 1: | Line 1: | ||

+ | :Email: [mailto:stefane1@illinois.edu stefane1@illinois.edu]. | ||

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

+ | |||

<div align="justify"> | <div align="justify"> | ||

I am a PhD student in the Computer Science Department University of Illinois at Urbana-Champaign. I work with [[Grigore Rosu|Prof. Grigore Rosu]] in the [[Main Page|Formal Systems]] group. I also collaborate with [http://www.cs.uiuc.edu/~madhu/ Prof. Madhusudan Parthasarathy]. Before joining UIUC, I received a BSc in computer science from [http://www.acs.pub.ro/ University "Politechnica" Bucharest]. | I am a PhD student in the Computer Science Department University of Illinois at Urbana-Champaign. I work with [[Grigore Rosu|Prof. Grigore Rosu]] in the [[Main Page|Formal Systems]] group. I also collaborate with [http://www.cs.uiuc.edu/~madhu/ Prof. Madhusudan Parthasarathy]. Before joining UIUC, I received a BSc in computer science from [http://www.acs.pub.ro/ University "Politechnica" Bucharest]. | ||

Line 10: | Line 13: | ||

I am also involved in [http://www.cs.uiuc.edu/~madhu/dryad/ 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 also involved in [http://www.cs.uiuc.edu/~madhu/dryad/ 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. | ||

</div> | </div> | ||

− | |||

− | |||

I am on the job market. Here my {{pdf|AndreiStefanescu_CV.pdf|CV}}, {{pdf|AndreiStefanescu_Research_Statement.pdf|Research Statement}}, and {{pdf|AndreiStefanescu_Teaching_Statement.pdf|Teaching Statement}}. | I am on the job market. Here my {{pdf|AndreiStefanescu_CV.pdf|CV}}, {{pdf|AndreiStefanescu_Research_Statement.pdf|Research Statement}}, and {{pdf|AndreiStefanescu_Teaching_Statement.pdf|Teaching Statement}}. |

## Revision as of 22:32, 22 December 2015

- 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