Andrei Stefanescu

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

25px-Pdf_icon.png CV Info_circle.png

Personal tools