About the Logic and Sematics Group

The Logic and Semantic (LogSem) group develops new models and logics for reasoning about correctness and security properties of software systems.

The software systems range from embedded systems and capability machine models, over distributed, concurrent, higher-order, imperative programs, to type theories underlying current and future proof assistants.

The models and logics are being applied to design, analysis and verification of key components of the software infrastructure of modern society, such as widely-used challenging data structures and algorithms; new programming languages and compilers; and cryptographic protocols. Moreover, they are also used to establish important meta-theoretic properties of programming languages (e.g., type safety and non-interference) and type theories (e.g., canonicity and normalization).

We also develop tools for machine-supported reasoning in the models and logics. The tools range from full interactive verification in proof assistants to automatic program analysis and model checking.

For more details, see the home pages of the faculty members of the group and the research page for links to current research projects.