Seminare

This course explores the world of unsupervised learning, that is, learning from data without access to labeled examples. We begin by examining the task of clustering, which aims to group similar instances and identify common patterns in data. Our focus then shifts to deep clustering — the integration of clustering with techniques from deep learning. These methods have gained popularity in recent years and have demonstrated strong performance on tasks involving image and text data.

Identifying clusters in high-dimensional data, such as images, text, or video, is a complex task due to the curse of dimensionality — a phenomenon where data points become increasingly similar as dimensionality grows. To address this, clustering is often preceded or accompanied by dimensionality reduction. Deep clustering addresses this challenge by combining deep representation learning with clustering-specific objectives, enabling models to learn meaningful features and groupings simultaneously.

The course covers a variety of deep clustering approaches and how they partition data. It also fosters critical discussions on the rationale behind algorithmic choices, exploring key research questions and design trade-offs

Master Seminar: Software-Verification Algorithms and Tools

Regular Slot 

Tuesday, 14-16, starting from October 14th.

Prerequisites

You should be knowledgeable on the contents of 
the bachelor lectures "Formal Specification and Verification" 
and "Formal Languages and Complexity".

Additionally, there are Master lectures concerned with software verification.
In particular, the following lectures are very beneficial for the seminar:

• Software Verification
• Verification of Parallel Programs
• Software Testing

Description

As software becomes more critical, 
the consequences of bugs or failures become more severe. 
To build trust in software systems, 
we need strong tools and techniques to prove that programs behave correctly. 
This is where software verification comes in.

In this seminar, you will be introduced to key concepts and modern techniques used to formally check the (in)correctness of software. 
These approaches complement testing: 
they aim to automatically verify that programs meet their specifications, 
detect potential bugs, 
or prove that certain errors cannot occur under any circumstances.

This course is ideal for students who are curious about topics such as static analysis, model checking,
and how these concepts are used to automatically prove software systems correct regarding a given specification.
We will discuss the ideas of selected research papers in our weekly group sessions, 
and practice presenting scientific content in written and oral form.

Preliminary Selection of Topics (may be extended):

Each topic will be introduced through a research paper. You will pick (or be assigned) one of these topics and papers.

• A Unifying View on SMT-Based Software Verification (https://doi.org/10.1007/s10817-017-9432-6)
• Symbolic Execution with CEGAR (https://doi.org/10.1007/978-3-319-47166-2_14)
• Explicit-State Software Model Checking Based on CEGAR and Interpolation (https://doi.org/10.1007/978-3-642-37057-1_11)
• Software Model Checking for People Who Love Automata (https://doi.org/10.1007/978-3-642-39799-8_2)
• Software Verification Using k-Induction (https://10.1007/978-3-642-23702-7_26)
• Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis (https://doi.org/10.1007/978-3-540-73368-3_51)
• Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification (https://doi.org/10.1007/s10817-024-09702-9)
• A Transferability Study of Interpolation-Based Hardware Model Checking for Software Verification (https://doi.org/10.1145/3660797)
• Bounded Model Checking (https://doi.org/10.3233/FAIA201002)
• Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints (https://doi.org/10.1145/512950.512973)
• Predicate Abstraction with adjustable-block encoding (https://doi.org/10.5555/1998496.1998532)
• Termination Analysis by Learning Terminating Programs (https://doi.org/10.1007/978-3-319-08867-9_53)

Expectations

• Write a seminar thesis about an assigned paper (approx. 6-8 pages incl. references), using the ACMART (two column) format.
• Give a 25-minute presentation explaining the paper's core ideas and methods, followed by a 5-minute Q&A session.

Browser extensions enhance user experience by adding functionality to web browsers, but they also present significant security risks. With access to sensitive data and system resources, extensions can become vectors for malicious activities, such as data theft, privacy invasion, and unauthorized actions. In recent years, the security of browser extensions has become a growing concern due to their increasing prevalence and capability. This seminar will explore the landscape of security analysis for browser extensions, discussing both static and dynamic analysis techniques to detect vulnerabilities and malicious behavior. It will also examine key challenges such as extension privilege misuse, obfuscation tactics, and scalability in detection methods. Through this, participants will gain insights into emerging solutions and ongoing research efforts aimed at securing browser extensions in a rapidly evolving ecosystem.

We will cover a variety of topics like…

• Malware and Vulnerability Detection
  
• Privacy and Sensitive Data
  
• Machine Learning
  
• Static and Dynamic Analysis
  

---