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.