c-semantics AT lists.cs.illinois.edu
Subject: C Semantics in K Framework
List archive
- From: "Rosu, Grigore" <grosu AT illinois.edu>
- To: "c-semantics AT cs.illinois.edu" <c-semantics AT cs.illinois.edu>
- Subject: [C-Semantics] Postdoc position at UIUC in programming languages
- Date: Fri, 23 Nov 2012 14:36:22 +0000
- Accept-language: en-US
- List-archive: <http://lists.cs.uiuc.edu/pipermail/c-semantics/>
- List-id: C Semantics in K Framework <c-semantics.cs.illinois.edu>
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
- [C-Semantics] Postdoc position at UIUC in programming languages, Rosu, Grigore, 11/23/2012
Archive powered by MHonArc 2.6.16.