The Programming Languages, Logic, and Software Security section advances the foundations and applications of programming languages, software verification, and security. Researchers develop new models, logics, and analysis techniques to ensure software reliability, protect against vulnerabilities, and improve programming productivity. By combining expertise in both theory and application of mathematical modeling, type theory, formal methods, and program analysis, our researchers explore how software can be made safer, more efficient, and easier to develop.

A key focus is on designing tools and frameworks that enhance software quality - whether through verification techniques that prove correctness and security of programs, programming language innovations that prevent security flaws, or scalable analysis methods for large-scale systems. These tools and frameworks help ensure that critical infrastructure remains resilient to attacks and data breaches.

With a strong foundation in theoretical computer science and a commitment to real-world impact, our researchers collaborate with industry and academia to shape the future of reliable and secure computing.

This section is a combination of the two research group Logic and Semantics and Programming Languages.