Research Group Computer Science 2
"Programming Languages and Verification"
|
Research
To guarantee correctness of software, especially for safety-critical and distributed systems, testing alone is insufficient, making formal verification based on mathematical proofs necessary.
The goal of our research is to automatically verify
software without needing to rely on tests or on difficult mathematical proofs written by
a human expert.
Thus, a main topic of our research is the development of methods and tools
for mechanized analysis and verification of algorithms and programs.
For example, we are developing the following tools:
AProVE
AProVE is a powerful system for automated termination, complexity, and safety proofs of several variations of term rewrite systems, as well as other formalisms including imperative, functional, and logic programs.
Learn More
KoAT
KoAT is a tool to automatically infer complexity bounds for (probabilistic) integer programs, based on an alternating modular inference of upper runtime and size bounds for program parts.
Learn More
LoAT
LoAT is a powerful tool for analyzing satisfiability of constraint Horn clauses (CHCs), and termination and worst-case complexity for transition systems.
Learn More
Upcoming Teaching Activities
-
Summary: The course gives an introduction to functional programming using the language Haskell. Moreover, we will discuss models for the semantics and the implementation of functional languages. This also includes techniques for type checking and type inference.
-
Summary: The focus of this seminar is automatic satisfiability checking of formulas. Here we consider several logics, e.g., pure propositional logic, but also extensions like quantified boolean formulas or SAT modulo theories. We will discuss both techniques for efficient satisfiability checking and practical applications in program verification. One has to write a 10 page paper about a specific
topic and present the results in a 30 minute talk.
-
Summary: In this seminar we will discuss advanced concepts of several programming languages from different programming paradigms. Besides others, we regard Java as an example of an imperative and object-oriented language, Haskell as a functional language, and Prolog as a logic programming language. The seminar is based on the lecture "Programming Concepts", where the basics of different programming languages were introduced.
Previous Teaching Activities
-
Programming Concepts
Summary: In this course we teach the basics of several
different programming languages, including imperative (object-oriented or
procedural) and declarative (logical or functional) programming languages. For
imperative programming, we consider the programming language Java. Moreover, we
present the basics of Haskell (a functional programming language) and Prolog (a
logical programming language). We also present an introduction to program
verification using the Hoare calculus.
Year: WiSe2025, WiSe2024, WiSe2023, WiSe2022, WiSe2021, WiSe2020, WiSe2019, WiSe2018, WiSe2017, WiSe2016, WiSe2014, WiSe2012, WiSe2011, WiSe2008, WiSe2007, WiSe2005, WiSe2003
-
Foundations of Logic Programming
Summary: In addition to a short introduction to the programming language Prolog, the lecture deals with the foundations of logic programming, with programming techniques in these languages, with the implementation of logic programming languages, and with their application in several areas.
Year: SuSe2025, SuSe2022, SuSe2020, SuSe2017, SuSe2015, SuSe2013, WiSe20, SuSe2008, SuSe2006
-
Foundations of Functional Programming
Summary: The course gives an introduction to functional programming using the language Haskell. Moreover, we will discuss models for the semantics and the implementation of functional languages. This also includes techniques for type checking and type inference.
Year: SuSe2024, SuSe2021, SuSe2019, SuSe2016, SuSe2014, SuSe2012, WiSe2009, SuSe2007, SoSe2005, WiSe2002
-
Term Rewriting Systems
Summary: Term rewriting systems are used for computations and mechanized proofs with equations. All functional programming languages are based on term rewriting systems, too. Therefore, term rewriting systems are used in many areas like automated program verification, specification of programs, and declarative programming.
Year: WiSe2015, SuSe2011, WiSe2006, SuSe2004, SuSe2002
-
Seminar: Verification Techniques
Summary: In this seminar we consider recent research topics in
the area of formal verification of software. One has to write a 10 page paper
about a specific
topic and present the results in a 30 minute talk.
Year: WiSe2025, WiSe2024, WiSe2023, WiSe2022, WiSe2021, WiSe2020, WiSe2019, SuSe2019, WiSe2018, WiSe2017, WiSe2016, WiSe2014, WiSe2012, WiSe2010, WiSe2009, SuSe2008, SuSe2007, SuSe2006, SuSe2005, SuSe2003, WiSe2002
-
Seminar: Satisfiability Checking
Summary: The focus of this seminar is automatic satisfiability checking of formulas. Here we consider several logics, e.g., pure propositional logic, but also extensions like quantified boolean formulas or SAT modulo theories. We will discuss both techniques for efficient satisfiability checking and practical applications in program verification. One has to write a 10 page paper about a specific
topic and present the results in a 30 minute talk.
Year: SuSe2025, SuSe2024, SuSe2022, SuSe2021, SuSe2020, SuSe2019, SuSe2017, SuSe2016, SuSe2015, SuSe2014, SuSe2013, SuSe2012, WiSe2011, WiSe2010, WiSe2009
-
Seminar: Advanced Topics in Term Rewriting
Summary: In this seminar we will discuss advanced topics in term rewriting. In particular, we will also handle techniques and tools for program analysis that are based on term rewriting. One has to write a 10 page paper about a specific topic and present the results in a 30 minute talk.
Year: WiSe2015, SuSe2011, WiSe2006, SuSe2004, SuSe2002
-
Proseminar: Advanced Programming Techniques
Summary: In this seminar we will discuss advanced concepts of several programming languages from different programming paradigms. Besides others, we regard Java as an example of an imperative and object-oriented language, Haskell as a functional language, and Prolog as a logic programming language. The seminar is based on the lecture "Programming Concepts", where the basics of different programming languages were introduced.
Year: SuSe2025, SuSe2024, SuSe2023, SuSe2022, SuSe2021, SuSe2020, SuSe2019, SuSe2017, SuSe2016, WiSe2015, SuSe2015, SuSe2014, SuSe2013, SuSe2012, SuSe2011, SuSe2010, SuSe2008, SuSe2007, SuSe2006, SuSe2005
Older Teaching Activities