+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Montag, 13. November 2023, 09.30 Uhr
Ort: Informatikzentrum, E3, 2. Etage, Raum 9222
Referent: Henri Lotze M.Sc.
Lehr- und Forschungsgebiet Theoretische Informatik
Thema: Going Offline -- Delays, Reservations and Predictions in Online
Computation
Abstract:
The study of classical online computation builds upon a rather simple
model. The input to a given problem is not known in advance,
decisions have to made immediately upon the arrival of a new element
and these decisions are irrevocable.
While this model is very well suitable to compute worst case bounds to
a broad range of problems, there are some problems which are not well
suited for this analysis. Naturally, problems that do not admit a
constant approximation ratio in their offline formulation do not admit
a constant competitive ratio in the worst case in the online
formulation. However, some problems that are approximable still do
not admit a constant competitive ratio when analyzed in the online
case. For a subset of these problems, such as the Online Simple
Knapsack problem and the class of general F-Node- and F-Edge-Deletion
problems, the reason for this seems to be that a single, specific bad
decision by an algorithm can be arbitrarily punished by an adversary.
In this talk, we explore modifications of the classical online model
with the aim to find natural models that on the one hand cover a large
range of problems and on the other hand work against pathological
kinds of instances that restrict an algorithm from obtaining a
constant competitive ratio. To this end, we study three modifications
of the classical online model.
The models that we study are that of "Late Accepts" -- with Advice --,
which allows to postpone decisions in online minimization problems
until a current partial solution does not uphold a certain property
anymore. The second one is that of "Reservations", in which any
decision may be postponed for a cost proportional to the gain of an
item. Finally, the model of "Bounded Predictions" allows an online
algorithm to see the complete instance in advance, with a caveat:
There is noise on the instance -- controlled by an adversary -- and
each element may actually deviate from its prediction, up to factor
that is known to the algorithm.
We are able to partially classify the advice complexity of the
complete class of both F-Node-Deletion and F-Edge-Deletion problems.
We give tight bounds on the competitive ratio for the Online Simple
Knapsack problem with Reservations for the whole range of possible
reservation costs, i.e. for a factor between 0 and 1. Finally, we give
partially tight bounds for the Online Simple Knapsack problem with
Bounded Predictions for the whole range of possible noise factors on
the size of the items.
Es laden ein: die Dozentinnen und Dozenten der Informatik
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Mittwoch, 13. Dezember 2023, 16:00 Uhr
Ort: Informatikzentrum Ahornstr. 55, Raum 5053.2 (B-IT)
Referentin: Jana Berger M.Sc.
Lehrstuhl Informatik 2
Thema: Applying Software Model Checking: Experiences and Advancements
Abstract:
We present a comprehensive investigation into the applicability of
formal methods for software model checking, with a particular emphasis
on the automotive sector.
The work is grounded in a practical study carried out with Ford Motor
Company, offering a basis for the exploration and enhancement of both
commercial and academic model checking tools.
In the first part of the study, we collaborated with Ford Motor Company
to formalise their natural language requirements for two automotive case
studies employing the commercial C code model checker, BTC EmbeddedPlatform.
Our investigation focused on the verification of auto-generated C code
from Simulink models, analysing the associated challenges and providing
practical recommendations for both engineers and tool developers.
Building on this foundation, we then applied academic C code model
checkers to the same case studies, comparing their performance
against BTC EmbeddedPlatform.
This comparison yielded a fresh set of insights and recommendations
aimed at enhancing academic model checking tools.
The second part of this work addresses the development of new tools and
methods aimed at advancing the state of the art in software model checking.
First, we designed NITWIT, a novel violation witness validator based on
C code interpretation.
This approach yields fast execution with a minimal memory footprint and
is agnostic of existing model checkers.
Next, we developed a tool for writing specifications with formal
semantics, tailored specifically for the automotive industry.
This tool is capable of auto-generating (a) specifications in Simulink,
BTC and pure C code for verification, streamlining the formal
verification process, and (b) natural language representations with
fixed semantics for stakeholders and non-experts to review and use.
Finally, to better facilitate the testing and benchmarking of C code
model checkers, we built a tool that generates C code.
The style of the generated code borrows from the two case studies, thus
providing a valuable resource for stress-testing model checkers while
respecting non-disclosure agreements, offering a wide variety of
controllable code metrics, features and transformers.
In summary, this thesis provides new and relevant insights as well as
novel tools aimed at improving the application and comparison of
software model checking, particularly in the context of the automotive
industry.
It offers practical solutions to real-world challenges, and helps to
bridge the gap between commercial and academic approaches to software
model checking.
Es laden ein: die Dozentinnen und Dozenten der Informatik
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Freitag, 08.12.2023, 13:00-14:00 Uhr
Ort: Raum 5053.1 (kleiner B-IT-Hörsaal)/Informatikzentrum, Ahornstraße 55
Referent: Herr Fabian Ohler, M. Sc.
Lehrstuhl Informatik 5
Thema: Die Rolle funktionaler Domänenmodelle in der Entwicklung allianzgetriebener Softwareplattformen
Abstract:
Organisationen können durch die Bildung von Allianzen gemeinsame Ziele verfolgen. Gestalten sie dabei zusammen eine Plattform, müssen bereits in einem frühen Stadium eine Vielzahl an Prozessen zusammengeführt und die Verteilung der Funktionen auf die Akteure geklärt und koordiniert werden.
Im Vortrag wird die methodische und technische Unterstützung für die unternehmensübergreifenden, von Kollaboration geprägten Entwurfsaktivitäten der zugehörigen Systemarchitektur am Beispiel einer Plattformentwicklung zur Kooperation öffentlicher Verkehrsträger und Verkehrsverbünde vorgestellt. Dafür wird eine empirisch ausgearbeitete Methode zur Herleitung eines funktionalen Domänenmodells und für die Weiterentwicklung zu einer Systemarchitekturbeschreibung präsentiert. Die Rolle des funktionalen Domänenmodells in diesem Kontext wird beleuchtet. Ergänzend werden Software-Werkzeuge zur Unterstützung der Entwicklungsphasen der Feinspezifikation und Validierung vorgestellt. Diese basieren auf in Experteninterviews erhobenen Erkenntnissen über die Defizite bislang eingesetzter Werkzeuge sowie daraus abgeleiteten Anforderungen. Die erarbeitete Methode wurde bereits erfolgreich in zwei Domänen eingesetzt, so dass eine Übertragbarkeit auf weitere Domänen zu erwarten ist.
Es laden ein: die Dozentinnen und Dozenten der Informatik
_______________________________
Leany Maaßen
RWTH Aachen University
Lehrstuhl Informatik 5, LuFG Informatik 5
Prof. Dr. Stefan Decker, Prof. Dr. Matthias Jarke,
Prof. Gerhard Lakemeyer Ph.D., JunProf. Dr. Sandra Geisler
Ahornstrasse 55
D-52074 Aachen
Tel: 0241-80-21509
Fax: 0241-80-22321
E-Mail: maassen(a)dbis.rwth-aachen.de
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Dienstag, 5. Dezember 2023, 13.00 Uhr
Ort: Großer b-it Raum (5053.2), Geb. E2, Informatikzentrum, Ahornstr. 55
Der Vortrag findet hybrid statt.
Zoom:
https://rwth.zoom-x.de/j/63672895840?pwd=L2ZoLzRDMzV3dzIrZ2hsNTAwaFNldz09
Meeting ID: 636 7289 5840, Passcode: 964382
Referent: Istvan Sarandi, M.Sc.
Lehrstuhl Informatik 13
Thema: Robust and Efficient Methods in Visual 3D Human Pose Estimation
Abstract:
Computer vision algorithms for perceiving humans in the real world are
crucial for several impactful emerging technologies, including self-driving
cars and mobile service robots.
In this talk, I will present three contributions to improving the state of
the art in deep learning-based 3D human pose estimation, that is,
localizing major anatomical landmarks of the human body in 3D space from
RGB images only. The central themes are robustness and efficiency, which
constitute the main challenges in robotics applications.
We start by addressing robustness to occlusions, i.e., when objects block
the line of sight between the person and the camera. After presenting the
first systematic study of how occlusions deteriorate 3D pose estimation
accuracy, we propose to mitigate the problem using an effective synthetic
occlusion data augmentation strategy.
We then turn to the problem of truncation, i.e., when only a part of the
body is within the camera's field of view. We develop a truncation-robust
heatmap representation, which also allows learned recovery of the metric
scale. Building upon this capability, I present an end-to-end learned
absolute pose estimation method called MeTRAbs, for robustly reconstructing
human poses in the camera's reference frame at state-of-the-art accuracy.
In the third part, I present the largest-scale experiment reported in the
3D pose literature to date, by merging a total of 32 datasets, in the
pursuit of improved in-the-wild generalization, outside the controlled
environments of motion capture studios. We overcome the challenge of
differently annotated datasets through a novel affine-combining autoencoder
formulation for capturing the common information in different landmark
annotation formats. Importantly, these methods can run on low-powered robot
hardware in real time.
I conclude with a discussion of possible extensions to the presented works,
as well as exciting future challenges for the field as a whole.
Es laden ein: die Dozentinnen und Dozenten der Informatik
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Freitag, 01. Dezember 2023, 09.00 Uhr
Ort: IT Center, Kopernikusstraße 6, Seminarraum 003
Referent: Jannis Klinkenberg M.Sc.
Lehrstuhl Informatik 12
Thema: Reactive Runtimes for Parallel Programming Models on Shared,
Distributed, and Heterogeneous Memory Systems
Abstract:
The persistent drive to enhance the scale and precision of scientific
simulations over the past decades has created an ever-growing demand for
computational resources. This, in turn, has catalyzed several innovations in
the architectural design and manufacturing procedures of computer systems,
such as the introduction of multi-core processors and multi-socket shared
memory systems, which are typically operated in High Performance Computing
(HPC) installations. Historically, scientific applications have primarily
been developed with the presumption of a uniform execution environment,
where every compute node and core within an installation operates at a
consistent, unchanging speed and where the execution time can be accurately
predicted. However, in the last decades, both hardware and software have
become increasingly complex and often exhibit dynamic execution behavior,
causing performance fluctuations and run time variability. Consequently, a
priori load balancing within and between compute nodes becomes increasingly
challenging in such environments. Applications as well as runtime systems
therefore demand for new techniques to be able to dynamically react to
changing execution conditions and efficiently balance the load.
This thesis presents reactive concepts, runtime implementations, and runtime
extensions designed to address the growing complexity of both hardware and
software. The objective is to provide portable, vendor-independent solutions
to improve application performance, minimize run time variability and
mitigate impending load imbalances. Locality-aware task scheduling
extensions in OpenMP improve the data locality on contemporary shared memory
NUMA architectures by dynamically identifying physical data locations and
reactively adjusting the task distribution and scheduling. Further,
continuous performance introspection combined with reactively migrating or
replicating tasks in distributed memory can efficiently detect and mitigate
emerging imbalances at execution time. Lastly, abstracting regular memory
allocation allows specifying additional requirements or hints regarding how
the data is used throughout the execution, which can be exploited to
dynamically guide the data placement on systems with heterogeneous memory.
Systematic evaluations demonstrate the effectiveness of the presented
concepts and show that placing the burden on runtime systems to proficiently
handle these low-level aspects is crucial to achieve high performance on
current and future architectures.
Es laden ein: die Dozentinnen und Dozenten der Informatik
Das war ein Fehlversuch.
Sorry M. Nagl
Von: Nagl, Manfred
Gesendet: Mittwoch, 25. Oktober 2023 16:34
An: Vortraege(a)informatik.rwth-aachen.de
Betreff:
Prof. Dr.-Ing. Dr. h.c. Manfred Nagl, Emeritus
Lehrstuhl Software Engineering
RWTH Aachen University
52074 Aachen
Tel. +49 241 8021350
Mobil +49 171 5463727
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Freitag, 20. Oktober 2023, 15.30 Uhr
Ort: Seminarraum Informatik 4 (COMSYS) - 9007, E3, Ahornstr. 55 [1]
Digtaler Zugang (hybrider Vortrag): https://rwth.zoom-x.de/j/69772277508?pwd=SU5qN1FPVXI5V3UwakYydnBUUW1Ldz09
(Meeting-ID: 697 7227 7508 Kenncode: 031824)
Referent: Roman Matzutt M.Sc.
Lehrstuhl Informatik 4 (COMSYS)
Thema: Demystifying and Adjusting the Promises of Blockchain-based Data
Management in the Permissionless Setting
Abstract:
The digital currency Bitcoin introduced the blockchain as a data
structure for establishing consensus in a decentralized manner.
Since then, blockchain technology generalized to immutably recording
arbitrary events and data, now allowing more general online
interactions between distrusting users. This interaction model sparked
a tremendous interest in blockchain technology, its potential,
and applications. However, the identification of multiple shortcomings
has since dampened this initial spirit of optimism.
Our research focuses on deepening the understanding of these
shortcomings, improving upon them, and gauging the true potential for
blockchain-backed applications despite these limitations. We take a
data-driven perspective to assess the security and longevity of
permissionless blockchains, such as Bitcoin, where anybody can access
the blockchain's full history and propose new data to be appended.
Here, we identify two core challenges: First, the ability of malicious
actors to irrevocably append illicit content to a blockchain implies
required moderation capabilities despite the desired immutability.
Second, the need for massively replicating the full and ever-growing
blockchain history poses significant scalability challenges.
We tackle these challenges with four contributions. First, we
systematically analyze the phenomenon of blockchain content insertion,
showing that inserting illicit content can create devastating
consequences. Second, we explore means to mitigate these consequences
by considering strategies to prevent content insertion and by proposing
a new redactable blockchain for the swift and transparent removal of
unwanted content. Third, we address the challenge of ever-growing
blockchain sizes by proposing a gradually deployable block-pruning
scheme that is retrofittable to Bitcoin and enables users to
retroactively reduce their storage requirements.
Finally, our fourth contribution shows that permissionless blockchains
still hold an untapped potential for fueling novel applications by
demonstrating how Bitcoin can help securely bootstrapping decentralized
anonymity services.
Overall, we shed new light on the potential impact of the data
persisted on blockchains and widen the scope for resilient and durable
blockchain designs for data management tasks.
Es laden ein: die Dozentinnen und Dozenten der Informatik
[1] https://www.comsys.rwth-aachen.de/fileadmin/misc/how-to-get-to-comsys.pdf
+**********************************************************************
*
*
*Einladung
*
*
*
*Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Donnerstag, 12. Okt. 2023, 09:00 Uhr Ort: Informatikzentrum der
RWTH Aachen University, Gebäude E3, 2. Etage, Raum 9222 Referent: Jera
Hensel, M.Sc. Lehr- und Forschungsgebiet Informatik 2 Thema: Automated
Termination Analysis of C Programs Abstract:
The termination behavior of a program is a crucial property when
reasoning about its correctness and safety. Non-termination and also
undesired termination can lead to serious consequences such as system
crashes and security vulnerabilities. Therefore, we are interested in
techniques to (dis)prove termination of programs to make software
systems more secure and reliable. Analyzing the termination behavior of
C programs is especially challenging since C combines concepts of higher
programming languages with pointers and explicit memory management.
In this talk, we summarize our improvements of a termination analysis
approach that is especially powerful for C programs with memory
allocation and explicit pointer arithmetic, but which was limited to
rather small non-recursive programs without recursive data structures,
where all integers were interpreted as unbounded (mathematical)
integers. This approach uses symbolic execution with abstraction to
convert the analyzed program to an integer transition system (ITS) with
the property that termination of this ITS implies termination of the C
program. Thus, after this transformation, existing techniques for ITSs
can be applied to prove termination of the program. We lift the above
mentioned restrictions by new techniques that only require adaptions of
the symbolic execution rules and the abstraction methods, but use the
same transformation to ITSs as before. Moreover, we briefly show how
this approach is modified to prove non-termination. We implemented all
extensions in our tool AProVE and evaluate them in comparison with other
leading termination tools.
Es laden ein: die Dozentinnen und Dozenten der Informatik --
Elke Ohlenforst
Softwaremodellierung und Verifikation
Lehrstuhl Informatik 2, RWTH Aachen
Ahornstr. 55, D-52074 Aachen/Germany
Tel.: +49 (0)241 80-21201
email:ohlenforst@informatik.rwth-aachen.de
https://moves.rwth-aachen.de/
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Donnerstag, 14. September 2023, 15.00 Uhr
Ort: Informatikzentrum, H, 2. Etage, Raum 2202.
Referent: Dzenan Dzafic, M. Sc.
Lehrstuhl Informatik 11 (Embedded Software)
Thema: Fahrassistenz für Elektrorollstühle
Abstract:
In der heutigen Gesellschaft unterstützen Smartphone-Apps die Menschen in den meisten Bereichen. Seien es Planungen von täglichen Aktivitäten oder die spezifische Suche nach Information. Ein weiterer sehr großer Anwendungsbereich ist die Frage: “Wie kommt ein Mensch von A nach B?”. Bei den meisten Menschen kommen Navigationsapps wie z.B. Google-Maps etc. zum Einsatz. Für über zwei Millionen der Deutschen ist dies nicht immer möglich[1] [2], da Menschen mit einer schweren Behinderung andere Anforderung haben. Denn viele Wege sind nicht barrierefrei, die Akkukapazität des Elektrollstuhls ist beschränkt und damit auch ihre Reichweite, oder der Bodenbelag ist für ihren Rollstuhl so uneben, dass eine erhöhte Kippgefahr besteht. Zusatzlich dazu bewirken einige Bodenbelage eine drastische Senkung des Komforts für den Rollstuhlfahrer, der stark darauf durchgeschüttelt wird. Genau an diesem Punkt setzt diese Arbeit mit den Projekt eNav an. eNav ist ein Navigationssysstem für Rollstuhlfahrer mit dem Ziel die Lebensqualität von Menschen mit Mobilitätseinschränkung zu erhöhen. Dabei steht neben der Barrierefreiheit auch der Energieverbrauch des Elektrorollstuhls im Vordergrund. Das System informiert den Benutzer über den Energieverbrauch, sodass dieser nicht mitten auf dem Weg stehen bleibt. Die Entwicklung des eNav Systems zeigt, wie es möglich ist das Kartenmaterial aufzubereiten, um mit eNav barrierefreies energieeffizientes Routen zu ermöglichen und was dafür notwendig ist. Die Beschaffung und Erzeugung der dafür benötigten Datenquellen spielt hier eine zentrale Rolle. Ein dafür modifizierter A*-Algorithmus sorgt dann für energieeffizientes Routen. Das Multimodale Dynamische Routing verkürzt die Reisezeit und reduziert den Energieverbrauch, indem es den öffentlichen Nahverkehr einbezieht. Eine Untersuchung zeigt, dass in der Stadt Aachen in 41% allen untersuchten Routen eine energieeffizientere Route im Vergleich zur kürzesten Route existiert. Der Benutzer kann die Vorteile von eNav mit Hilfe eines Routenplaners und einer Navigations-App nutzen.
Es laden ein: die Dozentinnen und Dozenten der Informatik
_______________________________________________
Informatik-assistenten mailing list -- informatik-assistenten(a)lists.rwth-aachen.de
To unsubscribe send an email to informatik-assistenten-leave(a)lists.rwth-aachen.de
https://lists.rwth-aachen.de/postorius/lists/informatik-assistenten.lists.r…
________________________________________________
Dzenan Dzafic, M. Sc. RWTH
RWTH Aachen University
Embedded Software (Lehrstuhl für Informatik 11)
Ahornstrasse 55, 52074 Aachen, Germany
Office: Room 2309 (Building H)
Tel.: +49 241 80 21159
Mobile: +49 173 5720384
Fax: +49 241 80 21150
Email: dzafic(a)embedded.rwth-aachen.de
Web: https://embedded.rwth-aachen.de/
**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
***********************************************************************
Zeit: Mittwoch, 20. September 2023, 14:00 Uhr
Ort: Informatikzentrum, 5053.2 (B-IT)
Zoom:https://rwth.zoom-x.de/j/63749614813
Referent: Till Hofmann, M.Sc.
Thema: Towards Bridging the Gap between High-Level Reasoning and
Execution on Robots
Abstract:
When reasoning about actions, e.g., by means of task planning or agent
programming with Golog, the robot's actions are typically modeled on an
abstract level, where complex actions such as picking up an object are
treated as atomic primitives with deterministic effects and
preconditions that only depend on the current state. However, executing
such an action on a robot is a complex task involving multiple steps
with additional temporal preconditions and timing constraints.
Furthermore, the action may be noisy, e.g., producing erroneous sensing
results and not always having the desired effects. While these aspects
are typically ignored in reasoning tasks, they need to be dealt with
during execution. In this thesis, we propose several approaches towards
closing this gap.
Based on a variant of the situation calculus that incorporates metric
time and metric temporal logic, we propose modeling the robot platform
with timed automata and temporal constraints to describe the connection
between the high-level actions and the robot platform. We then describe
two approaches towards transforming the high-level program. First, we
view the transformation as a synthesis problem, where the task is to
synthesize a controller that executes the program while satisfying the
specification, independent of the environment's choices. We show that
the synthesis problem is decidable, describe an algorithm to construct a
controller, and evaluate the approach in two robotics scenarios. While
this approach supports controlling Golog programs against a
specification with timing constraints, the synthesis problem has
non-primitive recursive complexity and therefore does not scale well.
For this reason, we describe a second approach based on some simplifying
assumptions which allow us to view the transformation problem as a
reachability problem on timed automata, which can be solved with
state-of-the-art tools. We demonstrate the effectiveness and scalability
of the approach in a number of scenarios.
Finally, we turn towards noisy sensors and effectors. Based on DS, a
probabilistic variant of the situation calculus that allows modeling the
agent's degree of belief, we describe an abstraction framework for Golog
programs with noisy actions. In this framework, a high-level and
non-stochastic program is mapped to a more detailed and stochastic
low-level program. As the high-level program is non-stochastic, we may
use non-probabilistic reasoning methods such as task planning. At the
same time, by mapping the abstract actions to low-level programs, we may
still deal with uncertainty during execution. We define a suitable
notion of bisimulation that guarantees the equivalence between the
high-level and low-level programs and demonstrate the approach with an
example.
Es laden ein: die Dozentinnen und Dozenten der Informatik
--
Stephanie Jansen
Faculty of Mathematics, Computer Science and Natural Sciences
HLTPR - Human Language Technology and Pattern Recognition
RWTH Aachen University
Theaterstraße 35-39
D-52062 Aachen
Tel: +49 241 80-21601
sek(a)hltpr.rwth-aachen.de
www.hltpr.rwth-aachen.de