- informatik-vortraege - lists.rwth-aachen.de

Einladung: Informatik-Kolloquium Michael Schaub (08.01.2020, 14:00)

von Thomas Noll

*********************************************************************** * * * Einladung * * * Informatik-Kolloquium * * *********************************************************************** Zeit: Mittwoch, 8. Januar 2020, 14:00 Uhr Ort: Raum 9222, Gebäude E3, Informatikzentrum Referent: Michael Schaub University of Oxford, UK and MIT, USA Thema: Data Science for Networks Abstract: Networks have become a widely adopted model for a range of systems, cutting across Science and Engineering. However, our theoretical understanding of many fundamental phenomena that arise in complex networks and networked systems is still limited. My vision is to develop a data science for networks and dynamical systems that will contribute to addressing this challenge, by combining data-driven and model-based approaches, using the language of graphs and networks. In this talk, we will give a brief overview of such a Data Science for Networks. We first discuss how networks appear naturally within models in different research domains and illustrate the underlying scientific questions via examples drawn from applications. We then examine in some detail the problem of feature learning from graphs with unobserved edges, in which we aim to learn certain aspects of a graph solely from dynamical observations on its nodes, without knowledge of the edge-set of the graph. We conclude with a brief outlook on future challenges and open problems. Es laden ein: die Dozentinnen und Dozenten der Informatik

4 Jahre, 4 Monate

1
0
0 0

[Informatik-assistenten] Einladung: Informatik-Oberseminar Christoph Matheja

von Matheja, Christoph

+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +********************************************************************** Zeit: Donnerstag, 9. Januar 2019, 14.00 Uhr Ort: Informatikzentrum, E3, Raum 9222 Referent: Christoph Matheja, M.Sc. Lehrstuhl für Informatik 2 (Software Modeling and Verification) Thema: Automated Reasoning and Randomization in Separation Logic Abstract: We study three aspects of program verification with separation logic: 1. Reasoning about quantitative properties, such as the probability of memory-safe termination, of randomized heap-manipulating programs. 2. Automated reasoning about the robustness of and entailments between formulas in the symbolic heap fragment of separation logic itself. 3. Automated reasoning about pointer programs by combining abstractions based on separation logic with the above techniques and model checking. Regarding the first item, we extend separation logic to reason about quantities, which evaluate to real numbers, instead of predicates, which evaluate to Boolean values. Based on the resulting quantitative separation logic, we develop a weakest precondition calculus à la Dijkstra for quantitative reasoning about randomized heap-manipulating programs. We show that this calculus is a sound and conservative extension of both separation logic and McIver and Morgan's weakest preexpectations which preserves virtually all properties of classical separation logic. We demonstrate its applicability by several case studies. Regarding the second item, we develop an algorithmic framework based on heap automata to compositionally check robustness properties, e.g., satisfiability or acyclicity, of symbolic heaps with inductive predicate definitions. We consider two approaches to discharge entailments for fragments of separation logic. In particular, this includes a pragmatic decision procedure with nondeterministic polynomial-time complexity for entailments between graphical symbolic heaps. Regarding the third item, we introduce Attestor - an automated verification tool for analyzing Java programs operating on dynamic data structures. The tool involves the generation of an abstract state space employing inductive predicate definitions in separation logic. Properties of individual states are defined by heap automata. LTL model checking is then applied to this state space, supporting the verification of both structural and functional correctness properties. Attestor is fully automated, procedure modular, and provides informative visual feedback including counterexamples for violated properties. Es laden ein: die Dozentinnen und Dozenten der Informatik

4 Jahre, 4 Monate

1
0
0 0

Einladung: Informatik-Oberseminar Daniel Neuen

von Daniel Neuen

+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +********************************************************************** Zeit: Dienstag, 17. Dezember 2019, 12.00 Uhr Ort: Raum 5053.2 (großer Bit-Raum), Ahornstr. 55 Referent: Daniel Neuen M.Sc. Lehrstuhl Informatik 7 Thema: The Power of Algorithmic Approaches to the Graph Isomorphism Problem Abstract: The Graph Isomorphism Problem asks, given two input graphs, whether they are structurally the same, that is, whether there is a renaming of the vertices of the first graph in order to transform it to the second graph. By a recent breakthrough result of Babai, this problem can be solved in quasipolynomial time. However, despite extensive research efforts, it remains one of only few natural problems in NP that are neither known to be solvable in polynomial time nor known to be NP-complete. Over the past five decades several powerful techniques tackling the Graph Isomorphism Problem have been investigated uncovering various surprising links between different approaches. One of the most fundamental methods in the context of graph isomorphism testing is the Weisfeiler-Leman algorithm and the related paradigm of individualization and refinement. The latter is in particular employed in all practical tools tackling the isomorphism problem. We present new upper and lower bounds on the power of such purely combinatorial approaches. For example, this leads to the first exponential lower bounds on the worst-case complexity of all state-of-the-art isomorphism tools used in practice. A second crucial approach to the Graph Isomorphism Problem is based on group-theoretic techniques. In this direction, one of the algorithmic cornerstones is Luks polynomial time algorithm for testing isomorphism of bounded degree graphs. Adapting the novel group-theoretic methods by Babai developed for his quasipolynomial time isomorphism test we give an isomorphism test for graphs of maximum degree d with a running time bounded by a polynomial of degree polylogarithmic in d. As a consequence of this result we also obtain an improved fpt algorithm for testing isomorphism of graphs of bounded tree-width. Es laden ein: die Dozentinnen und Dozenten der Informatik

4 Jahre, 4 Monate

1
0
0 0

Einladung: Informatik-Oberseminar Matthias Hoelzel

von Matthias Hoelzel

+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +********************************************************************** Zeit: Dienstag, 10. Dezember 2019, 12:00 Uhr Ort: Raum 9222, Gebäude E3, Ahornstr. 55 Referent: Matthias Hoelzel, M.Sc. LuF Math. Grundlagen der Informatik (Lehrgebiet Informatik 7) Thema: Fragments of Existential Second-Order Logic and Logics with Team Semantics Abstract: Team semantics is the modern basis for logics of dependence and independence whose formulae are not evaluated with single assignments, but with sets of such assignments. We study different fragments of logics with team semantics and existential second-order logic (ESO) such as the union-closed fragments of these logics, inclusion logic of restricted arity and logics with team semantics using weaker dependency concepts. We will present syntactic characterisations for the union-closed fragment of ESO and inclusion-exclusion logic. In order to obtain these characterisation results, novel inclusion-exclusion games are utilised as a bridge between semantical and syntactical fragments. These games are not only the model-checking games of ESO-sentences, but they can also be adapted for fragments of ESO and give rise to the definition of a single team-based atom that captures the union-closed fragment. Further we answer an open question due to Rönnholm regarding the connection between inclusion logic of restricted arity and a fragment of greatest fixed-point logic. Finally, we study variants of logics with dependency concepts, which can distinguish elements only up to a given equivalence. We juxtapose these new logics with equivalent fragments of ESO and analyse their expressive powers. Es laden ein: die Dozentinnen und Dozenten der Informatik

4 Jahre, 5 Monate

1
0
0 0

Einladung: Informatik Oberseminar Stefan Breuers

von Stefan Breuers

+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +********************************************************************** Zeit: Montag, 02. Dezember 2019, 13:30 Uhr Ort: UMIC Research Centre, room 025, Mies-van-der-Rohe Strasse 15 Referent: Stefan Breuers, MSc., Lehrstuhl Informatik 8 (Computer Vision) Thema: Multi-object Tracking and Person Analysis from Mobile Robot Platforms Abstract: Detecting and tracking the persons in a scene has been an active field of research in the area of computer vision for decades. One of the main applications are mobile platforms, such as autonomous cars or service robots. In this talk, we are going to analyze different tracking approaches working on the image domain and have a deeper look at their errors, before we move forward to multi-object tracking from robots operating in the 3D world. We present our detection-tracking framework for systematic tracking evaluation and our insights on experiments in challenging environments. On top of that detection-tracking pipeline, we then run person analysis modules and look at the benefits of such an integration for an improved person-robot interaction. By utilizing the temporal information in the form of the person track identities, we enable a robust and efficient operation of expensive deep learning analysis methods on low-cost platforms. We conclude the talk by presenting an explorative work on the integration of person re-identification and multi-object tracking to overcome common compromises of classical tracking approaches, taking a step towards an end-to-end, image-to-track paradigm. Es laden ein: die Dozentinnen und Dozenten der Informatik

4 Jahre, 5 Monate

1
0
0 0

Einladung: Informatik Oberseminar Herr Marius Alwin Shekow

von Daniele Gloeckner

+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +********************************************************************** Zeit: Freitag, 22.11.2019 um 13.00 Uhr Ort: Informatikzentrum, E3, Raum 5053.2 (ggü. AH 6) Referent: Marius Alwin Shekow, M. Sc. Informatik 5 Thema: Syncpal: A Simple and Iterative Reconciliation Algorithm for File Synchronization Abstract: To facilitate collaboration scenarios and data management across multiple devices, knowledge workers and individuals use file synchronizers. These tools replicate the devices local file system to a cloud storage. As Marius Shekow discusses in his doctoral viva, bugs in these file synchronizers force users to detect and fix synchronization errors manually, resulting in cost-intensive iterations in cooperation processes, which should be avoided. He presents the three core challenges in file synchronization which he examined in his doctoral thesis. You will learn about (a) heterogeneity of file systems and alternatives to handle their incompatibilities, (b) conflicting operations and options for conflict resolution, and (c) inferring a valid operation propagation order to optimize the synchronization efficiency and correctness. The speaker presents how these challenges are solved by example with the iterative Syncpal algorithm he developed in his thesis. The evaluation of its implementation shows that Syncpal improves the handling of file system heterogeneity and synchronizes changes from long offline periods correctly. Es laden ein: die Dozentinnen und Dozenten der Informatik

4 Jahre, 5 Monate

1
0
0 0

Terminänderung: Informatik-Oberseminar Florian Göbe

von Göbe, Florian

+********************************************************************** * * * Terminänderung * * * * Informatik-Oberseminar * * * +********************************************************************** ++++++++ * ALTE ZEIT: Donnerstag, 7. November 2019, 10:00 Uhr * NEUE ZEIT: Donnerstag, 7. November 2019, 9:30 Uhr ++++++++ Ort: Raum 2359|222 (9222), Informatikzentrum Erweiterungsbau 3 Referent: Florian Göbe, M.Sc.RWTH Informatik 11 – Embedded Software Thema: Überwachung von SPS-Programmen zur Laufzeit mittels ereignisdiskreter Systeme Kurzfassung: Bei der von Ramadge und Wonham eingeführten Supervisory Control Theory (SCT) handelt es sich um einen der verbreitetsten Ansätze für die Synthese von Lösungen im Bereich diskreter Steuerungen. In diesem Vortrag wird ein Ansatz vorgestellt, der das SCT-Rahmenwerk zur Überwachung existierender SPS-Steuerungsprogramme einsetzt. Letztere werden als vom Benutzer manuell implementiert angenommen, weswegen ihre Fehlerfreiheit in Bezug auf gewisse Anforderungen, beispielsweise an die funktionale Sicherheit, nicht in allen prinzipiell möglichen Situationen formal sichergestellt werden kann. Im vorgestellten Ansatz können diese Anforderungen als ereignisdiskrete Systeme formalisiert werden. Mittels einer modifizierten Form des Ramadge-Wonham-Rahmenwerkes wird aus diesen Modellen schließlich eine Überwachungsschicht generiert. Diese verhindert frühzeitig solche Aktionen der Steuerung, die schlussendlich zu einer Verletzung der Anforderungen führen könnten. Um eine möglichst große Bandbreite realistischer Anwendungsfälle abzudecken, wurden mehrere Anpassungen am ursprünglichen Rahmenwerk vorgenommen und Erweiterungen eingeführt, beispielsweise bedingte Transitionen, Vorlagen sowie Ereigniserzwingung zur Verhinderung unerwünschter Vorkommnisse. Das vorgestellte Konzept bildet den gesamten Prozess von der Erstellung der Anforderungsmodelle bis hin zu einer auf der Zielhardware direkt einsetzbaren Sicherheitsschicht ab und wurde in Form eines Werkzeugs prototypisch realisiert und evaluiert. Es laden ein: die Dozentinnen und Dozenten der Informatik

4 Jahre, 6 Monate

1
0
0 0

Einladung Informatik-Kolloquium Prof. Salil Kanhere

von Roman Matzutt

+********************************************************************** * * * Einladung * * * * Informatik-Kolloquium * * * +********************************************************************** Zeit: Montag, 21. Oktober 2019, 10.30 Uhr Ort: Informatikzentrum, E3, Raum 9007 Referent: Prof. Salil Kanhere School of Computer Science and Engineering, UNSW Sydney Thema: TrustChain: Trust Management in Blockchain and IoT supported Supply Chains Abstract: Traceability and integrity are major challenges for the increasingly complex supply chains of today’s world. Although blockchain technology has the potential to address these challenges through providing a tamper-proof audit trail of supply chain events and data associated with a product lifecycle, it does not solve the trust problem associated with the data itself. Reputation systems are an effective approach to solve this trust problem. However, current reputation systems are not suited to the blockchain based supply chain applications as they are based on limited observations, they lack granularity and automation, and their overhead has not been explored. In this talk, we propose TrustChain, as a three-layered trust management framework which uses a consortium blockchain to track interactions among supply chain participants and to dynamically assign trust and reputation scores based on these interactions. The novelty of TrustChain stems from: (a) the reputation model that evaluates the quality of commodities, and the trustworthiness of entities based on multiple observations of supply chain events, (b) its support for reputation scores that separate between a supply chain participant and products, enabling the assignment of product-specific reputations for the same participant, (c) the use of smart contracts for transparent, efficient, secure, and automated calculation of reputation scores, and (d) its minimal overhead in terms of latency and throughput when compared to a simple blockchain based supply chain model. Speaker Biography: Salil Kanhere is a Professor in the School of Computer Science and Engineering at UNSW Sydney. He is also a conjoint researcher at CSIRO's Data61 and a participating researcher in the Cyber Security Cooperative Research Centre. He has held visiting appointments at Technical University Darmstadt, University of Zurich, Graz University of Technology and Institute of Infocom Research Singapore. His research interests include Internet of Things, blockchain, cyber physical systems, applied machine learning and cybersecurity. His research has been featured in various media outlets including ABC News Australia, Forbes, IEEE Spectrum, Wired, ZDNET, Computer World, Medium and MIT Technology Review. He serves as the Editor in Chief of the Ad Hoc Networks Journal and as Associate Editor of Pervasive and Mobile Computing and Computer Communications journals. He is an Humboldt Research Fellow and ACM Distinguished Speaker. He regularly serves on the organising committee of top-tier IEEE/ACM conferences in his discipline. Es laden ein: die Dozentinnen und Dozenten der Informatik

4 Jahre, 6 Monate

1
0
0 0

Einladung: Informatik-Oberseminar Florian Göbe

von Göbe, Florian

+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +********************************************************************** Zeit: Donnerstag, 7. November 2019, 10.00 Uhr Ort: Raum 2359|222 (9222), Informatikzentrum Erweiterungsbau 3 Referent: Florian Göbe, M.Sc.RWTH Informatik 11 – Embedded Software Thema: Überwachung von SPS-Programmen zur Laufzeit mittels ereignisdiskreter Systeme Kurzfassung: Bei der von Ramadge und Wonham eingeführten Supervisory Control Theory (SCT) handelt es sich um einen der verbreitetsten Ansätze für die Synthese von Lösungen im Bereich diskreter Steuerungen. In diesem Vortrag wird ein Ansatz vorgestellt, der das SCT-Rahmenwerk zur Überwachung existierender SPS-Steuerungsprogramme einsetzt. Letztere werden als vom Benutzer manuell implementiert angenommen, weswegen ihre Fehlerfreiheit in Bezug auf gewisse Anforderungen, beispielsweise an die funktionale Sicherheit, nicht in allen prinzipiell möglichen Situationen formal sichergestellt werden kann. Im vorgestellten Ansatz können diese Anforderungen als ereignisdiskrete Systeme formalisiert werden. Mittels einer modifizierten Form des Ramadge-Wonham-Rahmenwerkes wird aus diesen Modellen schließlich eine Überwachungsschicht generiert. Diese verhindert frühzeitig solche Aktionen der Steuerung, die schlussendlich zu einer Verletzung der Anforderungen führen könnten. Um eine möglichst große Bandbreite realistischer Anwendungsfälle abzudecken, wurden mehrere Anpassungen am ursprünglichen Rahmenwerk vorgenommen und Erweiterungen eingeführt, beispielsweise bedingte Transitionen, Vorlagen sowie Ereigniserzwingung zur Verhinderung unerwünschter Vorkommnisse. Das vorgestellte Konzept bildet den gesamten Prozess von der Erstellung der Anforderungsmodelle bis hin zu einer auf der Zielhardware direkt einsetzbaren Sicherheitsschicht ab und wurde in Form eines Werkzeugs prototypisch realisiert und evaluiert. Es laden ein: die Dozentinnen und Dozenten der Informatik

4 Jahre, 6 Monate

1
0
0 0

Einladung Oberseminar Stefan Schupp

von Stefan Schupp

+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +********************************************************************** Zeit: Mittwoch, 25. September 2019, 15.00 Uhr Ort: Informatikzentrum, E3, Raum 9222 Referent: Stefan Schupp M.Sc.(Theory of Hybrid Systems) Thema: State Set Representations and their Usage in the Reachability Analysis of Hybrid Systems Abstract: Hybrid systems in computer science are systems with combined discrete-continuous behavior. This work presents results obtained in the field of safety verification for linear hybrid systems whose continuous behavior can be described by linear differential equations. We focus on a special technique named flowpipe-construction-based reachability analysis, which over-approximates the reachable states of a given hybrid system as a finite union of state sets. In these computations we can use different geometric and symbolic representations for state sets as datatypes. In this talk we focus on the following aspects: - We present our C++ library HyPro, offering implementations for several state set representations that are commonly used in flowpipe-construction-based reachability analysis. - We show the applicability of HyPro by embedding a flowpipe-construction-based reachability analysis method in a CEGAR-based abstraction refinement framework. - We present our approach to decompose the search space and replace high-dimensional computations by computations in lower-dimensional subspaces. Es laden ein: die Dozentinnen und Dozenten der Informatik

4 Jahre, 7 Monate

1
0
0 0

2024

2023

2022

2021

2020

2019

2018

informatik-vortraege