Difference between revisions of "Andrei Stefanescu"

From FSL
Jump to: navigation, search
Line 16: Line 16:
 
{{Header | Publications}}
 
{{Header | Publications}}
  
<pubbib authors='Andrei Stefanescu'/>
+
<pubbib authors='andrei stefanescu'/>

Revision as of 23:50, 6 May 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.

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


Personal tools
Namespaces

Variants
Actions
Navigation