Website for the course on Automated Theorem Proving

The course is given in digital form. All information will be made available at the Moodle course website before the first lecture.

Contents:
- Theoretical foundations of calculi for automated theorem proving in first-order logic
- Correctness and completeness proofs
- Algorithms and data structures used in first-order logic theorem provers
- Comparison of different approaches to first-order theorem proving
- Foundations of modern SAT and SMT solvers

Literature:
Robinson, Voronkov: Handbook of Automated Reasoning, 2 vols., North-Holland

Prerequisites:

Highly recommended is participation in the lecture “Aussagen- und Prädiketenlogik” or a similar module on propositional and first-order logic. Basic training in mathematics should be sufficient.

Modern society is increasingly dependent on large-scale software systems that are distributed, collaborative, and communication-centred. Tackling the additional complexity that is caused by distributed actors is one of the major tasks in the research area concurrency theory. To understand the behaviour of such systems, concurrency theory studies the modelling, simulation, and verification of concurrent systems. The modelling languages range from graphical approaches such as Event Structures and Petri nets to approaches that are close to programming languages such as process calculi. To analyse such systems different techniques such as type systems, model checking, and interactive theorem proving are adapted to the needs of concurrent systems and new techniques are developed. In this seminar current articles on research in the area of concurrency theory are presented and discussed.

Erste Veranstaltung: Mittwoch, 20. Oktober 2021, 09:50

Diese Veranstaltung richtet sich an Studierende, die grundlegende Kenntnisse im Design von Hardwarebeschleunigern im Rahmen eines Systems-on-Chip erhalten möchten. Im Rahmen des Praktikums erhalten Studierende umfangreiche Einblicke in relevante Themen wie:

  • Treiber für selbst erstellte Hardwarebeschleuniger
  • Einbindung von in Bluespec erstellten Beschleunigern in ein ZynqMP-SoC
  • Toolchains für Hardware- und Software-Komponenten

Die Teilnehmer werden im Rahmen des Praktikums Aufgaben zu einem typischen Einsatzgebiet von Hardwarebeschleunigung bearbeiten. Ein typisches Anwendungsgebiet eines solchen Hardwarebeschleunigers ist die Verarbeitung und Erfassung von Kamerabildern, zum Beispiel im Rahmen von Stereo Vision.


Erste Veranstaltung: Mittwoch, 20. Oktober 2021, 11:00

Moodle course for the seminar 'Extended Seminar: Systems and Machine Learning' jointly held by profs. Mezini, Kersting, Koch and Binnig

Lehrinhalte

Einführung in die Grundlagen der Computergraphik, insb. Ein- u. Ausgabegeräte, Rendering Pipeline am Beispiel von OpenGL, räumliche Datenstrukturen, Beleuchtungsmodelle, Ray Tracing, aktuelle Entwicklungen in der Computergraphik.

Vorwissen
  • Programmierkenntnisse
  • Grundlegende Algorithmen und Datenstrukturen
  • Lineare Algebra
  • Analysis
  • Inhalte der Vorlesung Visual Computing
Personen
Dozent: Prof. Dr. techn. Fellner
Betreuung: David Spitzenberg, Daniel Ströter
Erste Veranstaltung: Montag, 18. Oktober 2021, 09:50
Über das vorlesungsbegleitende Skript hinausgehende Informationen und Unterlagen zur Lehrveranstaltung werden über diesen Kurs bereitgestellt.
Der Einschreibeschlüssel zum Kurs wird ihnen vor Beginn der Lehrveranstaltung über eine Tucan-Nachricht (Anmeldung vorausgesetzt) und in der ersten Vorlesungsstunde mitgeteilt.

Materialien zur Auffrischung von mathematischen Grundlagen werden als Wiederholungsangebot bis zum 2.11.2020 im Moodle-Kurs zur Verfügung gestellt.

Die Lehrveranstaltung wird aufgrund der Corona-Pandemie und der daraus resultierenden Regelungen der TU Darmstadt online durchgeführt werden. D.h. die Vorlesungs- und Übungsstunden finden zu den angekündigten Terminen per Online-Webinar bzw. Videokonferenz statt. Die Vorlesungstermine werden dabei auch aufgezeichnet und anschließend als Videodatei per Download zur Verfügung gestellt.

Alle Informationen, insbesondere die Links zum digitalen Lehrangebot, finden Sie im Moodle-Kurs zur Lehrveranstaltung.

Fragen zum Kurs können Sie gerne an gdr@sim.tu-darmstadt.de senden.

Kursdetails:
Voraussetzungen:
grundlegende mathematische Kenntnisse und Fähigkeiten in Linearer Algebra, Analysis mehrerer Veränderlicher und Grundlagen gewöhnlicher Differentialgleichungen

Lehrinhalte:

  • Räumliche Darstellungen und Transformationen 
  • Manipulatorkinematik 
  • Fahrzeugkinematik 
  • kinematische Geschwindigkeit und Jacobi-Matrix 
  • Bewegungsdynamik von Robotern 
  • Roboterantriebe, interne und externe Sensoren 
  • grundlegende Roboterregelungen 
  • Bahnplanung 
  • Lokalisierung und Navigation mobiler Roboter 
  • Fallstudien 
  • theoretische und praktische Übungen sowie Programmieraufgaben zur Vertiefung der Fachkenntnisse und methodischen Fähigkeiten 

Literatur:

  • vorlesungsbegleitendes Skript und Vorlesungsfolien 

Umfassende Übersicht der Robotik:
  • B. Siciliano, O. Khatib: Springer Handbook of Robotics, Springer Verlag 

zu einzelnen Themen der Lehrveranstaltung:
  • J.J. Craig: Introduction to Robotics: Mechanics and Control, 3rd edition, Prentice Hall 
  • M.W. Spong, S. Hutchinson, M. Vidyasagar: Robot Modeling and Control, Wiley 
  • R. Siegwart, I.R. Nourbakhsh, D. Scaramuzza: Introduction to Autonomous Mobile Robots, MIT Press 
  • H. Choset, K.M. Lynch, S. Hutchinson, G.A. Kantor,W. Burgard, L.E. Kavraki, S. Thrun: Principles of Robot Motion: Theory, Algorithms, and Implementations, Bradford 
  • S. Thrun,W. Burgard, D. Fox: Probabilistic Robotics, MIT Press


Erste Veranstaltung: Dienstag, 19. Oktober 2021, 12:04

In diesem Kurs werden die Lehrmaterialien zur Veranstaltung "Informationssicherheitsmanagement" (20-00-1123) verteilt.

Im Rahmen der Vorlesung wird anhand eines beispielhaften, fiktiven Unternehmens dargelegt, wie Informationssicherheit ganzheitlich in alle Prozesse des Unternehmens etabliert wird.

Dabei werden u.A. die folgenden Themengebiete betrachtet:

  • Reifegradbewertung bzgl. Informationssicherheit des Unternehmens
  • Capability Maturity Model Integration (CMMI) Framework
  • Etablierung einer Cyber Security Strategie
  • Informationssicherheits-Governance
  • Etablierung eines Informationssicherheitsmanagementsystems (ISMS) nach ISO/IEC 27001:2013 und nach IT-Grundschutz
  • Sicherheitsbewusstsein im Unternehmen (Security Awareness)
  • Key Performance Indicator zum Messen der Informationssicherheit
  • Asset Management, Informationsverbunde und Prozessanalysen
  • Schutzbedarfsfeststellungen und Business Impact Analysen
  • Qualitatives und Quantitatives Risikomanagement
  • Prozesse der Risikoanalyse, -behandlung und -überwachung
  • Vulnerability Management (Umgang mit IT-Schwachstellen in eigenen und ausgelagerten Systemen)
  • Business Continuity Management (BCM)
  • Business Continuity Planning (BCP)
  • Sicherer IT-Betrieb, Absicherung der Betriebsprozesse
  • Sichere Entwicklung
  • Absicherung von Cloud-Diensten
  • Management von Dienstleistern
  • Incident Management: Absicherung, Erkennung und Reaktion auf Sicherheitsvorfälle
  • Audit Management
  • Überprüfung der eigenen Compliance und Governance

Erste Veranstaltung: Montag, 18. Oktober 2021, 00:00

Im integrierten Projekt, das im Wintersemester beginnt und über zwei Semester (mit zusammen 8 Semesterwochenstunden (SWS) bzw. 12 Leistungspunkten/Credit Points) läuft, werden Elemente von Seminar, Praktikum und Projektarbeit im Team kombiniert. Das integrierte Projekt bietet gegenüber einem normalem Praktikum u.a. eine tiefere, theoretische Fundierung und umfassendere Ausarbeitung mit Teamarbeit. Hintergrund ist, dass die meisten Fragestellungen bei (teil-)autonomen Robotersystemen so komplex sind, dass ein sinnvoller Einblick im Rahmen nur eines einsemestrigen Praktikums nicht möglich ist.

Bitte beachten Sie, dass das aufgrund der Gesamtkonzeption eine Teilnahme allein am Seminar in der Regel nicht möglich ist.

Es gibt in der Regel zwei Aufteilungsmöglichkeiten für das zweisemestrige Integrierte Projekt, um dieses je nach Studiengang und Studienordnung einbringen zu können. Es kann nur eine von beiden gewählt werden:

(i) Integriertes Projekt Teil 1 (WiSe, 4 SWS, 6 CP) und Teil 2 (SoSe, 4 SWS, 6 CP) oder

(ii) Seminar "Aktuelle Themen der Entwicklung und Anwendung moderner Robotersysteme" (WiSe, 2 SWS, 3 CP) und Projekt-Praktikum (SoSe, 6 SWS, 9 CP).

Weitere Informationen finden Sie hier.

The Web contains more than 10 billion indexable web pages, which can be retrieved via search queries. The lecture will present Natural Language Processing (NLP) methods to (1) automatically process large amounts of unstructured text from the web and (2) analyse the use of Web data as a resource for other NLP tasks.

Processing of unstructured web content

  • Introduction
  • NLP Basics - Tokenisation, Part of Speech Tagging, Chunking, Stemming, Lemmatization
  • Web contents and their characteristics - diverse genres of web contents, e.g. personal web sites, news sites, blogs, forums, wikis
  • Web contents and their characteristics - continued

NLP applications for the web

  • Information retrieval - introduction to the basics of information retrieval
  • Web information retrieval - natural language interfaces for web information retrieval
  • Question answering (QA): Factoid QA, Knowledge Base QA, Community QA
  • Crowdsourcing
  • Reproducibility

In this seminar we debate privacy and security implications of emerging Internet of Things technologies. More specifically, we will discuss new threats, various attack techniques and how to defend against them. We will cover topics such as wearable privacy, smart cars privacy, device fingerprinting, in-store tracking, HTTP (s) Traffic analysis, privacy leaks on mobile devices, data anonymization and differential privacy Issues and emerging solutions, transparency-enhancing technologies. Participants will be given a topic and a short list of recent research papers, and will be asked to prepare a seminar talk and submit a written report. The primary goal of this seminar is to improve students’ ability to read and interpret research articles, to prepare a presentation similar to what is required at a scientific conference and to lead/participate in a scientific discussion. In the scope of this seminar, students will simulate the different phases of a scientific conference: Submission of work, review, notification/feedback, submission of the final version of the report, presentation session and possibly the chairing a session.

Voraussetzungen:
A basic understanding of computer security, networking protocols will be helpful.


Data is the oil of the 21st century and users leave more and more digital traces that are collected and evaluated by companies like Facebook or Google, as well as by intelligence services.

In this seminar, we will look at techniques for protecting privacy that allow to process sensitive data under encryption without revealing the data itself. We will investigate both the theoretical background as well as practical issues of such solutions.

Small groups of students choose a topic for which they get one to three publications that they will summarize in a written report and present in a talk.

Website for the seminar DIVe

This seminar studies topics on automatic test-case generation. The goal of test-case generation is to find test inputs that reveal bugs in the the program or to find a set of test inputs that achieve a certain coverage value. In this seminar, we look into four different types of automatic test-case generation: (1) random input generation, (2) search-based input generation, (3) input generation with symbolic execution, and (4) input generation with reachability analyses.

Under the guidance of your supervisor you will

  • use the given literature and search for additional literature to become acquainted with your topic,
  • prepare and give a presentation about your topic and afterwards discuss the topic with the other participants,
  • write a scientific report, which provides a summary of your topic.

Under the guidance of your supervisor you will

  • use the given literature and search for additional literature to become acquainted with your topic,
  • prepare and give a presentation about your topic and afterwards discuss the topic with the other participants,
  • write a scientific report, which provides a summary of your topic.

Erste Veranstaltung: Montag, 25. Oktober 2021, 15:00

In this semester, the theme of the TK seminar will be Process Mining. Process Mining is a family of techniques combining data science and business process management to support the analysis of (business) processes solely based on event logs, typically recorded by enterprise information systems. These event logs contain events about what people, machines, and organizations are really doing. By using data mining, machine learning, and other related data analysis techniques, novel insights can be obtained to address performance and compliance problems of processes.

In process mining there exist mainly three categories of analysis:

  • (1) process discovery, which deals with the reconstruction of a process model from an event log,
  • (2) conformance checking, which checks if the reality conforms to the desired way of executing the process, and
  • (3) enhancement, which enriches process models with additional information.

All three analysis categories support an analyst finding issues in a process using data-centric techniques.

The TK seminar will give a short introduction into the topic and will make you familiar with the basic terminology and techniques.


Erste Veranstaltung: Dienstag, 19. Oktober 2021, 11:40

Type systems are an integral component of many programming languages and an important technique in verification. This course provides an introduction to type systems. It discusses basic concepts, advantages and limitations of type systems.

The course deals with mostly automatic verification approaches for multi-threaded programs with shared memory. Topics of the course are:

  • Semantics of parallel programs, e.g., interleaving semantics
  • Static and dynamic approaches for data race detection
  • Techniques for deadlock detection
  • Verification of program properties (e.g., with sequentialization, bounded model checking, etc.)
  • Partial Order Reduction
  • Thread-modular verification