The Workshop on AI and Theorem Provers in Mathematics (AITPM) will explore with leading experts some of the recent developments related to the use of AI and theorem provers in mathematics as well as the perspectives for such future use.
We have an open PhD position in Bridging the Gap Between Mathematical Numbers and Software Systems. To fill this position, we are seeking an enthusiastic PhD candidate with a strong background in computer science, software engineering, mathematics, or closely related fields. Expertise in formal methods such as program reasoning, programming language semantics, model checking, theorem proving, or computational logic is essential.
Once again, we are co-organizing BSides Exeter: it is set to return for its third run in April, with doors opening on main event, at The Forum, on 25th April 2026, and on 24th April 2026 a pre-event free, professional training day for those willing to contribute to charitable causes.
Dear Fellow Researchers!
Our dear colleague and friend David Basin is turning 65 in December 2026 and this has to be celebrated! We therefore organize a Festschrift and a Fest to celebrate his birthday and his extensive research contributions!
Many congratulations to Amy Stell who passed her PhD viva with minor
corrections!
Over the last few decades, deep neural networks (DNNs) have exhibited remarkable success in natural language processing (NLP). However, despite their impressive performance, DNNs have been shown to be highly vulnerable to adversarial examples, which are carefully crafted inputs with small, often imperceptible perturbations that cause models to make incorrect predictions. This vulnerability poses growing threats to security and privacy in online and safety-critical environments.
There are at least three reasons why it is desirable to perform proofs of security in a proof assistant like
Isabelle/HOL or Rocq. First, it gives us an overwhelming assurance that the proof of security is actually
a proof and not just the result of a bug in a complex verification tool.
Since 2007, the Test and Proof (TAP) conference has long been a leading venue for research on the intersection of software testing and formal verification. Now, TAP is joining the 27th International Symposium on Formal Methods (FM 2026) as a new special track. This integration places the ground-breaking work of the Test and Proofs community at the heart of the world’s premier conference on formal methods.