We develop techniques and abstractions for building trustworthy computer systems. Ie, systems that are safe and secure. Enjoy exploring the fundamental challenges posed to security and safety by large-scale systems consisting of many threads, many nodes, and millions of lines of code written by many programmers. Seek solutions that solve real-world problems by overcoming theoretical worst-case limitations. Our work is funded by ERC.