Andrei Stefanescu

From FSL
Jump to: navigation, search
AndreiStefanescuPicture.jpg

Email: stefane1@illinois.edu.
Office: 2109 Siebel Center, 201 N. Goodwin Ave, Urbana, IL 61801.


I graduated in summer 2016.


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 25px-Pdf_icon.png CV Info_circle.png, 25px-Pdf_icon.png Research Statement Info_circle.png, and 25px-Pdf_icon.png Teaching Statement Info_circle.png.


Publications

Semantics-Based Program Verifiers for All Languages 
Andrei Stefanescu and Daejun Park and Shijiao Yuwen and Yilong Li and Grigore Rosu
OOPSLA'16, ACM. 2016. To appear
PDF, Matching Logic, 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

Personal tools
Namespaces

Variants
Actions
Navigation