# Difference between revisions of "Andrei Stefanescu"

Line 16: | Line 16: | ||

{{Header | Publications}} | {{Header | Publications}} | ||

− | <pub authors='stefane1' | + | <pub authors='stefane1'/> |

## Revision as of 23:22, 27 February 2013

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.

Publications |
---|

*Checking Reachability using Matching Logic*- Grigore Rosu and
**Andrei Stefanescu**, ACM, pp 555-574. 2012**OOPSLA'12**

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

PDF, TR@UIUC *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, FM'12, , 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, ICALP'12, BIB *Recursive Proofs for Inductive Tree Data-Structures*- Parthasarathy Madhusudan, Xiaokang Qiu and
**Andrei Stefanescu**, ACM, pp 123-136, 2012**POPL'12**

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**http://hdl.handle.net/2142/28357, November 2011**Technical Report**

PDF, Matching Logic, TR@UIUC, , 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), Poster(pptx), Poster(pdf), Matching Logic, ACM, NIER ICSE'11, BIB *Matching Logic: A New Program Verification Approach*- Grigore Rosu and
**Andrei Stefanescu**. 2010**UV'10**

PDF, Slides(pptx), Slides(pdf), Matching Logic, K framework, UV'10, BIB