Skip to main content

Michael Sammler will join ISTA in January 2025.

Sammler Group

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.

Open Positions

PhD student and postdoc positions are available!
Prospective PhD students: please apply through
Prospective postdoctoral fellows: please contact

Current Projects

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

Selected Distinctions

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

Additional Information

Download CV

theme sidebar-arrow-up
Back to Top