Difference between revisions of "Andrei Stefanescu"

From FSL
Jump to: navigation, search
Line 8: Line 8:
  
 
<div align="justify">
 
<div align="justify">
I am also involved [http://www.cs.uiuc.edu/~madhu/dryad/ Dryad] is aimed at verifying programs directly based on the operational semantics of a language (without any Hoare Logics). To this end, I have implemented [http://matching-logic.org/index.php/Special:MatchCOnline MatchC], and efficient automated verifier for a C fragment. MatchC derives program properties from an operational semantics of the C fragment (defined in the [http://k-framework.org K Framework]) using the Matching Logic proof system.
+
I am also involved in [http://www.cs.uiuc.edu/~madhu/dryad/ Dryad],  
 
</div>
 
</div>
  
Line 14: Line 14:
 
:{{pdf|Andrei_Stefanescu_CV.pdf|CV}}
 
:{{pdf|Andrei_Stefanescu_CV.pdf|CV}}
  
== Publications ==
+
{{Header | Publications}}
  
 
<pub authors='stefane1'></pub>
 
<pub authors='stefane1'></pub>

Revision as of 01:02, 7 November 2012

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,

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