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

Oberseminar Herr Dipl.-Inform. Christoph Terwelp am 05.02.2019
by Daniele Gloeckner 18 Jan '19

18 Jan '19

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

1 0

[sekretariate] Einladung: Informatik Oberseminar Thomas Ströder
by Elke Ohlenforst 18 Jan '19

18 Jan '19

+********************************************************************** * * * 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 Veriﬁcation 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 ﬁnite over-approximation of all possible program executions for all possible inputs. We call this over-approximation a symbolic execution graph. The diﬀerence 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 simpliﬁed. So we exploit synergies between program analysis and synthesis techniques to obtain powerful veriﬁcation 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 eﬃcient analyses in practice (in particular due to the simpliﬁcation 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 ﬁelds 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 eﬀort 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 veriﬁcation tool AProVE and empirically evaluated by extensive experiments. Our contributions advance the state of the art in automated program veriﬁcation and oﬀer a guideline for creating future veriﬁcation techniques following our methodology. Es laden ein: Die Dozenten der Informatik

1 0

Einladung: Informatik-Oberseminar Svenja Schalthöfer
by Cormann, Silke 17 Jan '19

17 Jan '19

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

1 0

Einladung: Informatik-Oberseminar Benedikt Brütsch (20. Dez., 16:15 Uhr)
by Benedikt Brütsch 13 Dec '18

13 Dec '18

+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +********************************************************************** Zeit: Donnerstag, 20. Dezember 2018, 16:15 Uhr Ort: Raum 9222, Gebäude E3, Ahornstr. 55 Referent: Dipl.-Inform. Benedikt Brütsch Lehrstuhl Informatik 7 Thema: Strategies in Infinite Games: Structured Reactive Programs and Transducers over Infinite Alphabets Abstract: In this talk, we study the construction of winning strategies in games of the following kind: Two players take turns in choosing symbols from some fixed alphabet. They play forever, thus constructing an infinite sequence of symbols. The winning condition is a set L of such sequences: Player II wins if the constructed sequence is in the set L, otherwise Player I wins. These games can be viewed as a model of reactive systems, which maintain an ongoing interaction with their environment. We consider the so-called synthesis problem: Given a winning condition, determine whether Player II has a winning strategy, and construct such a strategy. First, we study the synthesis of winning strategies in the form of structured reactive programs (for omega-regular winning conditions). In particular, we show an exponential lower bound for the number of (Boolean) program variables that are required in the case of winning conditions specified in linear temporal logic (LTL), roughly matching the known upper bound. Second, we consider a more general form of the synthesis problem, where the alphabet is infinite. Specifically, we focus on the case where the symbols chosen by the players are natural numbers. To represent winning conditions, we define a model of automata over infinite alphabets such as the set N of natural numbers, namely N-memory automata. Analogously, we introduce N-memory transducers to represent strategies. We show that the synthesis problem is solvable in this setting: Given a winning condition defined by a deterministic N-memory automaton with a parity acceptance condition, we can determine which player has a winning strategy and construct such a strategy in the form of a deterministic N-memory transducer. Es laden ein: Die Dozenten der Informatik

1 0

Einladung: Informatik-Oberseminar Sarah Winter
by Sarah Winter 13 Dec '18

13 Dec '18

+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +********************************************************************** Zeit: Mittwoch, 19. Dezember 2018, 10:00 Uhr Ort: Gebäude E3, Seminarraum 9222, Ahornstr. 55 Referentin: Sarah Winter, M.Sc. Informatik 7 Thema: Synthesis of Transducers from Relations on Finite Words and Trees Abstract: The synthesis problem asks, given a specification that relates possible inputs to allowed outputs, whether there is a program realizing the specification, and if so, construct one. Such a program is referred to as an implementation of the specification. The field of automata theory offers a rich landscape of models for defining specifications and implementations over both words and trees. We consider synthesis of sequential transducers from automaton-definable specifications on finite words and trees. In this talk, concerning specifications over words, we discuss synthesis of sequential word transducers from rational relations in which the allowed input/output behavior is specified by a given set of synchronizations. Concerning specifications over trees, we focus on synthesis of deterministic top-down tree transducers from tree-automatic specifications. Es laden ein: Die Dozenten der Informatik

1 0

Vortrag, heute 16:15, AH I: Prof. Olivier Bonaventure (UC Louvain, BE) "Future Internet Protocols"
by Klaus Wehrle 13 Dec '18

13 Dec '18

Liebe Informatiker*innen, ein kurzer Reminder an den Vortrag heute Nachnmittag im Rahmen der Distinguished Lecture Series des SFB 1053 MAKI um 16:15h im AH I. viele Grüße klaus wehrle ************************************************************************ * * * Einladung * * * * Informatik-Kolloquium * * * ************************************************************************ When: Donnerstag, 13. Dezember 2018, 16.15 Uhr Where: AH I, Ahornstr. 55 Referent: Prof. Olivier Bonaventure UCLouvain Title: Future Internet protocols Abstract: For many years, there were few innovations in the core Internet protocols. This changed during the last years with Multipath TCP, IPv6 Segment Routing and protocols such as QUIC. This talk will discuss some of the recent changes to the core Internet protocols and discuss future challenges. Bio: Olivier Bonaventure is Professor at UCLouvain where he leads the IP Networking Lab (https://inl.info.ucl.ac.be). Most of his research focuses on improving Internet protocols. His PhD students participated to the design and implemented several Internet protocols including LISP, Multipath TCP or IPv6 Segment Routing. He wrote the open-source Computer Networking : Principles, Protocols and Practice ebook that is used by various universities and co-founded the Tessares startup that creates innovative solutions based on Multipath TCP.

1 0

Guest Talk: Dr. Marc Körner (ICSI, UC Berkeley) "Open Carrier Interfaces as an Enabler for Edge-Supported Services" (Dec 14, 10:00 - 10:45)
by Jens Hiller 11 Dec '18

11 Dec '18

************************************************************************ * * * Einladung * * * * Informatik-Kolloquium * * * ************************************************************************ When: Freitag, 14. Dezember 2018, 10.00 Uhr Where: COMSYS Seminar Room (Room 9007), Building E3, Ahornstr. 55 Referent: Dr. Marc Körner International Computer Science Institute (ICSI) and UC Berkeley Netsys Lab group Title: Open Carrier Interfaces as an Enabler for Edge-Supported Services Abstract: Edge computing is an increasingly important theme for carriers and application developers. This talk will outline how a merging of serverless computing and an open-carrier interface can facilitate the growth of edge-supported services. In this model, carriers open up their edge facilities to third-party application providers (hereafter called tenants) by offering the ability to deploy network edge processing on-demand without operator intervention. There are two keys to this Open Carrier Interface (OCI) model. First, the relevant edge processing is only invoked when clients associated with that tenant attach at an edge. Thus, much like serverless computing, the cost of OCI is proportional to the usage, greatly reducing the barriers to deploying new global services. Second, the carrier interface allows the tenant to specify an overall application interaction pattern, which controls where their clients traffic should be directed and provides edge-based lookup and redirection services. The combination of these two features provides a fully-automated and cost-effective way for third-parties to deploy new global services that are enhanced by edge support. Bio: Marc Körner is Postdoctoral Researcher currently working on a DAAD research fellowship at the UC Berkeley Netsys Lab group, the International Computer Science Institute (ICSI), and the EIT Digital Silicon Vally hub. He received a Dr.-Ing. degree from the faculty of EECS at TU Berlin in 2015 for his dissertation on Software Defined Networking based Data Center Services. His research focus is in scope of network technologies and SDN/NFV based data center solutions.

1 0

Einladung Informatik-Oberseminar, Ph.D. Exam Public Presentation
by Dan Matheson 08 Dec '18

08 Dec '18

+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +********************************************************************** Zeit: Freitag, 18. Januar 2019, 13.00 Uhr Ort: Raum 9222, Gebäude E 3, Ahornstr. 55 Referent: Dan Matheson, MSCS Lehrstuhl Informatik 3 Thema: SAMEM: A Methodology for the Elicitation and Specification of Requirements for Agile Model-driven Engineering of Large Software Solutions Abstract: In this talk, we present an overview of SAMEM (Software Agile Modeling and Engineering Methodology). The SAMEM focuses on Agile and Model-driven Development (MDD) techniques in the early stages of the product development process, primarily requirements specification. Adaptations and differences in applying Agile and MDD for requirements versus code developed are highlighted. The SAMEM approach has been applied in over 18 industry projects with two different development teams and customers. The SAMEM provides guidance through the abstraction hierarchy from initial ideas to deployment while ensuring engineering due diligence and enabling innovation. Es laden ein: Die Dozenten der Informatik

1 0

SFB MAKI Distinguished Lecture: Prof. Olivier Bonaventure (UCLouvain) "Future Internet protocols" (Dez 13, 16:15 - 17:30)
by Oliver Hohlfeld 06 Dec '18

06 Dec '18

************************************************************************ * * * Einladung * * * * Informatik-Kolloquium * * * ************************************************************************ When: Donnerstag, 13. Dezember 2018, 16.15 Uhr Where: AH I, Ahornstr. 55 Referent: Prof. Olivier Bonaventure UCLouvain Title: Future Internet protocols Abstract: For many years, there were few innovations in the core Internet protocols. This changed during the last years with Multipath TCP, IPv6 Segment Routing and protocols such as QUIC. This talk will discuss some of the recent changes to the core Internet protocols and discuss future challenges. Bio: Olivier Bonaventure is Professor at UCLouvain where he leads the IP Networking Lab (https://inl.info.ucl.ac.be). Most of his research focuses on improving Internet protocols. His PhD students participated to the design and implemented several Internet protocols including LISP, Multipath TCP or IPv6 Segment Routing. He wrote the open-source Computer Networking : Principles, Protocols and Practice ebook that is used by various universities and co-founded the Tessares startup that creates innovative solutions based on Multipath TCP.

1 0

Einladung: Informatik Oberseminar Ulrich Loup
by Ulrich Loup 29 Nov '18

29 Nov '18

+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +********************************************************************** Zeit: Freitag, 14. Dezember 2018, 13:00 Uhr Ort: Gebäude E3, Seminarraum 9222, Ahornstr. 55 Referent: Ulrich Loup Theory of Hybrid Systems Informatik 2 Thema: On Solving Real-algebraic Formulas in a Satisfiability-modulo-theories Framework Abstract: Quantifier-free real-algebraic formulas are Boolean combinations of polynomial equations and inequalities over the domain of the real numbers. Coming with a strong expressiveness and a still decidable satisfiability problem, real- algebraic formulas are a precious modeling language in many academic, industrial and commercial areas. However, only some classes of real-algebraic formulas allow an efficient solving in practice. For instance, conjunctions of linear real-algebraic constraints can be solved with the very successful simplex method. The general quantifier-free real-algebraic satisfiability problem, however, has a worst-case time complexity bound which is exponential in the number of input variables. Methods solving this general problem directly are often inefficient in practice. The very popular cylindrical algebraic decomposition (CAD) method has a doubly-exponential complexity bound in the number of input variables for its search space. This thesis tackles the solving of general quantifier-free real-algebraic formulas with a combination of different methods in a satisfiability-modulo- theories (SMT) framework: A SAT solver computes partial assignments for the Boolean structure of the real-algebraic formula and real-algebraic solvers check these assignments for consistency in the real domain. If the assignment is infeasible in the real domain, the SAT solver would profit from a small - preferably minimal - reason for this conflict in terms of a subset of the constraints corresponding to the conflicting assignment. In this talk, I focus on two real-algebraic solvers in our SMT-solving framework SMT-RAT, which are major contributions of my thesis. The first solver is an implementation of the CAD method specialized for an efficient embedding into an SMT solver. In particular, the CAD method is extended by the ability to solve incrementally, i.e. reuse pre-computed results, to backtrack and to compute minimal reasons. Moreover, bounds to the variables are used to prune the CAD search space, especially when combining the method with interval-arithmetic techniques. The second solver uses an extension of Buchberger's algorithm in order to compute a Gröbner basis. The solver supports incremental solving, backtracking and minimal reasons for some unsatisfiable cases, as well. We extended the method so that the solver can also be used in order to simplify formulas for other real-algebraic solvers in the SMT-solving framework. As a main part, my thesis comprises an evaluation of the two solvers in the SMT-RAT framework. In particular, the effects of combining the CAD method with a Gröbner-bases solver in an SMT framework are investigated. In my talk, some experimental results of this evaluation are shown, too.

1 0