[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
Disclaimer: This message does NOT include the word "types" in it, as requested on the types list webpage, but the successful candidate will also need to define a static semantics of C/LLVM. -------------------------------------------------------------------------------------------- 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 (gr...@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: gr...@illinois.edu, WWW: http://fsl.cs.uiuc.edu/~grosu