Selected Extended Papers of ITP 2022

June Andronick is CEO and co-founder of Proofcraft, providing commercial support for software verification in general and the seL4 microkernel verification in particular. She is also CEO of the seL4 Foundation, and conjoint Professor at UNSW Sydney. Her technical expertise is in increasing the reliability of critical software systems, by mathematically proving that the code behaves as expected and satisfies security and safety requirements. She previously led the Trustworthy Systems group, world-leading in the area of verified operating systems software, known worldwide for the formal verification of the seL4 microkernel.

Jasmin Blanchette is a professor of Theoretical Computer Science and Theorem Proving at Ludwig-Maximilians-Universität München, where he serves as the Dean of Studies for Computer Science. He is also a guest researcher in the VeriDis group at Loria in Nancy and in the Automation of Logic group at Max-Planck-Institut für Informatik in Saarbrücken. Prof. Dr. Jasmin Blanchette is the Editor-in-Chief of the Journal of Automated Reasoning. jasmin.blanchette@ifi.lmu.de.

Leonardo de Moura is a Senior Principal Researcher at Microsoft in the RiSE group. He joined Microsoft in 2006, and before that, he was a Computer Scientist at SRI International. He works with theorem proving and automated reasoning. In 2010, he received the Haifa Verification Award for his work on automated reasoning. In 2014, one of his articles, “Z3: an efficient SMT solver,” was nominated as the most influential tool paper in the first 20 years of TACAS. In 2015, Z3 received the Programming Languages Software Award from the ACM. He received the Herbrand award in 2019 to recognize his numerous and vital contributions to SMT solving.