through mathematics.
We pursue software reliability from both theoretical and practical angles—formal methods, program verification, and assurance cases. Our applications range from social infrastructure to software supply chains.
We welcome students interested in theoretical computer science and mathematical logic.
We specialize in software verification, formal methods, and assurance cases. Feel free to inquire about collaboration.
Research
More →Ensuring software safety with AI and mathematics
Using AI, mathematics, and logic to automatically assure that software behaves correctly. We focus on the safety and security of cyber-physical systems and software supply chains.
Logical foundations of software verification
Studying the logical systems used to specify and verify software correctness, with a focus on how temporal logic applies to systems with stochastic behavior.
Approaching computational complexity through logic
We study open questions in computational complexity theory through the logical framework of bounded arithmetic, aiming to clarify the relationship between proof complexity and computational efficiency.