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
Are you interested in writing a Bachelor's or Master's
thesis at our research group? Writing a thesis at our research group gives you a
good insight into how to combine theoretical computer
science with practical applicability. Get in touch and write us an e-mail if you are interested! (giesl@informatik.rwth-aachen.de)
Current Teaching Activities
-
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.
-
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