Michael Sammler will join ISTA in January 2025.
Programming Languages and Verification
Low-level systems software like operating systems or hypervisors is at the heart of modern computer systems. Such systems software often provides critical components that ensure the reliability and security of the overall system. On the flip side, this means that bugs and vulnerabilities in such low-level systems software can lead to catastrophic failures and security problems. As a consequence, detecting and preventing such bugs in low-level systems software is crucial for providing a reliable basis that the modern computer-based world can build upon.
One important approach to eliminate such bugs and vulnerabilities is formal verification. Unlike testing, which can show the presence of bugs for certain inputs, formal verification proves the absence of whole classes of bugs and vulnerabilities for all inputs by conducting a proof that the low-level program behaves as described by a high-level mathematical specification.
The Sammler group develops novel approaches and tools that enable the formal verification of real-world programs, with a focus on low-level software. To achieve this, the group builds realistic models of programming languages like C or assembly that accurately capture the nuances that programmers in low-level languages rely on (e.g., the behavior of the underlying architecture) and then develops verification methodologies that can verify real-world code against these models. The work of the group ranges from advancing the theoretical foundations of verification—for example, for reasoning about the interaction of different programming languages in the same program—to building practical verification tools that provide automatic verification while also generating machine-checkable proofs of correctness in a proof assistant.
Combining automated and foundational verification for real-world programs / Reasoning about multi-language programs / Translation validation for real-world compilers
Starting 2025 Assistant Professor, Institute of Science and Technology Austria (ISTA)
2024 Postdoctoral researcher, ETH Zurich, Switzerland
2019-2023 PhD, Max Planck Institute for Software Systems, Germany
2020-2023 Google PhD Fellowship
2023 Distinguished Paper Award at POPL
2022 Distinguished Paper Award at POPL
2021 Distinguished Paper Award and Distinguished Artifact Award at PLDI
2019 Internet Defense Prize and Distinguished Paper Award at USENIX Security