Andrei Stefanescu

From FSL
Revision as of 01:12, 7 November 2012 by Stefane1 (Talk | contribs)

Jump to: navigation, search

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.

Email
25px-Pdf_icon.png CV Info_circle.png
Publications

Checking Reachability using Matching Logic 
Grigore Rosu and Andrei Stefanescu
OOPSLA'12, ACM, pp 555-574. 2012
PDF, Slides(pptx), Slides(pdf), Matching Logic, OOPSLA'12, BIB
Reachability Logic 
Grigore Rosu, Andrei Stefanescu, Stefan Ciobaca and Brandon Moore
Technical Report http://hdl.handle.net/2142/32952, July 2012
PDF, TR@UIUC
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, FM'12, , 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, ICALP'12, BIB
Recursive Proofs for Inductive Tree Data-Structures 
Parthasarathy Madhusudan, Xiaokang Qiu and Andrei Stefanescu
POPL'12, ACM, pp 123-136, 2012
PDF, Slides(pptx), Slides(pdf), Dryad, ACM, POPL'12, BIB
Matching Logic Rewriting: Unifying Operational and Axiomatic Semantics in a Practical and Generic Framework 
Grigore Rosu and Andrei Stefanescu
Technical Report http://hdl.handle.net/2142/28357, November 2011
PDF, Matching Logic, TR@UIUC, , 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), Poster(pptx), Poster(pdf), Matching Logic, ACM, NIER ICSE'11, BIB
Matching Logic: A New Program Verification Approach 
Grigore Rosu and Andrei Stefanescu
UV'10. 2010
PDF, Slides(pptx), Slides(pdf), Matching Logic, K framework, UV'10, BIB

Personal tools
Namespaces

Variants
Actions
Navigation