Difference between revisions of "Andrei Stefanescu"
From FSL
| (26 intermediate revisions by one user not shown) | |||
| Line 1: | Line 1: | ||
| + | [[Image:AndreiStefanescuPicture.jpg|none|frame]]<br/> | ||
| + | |||
Email: [mailto:stefane1@illinois.edu stefane1@illinois.edu].<br/> | Email: [mailto:stefane1@illinois.edu stefane1@illinois.edu].<br/> | ||
Office: 2109 Siebel Center, 201 N. Goodwin Ave, Urbana, IL 61801. | Office: 2109 Siebel Center, 201 N. Goodwin Ave, Urbana, IL 61801. | ||
| − | <div align="justify"> | + | |
| − | My research interests are Programming Languages and Formal Methods, with focus on improving software quality via program verification. | + | <div class="text" align="justify" style="color:red">I graduated in summer 2016. See my new page [http://andrei.stefanescu.io here]</div> |
| + | |||
| + | |||
| + | <div class="text" align="justify"> | ||
| + | My research interests are Programming Languages and Formal Methods, with focus on improving software quality via program verification. Specifically, I work on techniques for automatically building efficient correct-by-construction program verifiers from operational semantics. I am the main developer of the [http://github.com/kframework/k K verification infrastructure], which uses these techniques and existing operational semantics to yield automatic program verifiers for these languages (such as those of [http://github.com/kframework/c-semantics C], [http://github.com/kframework/java-semantics Java], and [http://github.com/kframework/javascript-semantics JavaScript]). I also work on techniques for automated reasoning about heap-manipulating programs implementing complex data-structures. | ||
</div> | </div> | ||
| − | <div align="justify"> | + | |
| + | <div class="text" 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]. | ||
</div> | </div> | ||
| + | |||
I am on the job market. Here are 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 are my {{pdf|AndreiStefanescu_CV.pdf|CV}}, {{pdf|AndreiStefanescu_Research_Statement.pdf|Research Statement}}, and {{pdf|AndreiStefanescu_Teaching_Statement.pdf|Teaching Statement}}. | ||
| + | |||
{{Header | Publications}} | {{Header | Publications}} | ||
<pubbib authors='Andrei Stefanescu'/> | <pubbib authors='Andrei Stefanescu'/> | ||
Latest revision as of 01:32, 17 October 2016
Email: stefane1@illinois.edu.
Office: 2109 Siebel Center, 201 N. Goodwin Ave, Urbana, IL 61801.
I graduated in summer 2016. See my new page here
My research interests are Programming Languages and Formal Methods, with focus on improving software quality via program verification. Specifically, I work on techniques for automatically building efficient correct-by-construction program verifiers from operational semantics. I am the main developer of the K verification infrastructure, which uses these techniques and existing operational semantics to yield automatic program verifiers for these languages (such as those of C, Java, and JavaScript). I also work on techniques for automated reasoning about heap-manipulating programs implementing complex data-structures.
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.
I am on the job market. Here are 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
CSF 2018, IEEE, pp 204-217. 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
OOPSLA'16, ACM, pp 74-91. 2016
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
J.LAMP, Volume 85(1, Part 1), pp 98-120. 2016
PDF, project, DOI, J.LAMP, BIB - KJS: A Complete Formal Semantics of JavaScript
- Daejun Park and Andrei Stefanescu and Grigore Rosu
PLDI'15, ACM, pp 346-356. 2015
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
RTA'14, LNCS 8560, pp 425-440. 2014
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
WRLA'14, LNCS 8663, pp 97-112. 2014
PDF, K, DOI, WRLA'14, BIB - Natural Proofs for Structure, Data, and Separation
- Xiaokang Qiu and Pranav Garg and Andrei Stefanescu and Parthasarathy Madhusudan
PLDI'13, ACM, pp 231-242. 2013
PDF, Slides(PPTX), Dryad, DOI, PLDI'13, BIB - One-Path Reachability Logic
- Grigore Rosu and Andrei Stefanescu and Stefan Ciobaca and Brandon Moore
LICS'13, IEEE, pp 358-367. 2013
PDF, Slides(PPTX), Reachability Logic, LICS'13, BIB - Low-Level Program Verification using Matching Logic Reachability
- Dwight Guth and Andrei Stefanescu and Grigore Rosu
LOLA'13. 2013
PDF, Slides(PDF), Matching Logic, LOLA'13, BIB - Checking Reachability using Matching Logic
- Grigore Rosu and Andrei Stefanescu
OOPSLA'12, ACM, pp 555-574. 2012
PDF, Slides(PPTX), Slides(PDF), Matching Logic, DOI, OOPSLA'12, BIB - From Hoare Logic to Matching Logic Reachability
- Grigore Rosu and Andrei Stefanescu
FM'12, LNCS 7436, pp 387-402. 2012
PDF, Slides(PPTX), Slides(PDF), Matching Logic, DOI, FM'12, BIB - Reachability Logic
- Grigore Rosu and Andrei Stefanescu and Stefan Ciobaca and Brandon Moore
Technical Report http://hdl.handle.net/2142/32952, Jul 2012
PDF, Reachability Logic, DOI, BIB - Towards a Unified Theory of Operational and Axiomatic Semantics
- Grigore Rosu and Andrei Stefanescu
ICALP'12, LNCS 7392, pp 351-363. 2012
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
POPL'12, ACM, pp 123-136. 2012
PDF, Dryad, DOI, POPL'12, BIB - MatchC: A Matching Logic Reachability Verifier Using the K Framework
- Andrei Stefanescu
K'11, ENTCS 304. 2011
PDF, Matching Logic, DOI, BIB - Matching Logic: A New Program Verification Approach (NIER Track)
- Grigore Rosu and Andrei Stefanescu
ICSE'11, ACM, pp 868-871. 2011
PDF, Slides(PPTX), Slides(PDF), Matching Logic, DOI, ICSE'11, BIB - Matching Logic: A New Program Verification Approach
- Grigore Rosu and Andrei Stefanescu
UV'10. 2010
Slides(PPTX), Slides(PDF), Matching Logic, UV'10
