************************************************************************
*
* Einladung
*
*
* Informatik-Oberseminar
*
*
************************************************************************
Zeit: Dienstag, 26.02.2019 um 14.00 Uhr
Ort: Gebäude Informatikzentrum Hörn, Raum 5053.2 (B-IT Research School ggü.
AH 6)
Referent: Herr Dipl.-Inform. Christian Samsel
Titel: Ubiquitous Intermodal Travel Assistance
Abstract:
Global trends like urbanization, digitization, and climate change enforce
and accelerate the change of personal mobility.
Combining traditional mobility services, like trains, with emerging
services, like electric carsharing, enables fast, low-priced and
environmental-friendly journeys.
Because of the high complexity of such intermodal itineraries compared to
traditional travel, planning and conducting them requires assistance.
In this work we describe how an information system providing the required
information for intermodal traveling can be constructed.
To do so, a revised distributed system architecture and interfaces between
the components are required as well as strategies to combine public
transportation and sharing services into intermodal itineraries.
Based on these findings we show how to give personalized, intermodal route
recommendations to travelers to simplify travel planning.
Using a combination of content-based and context-aware recommender
algorithms we sort a set of intermodal itinerary provided by intermodal
travel information systems based on the travelers preferences.
The evaluation showed that a personalized travel planning is preferred over
a traditional departure time-based travel itinerary sorting.
An intermodal journeys usually includes multiple transfers between diverse
mobility services, rendering the journey complex.
To assist the traveler while on his or her way, we introduce the intermodal
mobility assistance, applying the principle of cascading information.
The cascading information principle denotes that only currently relevant
information should be conveyed to the user, and by that, simplifying the
information processing.
Intermodal implies that not only various public transportation systems are
covered but also walking directions and modern mobility schemes like
carsharing.
The traveler is assisted on the respective device he or she is using at a
specific moment.
This could be a smartphone during a bus travel, a wearable device while
walking, or a car while using a carsharing service.
In addition we show how to effectively support the traveler in situations
when the initial plan cannot be continued because of delays or disruptions
in the travel chain.
Evaluations of the respective prototypes show that the approach indeed
simplifies intermodal travel.
Es laden ein: Die Dozenten der Informatik
Lehrstuhl Informatik 5
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Dienstag, 12. Februar 2019, 15.00 Uhr
Ort: Gebäude E3, Seminarraum 118, Ahornstr. 55
Referent: Anne Gehre M.Sc.
Lehrstuhl Informatik 8
Thema: 3D Shape Analysis based on Feature Curve Networks
Abstract:
For high-level analysis of 3D shapes, we require an abstract
representation of
geometric data. Typically, this is achieved by developing descriptors on a
local pointwise level or globally on the entire shape. While point based
descriptors can be very sensitive to local changes of the shape (e.g.
noise),
global descriptors tend to be too coarse.
Feature curves trace out salient creases and crests of 3D geometric
data. They
provide an abstract representation of salient parts of the geometry and
contain
topological and global structural information about the shape as well as
geometric details. However, automatically computed feature curve
networks on
raw data can have various defects such as noise, fragmentation, or missing
data.
In this talk we present methods to asses the different abstraction
levels of a
feature curve network. This is vital in order to obtain a meaningful set of
feature curves. For this we combine local (feature curve strength, length,
parallelism, etc.) and global (density and symmetry) saliency measures and
obtain structural reoccurrence information from a raw, potentially noisy
input
data. In the context of high-level shape analysis we discuss how meaningful
feature curve networks have a highly positive impact on complex tasks
such as
the discovery of inter-surface maps.
Es laden ein: die Dozentinnen und Dozenten der Informatik
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Freitag, 8. Februar 2019, 14:00 Uhr
Ort: Raum 9222, E3, Ahornstr. 55
Referent: Benjamin Kaminski, M.Sc.
Lehrstuhl für Informatik 2
Thema: Advanced Weakest Precondition Calculi for Probabilistic Programs
Abstract:
We study quantitative reasoning about probabilistic programs. In doing so, we investigate two main aspects: The reasoning techniques themselves and the computational hardness of that reasoning.
As for the former aspect, we first give an introduction to weakest preexpectation reasoning à la McIver & Morgan - a reasoning technique for the verification of probabilistic programs that builds on Dijkstra's weakest precondition calculus for programs with nondeterminism and Kozen's probabilistic propositional dynamic logic for probabilistic programs. We then present advanced weakest-preexpectation-style calculi for probabilistic programs that enable reasoning about
- expected runtimes,
- conditional expected values and conditional probabilities, and
- expected values of mixed-sign random variables.
As with Dijkstra's calculus, our calculi are defined inductively on the program structure and thus allow for compositional reasoning on source code level. We put a special emphasis on proof rules for reasoning about loops.
The second aspect we study is the inherent computational hardness of reasoning about probabilistic programs, which is independent from the employed analysis technique. In particular, we study the hardness of approximating expected values and (co)variances as well as the hardness of deciding termination of probabilistic programs. While we study different notions of probabilistic termination, for instance almost-sure termination or termination within finite expected time (also known as positive almost-sure termination), we demonstrate that deciding termination of probabilistic programs is generally strictly harder than deciding termination of nonprobabilistic programs.
Es laden ein: die Dozentinnen und Dozenten der Informatik
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Freitag, 08. Februar 2019, 9:30 Uhr
Ort: Raum 5056, Gebäude E2, Ahornstr. 55
Referent: Dipl. Inform. Christoph Schulze
Titel: Agile Software-Produktlinienentwicklung im Kontext heterogener Projektlandschaften
Abstract:
Die Automobilindustrie sieht sich großen Herausforderungen gegenüber: Während der Markt
immer kürzere Entwicklungszyklen, höhere Qualität und günstigere Produkte fordert, steigt
gleichzeitig durch aktuelle Trends, wie autonomes Fahren oder die Digitalisierung des Fahrzeuges,
die Komplexität und der Testaufwand des Produktes.
Eine Möglichkeit erhöhte Qualität bei reduzierten Kosten zu realisieren ist durch die systematische
Wiederverwendung modularer Einheiten gegeben. Die Software-Produktlinienentwicklung
prognostiziert durch die Etablierung einer Software-Produktlinie eine deutliche Kosten und
Zeitreduktion durch intensive Wiederverwendung. Dabei birgt dieser Ansatz aber
auch deutliche Gefahren: Die Entwicklung einer wiederverwendbaren Einheit erhöht durch die
Einführung variabler Aspekte auch dessen Komplexität. Wird eine langfristige Strategie falsch
ausgerichtet, kann es schnell dazu kommen, dass sich der erhöhte Aufwand nicht rentiert, da
eine Wiederverwendung zwar technisch möglich ist, gleichzeitig aber die Nachfrage fehlt. Im
Kontext eines Zulieferers ist es außerdem deutlich schwieriger, eine eigene Strategie unabhängig
vom Kunden (OEMs) zu entwickeln.
Vergleicht man die durch die Forschung vorgeschlagenen Mechanismen zur Darstellung von
Variabilität im Lösungsraum mit der aktuell in der Industrie gelebten Praxis, wird schnell deutlich,
dass oft ein deutlicher pragmatischer Ansatz gewählt wird. Anstatt explizit Variabilität in
Entwicklungsartefakten anzugeben, werden ähnliche Artefakte von Vorgängerprojekten als Basis
kopiert und weiterentwickelt, das sogenannte Clone&Own. Dieses meist für das
aktuelle Software-Projekt im ersten Schritt sehr kostengünstige Verfahren wird allerdings oft
sehr unsystematisch durchgeführt und birgt trotz seines kurzfristigen Mehrwertes langfristige
Gefahren. Das Wissen um eine potentielle Wiederverwendung gegebener Varianten ist üblicherweise
nur in den Köpfen der Experten aus Vorgängerprojekten gegeben und droht durch Personalwechsel
sowie über Zeit verloren zu gehen. Des Weiteren ist die Wartung mehrerer Klone, die
sich während ihrer Evolution weiterentwickeln, aber trotzdem eine gemeinsame Basis besitzen,
erschwert. Insofern entsteht im ersten Moment zwar der Eindruck, dass durch unsystematisches
Clone&Own sehr effizient Wiederverwendung betrieben werden kann, die eigentlichen Vorteile
einer Software-Produktlinienentwicklung können aber nicht genutzt werden.
Innerhalb dieser Doktorarbeit wird der beschriebene Kontext im Rahmen beteiligter Industriepartner
aufgegriffen und sowohl Ansätze eines Clone&Own-Verfahrens systematisiert sowie
Methoden zur schrittweisen Migration in eine Software-Produktlinie ausgearbeitet. Dabei stehen
sowohl Verfahren zur stufenweisen (extrinsischen, schnittstellen-basierten, semantischen)
und automatischen Ähnlichkeitsanalyse als auch ein datenbankbasierte Etablierung und Wartung
einer Software-Produktlinie im Fokus.
Basierend auf Ansätzen der agilen Software-Produktlinienentwicklung wird somit ein pragmatischer
Ansatz vorgestellt, der im Kontext heterogener Projektlandschaften eines Zulieferers
eine schrittweise Überführung in eine Software-Produktlinienentwicklung ermöglicht und
gleichzeitig gegebene Normen der Automobilindustrie berücksichtigt.
Der Ansatz wird durch mehrere Werkzeuge unterstützt, die im Kontext dieser Doktorarbeit in Zusammenarbeit
mit Industriepartnern entwickelt und verwendet wurden.
Es laden ein: Die Dozenten der Informatik
************************************************************************
*
* Einladung
*
*
* Informatik-Oberseminar
*
*
************************************************************************
Zeit: Dienstag, 05.02.2019 um 9.00 Uhr
Ort: Gebäude Informatikzentrum Hörn, Raum 5053.2 (B-IT Research School ggü.
AH 6)
Referent: Herr Dipl.-Inform. Christoph Terwelp
Titel: Entwicklung eines Referenzmodells für Mobilitätsplattformen
Abstract:
Mobilität ermöglicht dem Menschen die Teilhabe am gesellschaftlichen Leben.
Der steigende Mobilitätsbedarf, die Endlichkeit der verfügbaren Ressourcen
und die aktuellen Umwelteinflüsse der Mobilität machen einen
Mobilitätswandel weg vom fossil angetriebenen Individualverkehr
unvermeidlich.
Ein vollständiger Ersatz des Individualverkehrs durch öffentliche
Personenverkehre würde jedoch zu einer erheblichen Einschränkung der
Mobilität führen. Hingegen ist eine Kombination verschiedener
Mobilitätsangebote (z. B. ÖPNV, Car-Sharing, Fernbusse) zum Erhalt der
Flexibilität in der Mobilität vielversprechend. Sie führt aber zugleich zu
einer erhöhten Komplexität bei der Nutzung, da Angebote unterschiedlicher
Mobilitätsanbieter verglichen und sowohl preislich als auch in Wegfindung
und Reisebegleitung kombiniert werden müssen. Mobilitätsplattformen sollen
die Mobilitätsangebote in einem Informationssystem zusammenführen und dem
Nutzer Funktionalitäten zur Auskunft, Buchung, Autorisierung,
Reisebegleitung, Abrechnung sowie zum Kundendienst über einen Zugangspunkt
bereitstellen, beispielsweise eine Applikation für mobile Endgeräte. Die
bisherigen Ansätze für solche Mobilitätsplattformen sind jedoch höchst
unterschiedlich, was ihre Interoperabilität fachlich, software- und
datentechnisch, aber auch in den Geschäftsmodellen stark erschwert.
Der Umgang mit dieser extremen Heterogenität kann durch ein Referenzmodell
für Mobilitätsplattformen entscheidend erleichtert werden. Als erstes
umfangreiches Experiment wurde dabei zunächst eine modellgestützte Plattform
konzipiert und für die Region Aachen prototypisch umgesetzt, welche
Auskunft, Buchung, Autorisierung und Abrechnung für
Mobilitätsdienstleistungen erstmals integrativ unterstützt. Diese Plattform
ist in Aachen mittlerweile in den Routineeinsatz übergegangen. Im Vergleich
der gewonnenen Erfahrungen mit denen von fachlich meist eingegrenzteren,
aber teils viel umfangreicheren Plattformen anderer Regionen und
bundesweiten Anbietern wurde jedoch festgestellt, dass mehrere
Verbesserungen an dem zugrundeliegenden Modell sowie Erweiterungen um
externe Empirie erst eine Übertragbarkeit auf andere Regionen oder andere
Geschäftsmodelle erlauben würden. Aus dieser integrativen
Anforderungsanalyse wurde in einem iterativen Prozess, unter Einbindung
zahlreicher Anwendungspartner, ein Referenzmodell für Mobilitätsplattformen
entwickelt, das es erlaubt für unterschiedliche Kooperationsszenarien
zwischen Plattform- und Mobilitätsanbieter und somit für unterschiedliche
Geschäftsmodelle angepasste Systemarchitekturen zu erzeugen, in denen
einheitliche Komponenten und Schnittstellen verwendet werden. Hierfür wurde
auch eine neue Entwicklungsmethodik erarbeitet, die Elemente verschiedener
aus der Literatur bekannter agentenorientierter Entwicklungsmethoden
vereint.
Es laden ein: Die Dozenten der Informatik
Lehrstuhl Informatik 5
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Montag, 28. Januar 2019, 16:30 Uhr
Ort: Gebäude E3, Seminarraum 9222, Ahornstr. 55
Referent: Thomas Ströder, Dipl.-Inform.
Lehr- und Forschungsgebiet Informatik 2
Thema: Symbolic Execution and Program Synthesis: A General Methodology for Software Verification
Abstract:
We are concerned with the correctness of software and present a general
methodology for verifying properties of programs in virtually any
programming language. This methodology consists of two stages: First, we
symbolically execute the program in question to obtain a finite
over-approximation of all possible program executions for all possible
inputs. We call this over-approximation a symbolic execution graph. The
difference of this graph compared to most existing approaches using
abstract domains is that its construction is strongly guided by the
analyzed program rather than using program-independent widening
operators. Afterwards, we synthesize programs in simple programming
languages from the symbolic execution graph capturing the essence of the
program properties that we want to analyze. Thus, the subsequent
analysis of these properties on the synthesized programs is
substantially simplified. So we exploit synergies between program
analysis and synthesis techniques to obtain powerful verification approaches.
Although the over-approximation induced by the symbolic execution graph
and subsequent program synthesis might lose precision, our empirical
evaluations demonstrate that the abstract domains introduced in this
thesis are more precise than other existing domains while still allowing
efficient analyses in practice (in particular due to the simplification
obtained by program synthesis and the exploitation of powerful existing
analysis techniques for the simple target languages). Hence, our
methodology proved to be very successful in the leading international
competitions in the fields of our analyses.
We apply our methodology to prove determinacy, termination, and upper
runtime complexity bounds of Prolog programs, memory safety and
termination of LLVM programs (compiled from C programs), deadlock and
livelock freedom of concurrent imperative programs with shared memory,
and to provide a solution to the Behavior Composition Problem, a program
synthesis problem trying to reliably achieve a deterministic target
behavior with a set of non-deterministic agents acting in a
non-deterministic environment.
Our methodology is particularly useful for analyzing “universal”
properties that hold for all program executions (e.g., termination,
memory safety, or upper bounds on runtime complexity). Here, our
empirical results show that our approach clearly outperforms any
previous existing approach. While our methodology can to some extent
also be applied to analyze “existential” properties that only need to
hold for some program executions (e.g., proving the presence of defects
like non-termination or violations of memory safety), additional effort
is necessary to make our approach sound for such analyses due to the
over-approximation inherently involved. In principle, we can detect
candidates satisfying such existential properties in our symbolic
execution graph but must prove their feasibility separately.
Many of our contributions have been implemented in the verification tool
AProVE and empirically evaluated by extensive experiments. Our
contributions advance the state of the art in automated program
verification and offer a guideline for creating future verification
techniques following our methodology.
Es laden ein: Die Dozenten der Informatik
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Donnerstag, 24. Januar 2019, 14:00 Uhr
Ort: Raum 9222, Gebäude E3, Ahornstr. 55
Referentin: Svenja Schalthöfer, M. Sc.
LuF Math. Grundlagen der Informatik (Lehrgebiet Informatik 7)
Thema: Choiceless Computation and Logic
Abstract:
Choiceless computation emerged as an approach to the fundamental open question in
descriptive complexity theory: Is there a logic capturing polynomial time? The main
characteristic distinguishing logic from classical computation is isomorphism-invariance.
Consequently, choiceless computation was developed as a notion of isomorphism-invariant
computation that operates directly on mathematical structures, independently of their
encoding. In particular, these computation models are choiceless in the sense that they
cannot make arbitrary choices from a set of indistinguishable elements.
Choiceless computation was originally introduced by Blass, Gurevich and Shelah in the
form of Choiceless Polynomial Time (CPT), a model of computation using hereditarily
finite sets of polynomial size as data structures.
We study the structure and expressive power of Choiceless Polynomial Time, the most
promising candidate for a logic capturing polynomial time. Further, we expand the
landscape of choiceless computation by a notion of Choiceless Logarithmic Space, which
is, to our knowledge, the only candidate for a logic capturing logarithmic space.
Es laden ein: Die Dozenten der Informatik
--
Silke Cormann
Sekretariat
Fakultät für Mathematik, Informatik und Naturwissenschaften
Informatik 7 - Logik und Theorie diskreter Systeme
RWTH Aachen University
Ahornstr. 55
52074 Aachen
Tel. +49 241 80-21701
Fax +49 241 80-22215
cormann(a)informatik.rwth-aachen.de