Martin Bodin has successfully defended his PhD on “Certified Semantics and Analysis of JavaScript”, covering his work on the formalization of JavaScript in Coq and the development of a framework to systematically derive certified abstract semantics from concrete semantics. [More…]
The Paper “Non-Interfererence through Annotated Multisemantics”, written by Gurvan Cabon and Alan Schmitt, has been accepted at the JFLA workshop. This paper defines an alternative semantics for programs that captures the notion of non-interference by tracking information flows. [More…]
Pierre Wilke has successfully defended his PhD on “Formally verified compilation of low-level C code”, covering his work on building a formally verified compiler providing the same level of guarantee as CompCert, but for C programs that perform low-level operations, in particular on the binary representation of pointers.
