June Andronick is an invited speaker to FM'19
2019-06-06 FM '19 is the third world congress on Formal Methods (held every 10 years). It's is in Porto this October, where our research group leader June Andronick is an invited speaker! You can learn more about FM'19 from this video.

Thomas Sewell is a 2019 CORE Award Winner!

2019-05-06 CORE (Computing Research & Education) have awarded Thomas Sewell the John Makepeace Bennett Award for the Australasian Distinguished Doctoral Dissertation! Thomas' PhD on binary translation validation is a breakthrough in formal verification: it manages to prove that the binary code emitted by a standard gcc compiler correctly implements the semantics of the input C program. His tool chain produces a separate proof for each input program -- when gcc produces correct output, the tool confirms with a proof, and when gcc produces incorrect output, it rejects. This is highly significant, as it means that the compiler no longer has to be trusted, and an off-the-shelf low-assurance compiler can be used to produce high-assurance code. The tool chain and methods developed in Thomas' PhD have further applications beyond binary verification. In particular, it enables making an analysis for worst-case execution time (WCET) to be more precise and highly assured.

Yuval Yarom and co-authors win Distinguished Paper Award at 40th IEEE Symposium on Security and Privacy
2019-05-03 The Distinguished Paper Award at 40th IEEE Symposium on Security and Privacy has been awarded to the "Spectre Attacks: Exploiting Speculative Execution" paper, which features Trustworthy Systems' own Yuval Yarom as a co-author. Congratulations!

2019-03-03 Johannes Aman Pohjola has won best paper at FORTE and at the DisCoTeC federated conference

Johannes Aman Pohjola has won best paper at FORTE 2019 and at the DisCoTeC 2019 federated conference. The paper covers the standard theoretical models of concurrent systems with explicit communication channels, such as the pi-calculus, which give rise to symmetric and transitive connectivity between processes. That is, if I can send a message to you, it follows that you can send a message to me, and that I can send a message to anyone you can send to. In this paper, this somewhat unrealistic assumption is relaxed by developing a more general model where channels can denote any connectivity relation, including one-way connections or connections that change over time. Congratulations Johannes!

Tony Hosking wins ARC DP grant on “Verified concurrent memory management on modern processors".
2018-12-03 Tony Hosking wins ARC DP grant on “Verified concurrent memory management on modern processors", which relates to the MicroVM project and CakeML project. Congratulations!