Research Group Computer Science 2

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:

Team

Head:

Research Assistants:

Room 4208	Name	Phone	E-Mail
	Nils Lommen, MSc	80-21214	lommen@cs.rwth-aachen.de
	Éléanore Meyer, MSc	80-21214	eleanore.meyer@cs.rwth-aachen.de

Room 4209	Name	Phone	E-Mail
	Dr. Florian Frohn	80-21241	florian.frohn@cs.rwth-aachen.de
	Jan-Christoph Kassing, MSc	80-21241	kassing@cs.rwth-aachen.de
	Moritz Leven Rosarius, MSc	80-21241	leven@cs.rwth-aachen.de

There are numerous former research assistants, who developed many important contributions.

Current 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.

• Seminar: Verification Techniques

  Summary: In this course 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.

Previous Teaching Activities

• Programming Concepts

  Year: WiSe2024, WiSe2023, WiSe2022, WiSe2021, WiSe2020, WiSe2019, WiSe2018, WiSe2017, WiSe2016, WiSe2014, WiSe2012, WiSe2011, WiSe2008, WiSe2007, WiSe2005, WiSe2003

• Foundations of Logic Programming

  Year: SuSe2025, SuSe2022, SuSe2020, SuSe2017, SuSe2015, SuSe2013, WiSe20, SuSe2008, SuSe2006

• Foundations of Functional Programming

  Year: SuSe2024, SuSe2021, SuSe2019, SuSe2016, SuSe2014, SuSe2012, WiSe2009, SuSe2007, SoSe2005, WiSe2002

• Term Rewriting Systems

  Year: WiSe2015, SuSe2011, WiSe2006, SuSe2004, SuSe2002

• Seminar: Verification Techniques

  Year: WiSe2024, WiSe2023, WiSe2022, WiSe2021, WiSe2020, WiSe2019, SuSe2019, WiSe2018, WiSe2017, WiSe2016, WiSe2014, WiSe2012, WiSe2010, WiSe2009, SuSe2008, SuSe2007, SuSe2006, SuSe2005, SuSe2003, WiSe2002

• Seminar: Satisfiability Checking

  Year: SuSe2025, SuSe2024, SuSe2022, SuSe2021, SuSe2020, SuSe2019, SuSe2017, SuSe2016, SuSe2015, SuSe2014, SuSe2013, SuSe2012, WiSe2011, WiSe2010, WiSe2009

• Seminar: Advanced Topics in Term Rewriting

  Year: WiSe2015, SuSe2011, WiSe2006, SuSe2004, SuSe2002

• Proseminar: Advanced Programming Techniques

  Year: SuSe2025, SuSe2024, SuSe2023, SuSe2022, SuSe2021, SuSe2020, SuSe2019, SuSe2017, SuSe2016, WiSe2015, SuSe2015, SuSe2014, SuSe2013, SuSe2012, SuSe2011, SuSe2010, SuSe2008, SuSe2007, SuSe2006, SuSe2005

Older Teaching Activities

• Formal Systems, Automata, Processes

  Year: SuSe2010

• Mechanized Program Verification

  Year: SuSe2003

• Seminar: Automated Termination Analysis

  Year: WiSe2011, SuSe2010, WiSe2008, WiSe2007, WiSe2005, WiSe2003

• Proseminar: IT-Security Concepts and Security in Java

  Year: SuSe2004, SuSe2003, SuSe2002