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

[Informatik-assistenten] Einladung: Informatik-Oberseminar Christoph Matheja
by Matheja, Christoph 11 Dec '19

11 Dec '19

+********************************************************************** * * * 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

1 0

Einladung: Informatik-Oberseminar Daniel Neuen
by Daniel Neuen 03 Dec '19

03 Dec '19

+********************************************************************** * * * 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

1 0

Einladung: Informatik-Oberseminar Matthias Hoelzel
by Matthias Hoelzel 27 Nov '19

27 Nov '19

+********************************************************************** * * * 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

1 0

Einladung: Informatik Oberseminar Stefan Breuers
by Stefan Breuers 25 Nov '19

25 Nov '19

+********************************************************************** * * * 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

1 0

Einladung: Informatik Oberseminar Herr Marius Alwin Shekow
by Daniele Gloeckner 05 Nov '19

05 Nov '19

+********************************************************************** * * * 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

1 0

Terminänderung: Informatik-Oberseminar Florian Göbe
by Göbe, Florian 29 Oct '19

29 Oct '19

+********************************************************************** * * * 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

1 0

Einladung Informatik-Kolloquium Prof. Salil Kanhere
by Roman Matzutt 16 Oct '19

16 Oct '19

+********************************************************************** * * * 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

1 0

Einladung: Informatik-Oberseminar Florian Göbe
by Göbe, Florian 15 Oct '19

15 Oct '19

+********************************************************************** * * * 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

1 0

Einladung Oberseminar Stefan Schupp
by Stefan Schupp 16 Sep '19

16 Sep '19

+********************************************************************** * * * 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

1 0

Einladung Informatik Oberseminar Simon Hacks
by Hacks, Simon 13 Aug '19

13 Aug '19

+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +********************************************************************** Zeit: Donnerstag, 12. September 2019, 10.00 Uhr Ort: AH VI (2356|051), Ahornstr. 55 Referent: Simon Hacks, M.Sc. Lehr- und Forschungsgebiet Informatik 3 Thema: Improving the Quality of Enterprise Architecture Models: Processes and Techniques Abstract: Information technology (IT) pervades organizations more and more and becomes increasingly important for their business models. It has evolved from a purely supportive role to an important strategic pillar in many organizations. Even more, it is important that IT is aligned to the needs of the organization. Approaches that realize this are often subsumed under the term "business-IT-alignment". One instrument for achieving business-IT-alignment is Enterprise Architecture (EA). EAs provide a holistic perspective on the structure of the organization and provide a set of techniques to guide and steer the evolution of the organization to a desired goal state. A key artifact of EA is the EA model. It abstracts the elements and their relationships to an understandable and manageable measure. Usually enterprise architects model business processes, applications, hardware components, data models and customer relationships. Based on the information stored in the EA model, the organization's management makes important decisions regarding future focus. Contrary, also on the operational level, the model can provide important information, for example which application is used in which business environment and exchanges data with other applications. In order to be able to derive meaningful decisions from the EA model, their quality is of crucial importance. Therefore, this work is elaborates on developing different processes and techniques that ensure the quality of the EA model. First, we present a process to ensure the quality of the EA model, where model maintenance is understood as a continuous evolution. For this purpose, we define different steps, which have to be considered in such a process. This process will serve as foundation for a continuous delivery pipeline that will help automate as many of these steps as possible. Next, we present an approach that allows storing contrary information in EA models. In addition to the aforementioned processes, we developed also several techniques to improve the quality of EA models. However, for improvement, we need a method to evaluate the quality, which we also introduce within this work. Subsequently, we facilitate machine-learning techniques to support the modeler reuse existing elements of the model. In addition, we compare the performance of different algorithms to determine the best on in a certain situation. Additionally, we present a method to identify unnecessary elements in the model. Es laden ein: die Dozentinnen und Dozenten der Informatik

1 0