[PRL] Fwd: Postdoc position at UIUC in programming languages

Pete Manolios pete at ccs.neu.edu
Fri Nov 23 13:10:46 EST 2012


FYI


---------- Forwarded message ----------
From: Rosu, Grigore <grosu at illinois.edu>
Date: Fri, Nov 23, 2012 at 9:56 AM
Subject: Postdoc position at UIUC in programming languages
To: "matthias at ccs.neu.edu" <matthias at ccs.neu.edu>, "pete at ccs.neu.edu"
<pete at ccs.neu.edu>


Dear Matthias and Pete,

I would be grateful if you could forward this message to your group
and collaborators.  Also, any
suggestions about where to look for good candidates are more than welcome.

Thank you,
Grigore

--------------------------------------

The Formal Systems Laboratory at UIUC is looking for an excellent postdoc or
researcher to work on the formal K semantics of C/LLVM and/or other low-level
languages.  The semantics will then be used for program analysis and
verification, using the novel matching logic approach and mechanical
translations of K into Coq/Isabelle/ACL2.

If interested, please contact Grigore Rosu (grosu at illinois.edu).

Here are links to related projects and background papers:
K project (http://k-framework.org);
Matching logic (http://matching-logic.org);
Existing C semantics (http://code.google.com/p/c-semantics);
Existing LLVM semantics (https://github.com/davidlazar/llvm-semantics);
popl'12 paper (http://fsl.cs.uiuc.edu/index.php/An_Executable_Formal_Semantics_of_C_with_Applications);
oopsla'12 paper:
(http://fsl.cs.uiuc.edu/index.php/Checking_Reachability_using_Matching_Logic)

Grigore Rosu
Department of Computer Science, University of Illinois at Urbana-Champaign
Email: grosu at illinois.edu, WWW: http://fsl.cs.uiuc.edu/~grosu


-- 
Pete Manolios
Northeastern University
http://www.ccs.neu.edu/home/pete



More information about the PRL mailing list