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

Einladung: Informatik-Oberseminar Christian Hensel
by Hensel, Christian 13 Nov '18

13 Nov '18

+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +********************************************************************** Zeit: Montag, 3. Dezember 2018, 15.00 Uhr Ort: Gebäude E3, Raum 9007, Ahornstr. 55 Referent: Dipl.-Inform. Christian Hensel Thema: The Probabilistic Model Checker Storm -- Symbolic Methods for Probabilistic Model Checking Abstract: In a world in which we increasingly rely on safety critical systems that simultaneously are becoming ever more complex, formal methods provide a means to mathematically rigorously prove systems correct. Model checking is a fully automated technique that is successfully applied in the verification of software and hardware circuits. Probabilistic model checking extends traditional model checking to deal with systems exhibiting stochastic behavior. As model checking can be simplistically viewed as an exhaustive exploration of the state space of the model under consideration, it suffers from the curse of dimensionality: State spaces grow exponentially in the number of components and variables and they quickly become too large to be effectively manageable, a problem that is typically referred to as state space explosion. Symbolic methods have helped to alleviate this problem substantially. Rather than considering states and transitions of the system individually, they instead exploit structure in the model and treat sets of states and transitions simultaneously. Model checkers based on symbolic techniques dominate the landscape of hardware and software model checking. In the probabilistic setting, symbolic methods show potential but are arguably not on par with their qualitative counterparts. In this talk, we summarize our advances in the field of symbolic techniques in the context of probabilistic model checking. After a brief introduction, we show how to reduce probabilistic systems including nondeterministic choices that are represented using decision diagrams with respect to bisimulation minimization, a well-studied technique for factoring out symmetry. Then, we show how to compute and refine bounds on reachability probabilities for infinite-state systems before presenting our novel probabilistic model checker Storm, which encompasses the aforementioned techniques and significantly outperforms competing tools on a set of standard benchmarks. Es laden ein: Die Dozenten der Informatik

1 0

Ankündigung eines Oberseminars (Lehr- und Forschungsgebiet Informatik 5) von Frau Anastassia Küstenmacher
by Daniele Gloeckner 09 Nov '18

09 Nov '18

************************************************************************ ** * Einladung * * * Informatik-Oberseminar * * ************************************************************************ Zeit: Montag, 19.11.2018, 16.30 Uhr Ort: Gebäude E3, Seminarraum 9222 Referentin: Frau Anastassia Küstenmacher, M.Sc. Titel: Improving the Reliability of Service Robots in the Presence of External Faults Abstract: In the field of domestic service robots, recovery from faults is crucial to promote user acceptance. In this context, this work focuses on some specific faults which arise from the interaction of a robot with its real world environment. Even a well-modelled robot may fail to perform its tasks successfully due to external faults which occur because of an infinite number of unforeseeable and unmodelled situations. Through investigating the most frequent failures in typical scenarios which have been observed in real-world demonstrations and competitions using the autonomous service robots Care-O-Bot III and youBot, we identified four different fault classes caused by disturbances, imperfect perception, inadequate planning operator of chaining of action sequences. This thesis then presents two approaches to handle external faults caused by insufficient knowledge about the preconditions of the planning operator. The first approach presents reasoning on detected external faults using knowledge about naïve physics. The naïve physics knowledge is represented by the physical properties of objects which are formalized in a logical framework. The proposed approach applies a qualitative version of physical laws to these properties in order to reason. By interpreting the reasoning results the robot identifies the information about the situations which can cause the fault. Applying this approach to simple manipulation tasks like picking and placing objects show that naïve physics holds great possibilities for reasoning on unknown external faults in robotics. The second approach includes missing knowledge about the execution of an action through learning by experimentation. Firstly, it investigates such representation of executing specific knowledge that can be learned for one particular situation and reused for situations which deviate from the original. The combination of symbolic and geometric models allows us to represent action execution knowledge effectively. This representation is called action execution model (AEM) here. The approach provides a learning strategy which uses a physical simulation for generating the training data to learn both symbolic and geometric aspects of the model. The experimental analysis, performed on two physical robots, shows that AEM can reliably describe execution specific knowledge and thereby serving as a potential model for avoiding the occurrence of external faults. Es laden ein: Die Dozenten der Informatik Lehr- und Forschungsgebiet Informatik 5

1 0

Einladung Informatik-Oberseminar Martin Henze
by Martin Henze 07 Nov '18

07 Nov '18

*********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * *********************************************************************** Zeit: Donnerstag, 22. November 2018, 15:00 Uhr Ort: Seminarraum 9007, Gebäude E3, Ahornstr. 55 Referent: Dipl.-Inform. Martin Henze Thema: Accounting for Privacy in the Cloud Computing Landscape Abstract: Cloud computing enables service operators to efficiently and flexibly utilize resources offered by third party providers instead of having to maintain their own infrastructure. As such, cloud computing offers many advantages over the traditional service delivery model, e.g., failure safety, scalability, cost savings, and a high ease of use. Consequently, cloud computing has revolutionized service delivery and we observe a tremendous trend for moving services to the cloud. However, this trend of outsourcing services and data to the cloud is limited by serious privacy challenges as evidenced by recent security breaches and privacy incidents. Overcoming these privacy challenges is key to enable corporate and private users to fully embrace the advantages of cloud computing. We argue that overcoming these privacy challenges requires cooperation between the various actors in the cloud computing landscape, i.e., users, service providers, and infrastructure providers. All these different actors have clear incentives to cater for privacy but often lack the technical means to do so. To overcome this situation, we provide technical approaches that enable each of them to account for privacy. In this talk, we specifically focus on two contributions in more detail: (i) To support users in exercising their privacy, we raise their awareness for the exposure to cloud services in the context of smartphone apps as well as email services and enable them to anonymously compare their cloud usage to their peers. (ii) By providing privacy requirements-aware cloud infrastructure, we realize user- specified per-data-item privacy policies and thus enable infrastructure providers to adhere to them when storing data in the cloud. Our contributions highlight that it is both promising and feasible to apply cooperation of different actors to strengthen users' privacy and consequently enable more corporate and private users to benefit from cloud computing. Es laden ein: Die Dozentinnen und Dozenten der Informatik

1 0

SFB MAKI Distinguished Lecture: Prof. Anja Feldmann (Director MPI Inf) "The Internet: Opportunities and Challenges" (Nov 15, 16:15 - 17:45)
by Oliver Hohlfeld 06 Nov '18

06 Nov '18

************************************************************************ * * * Einladung * * * * Informatik-Kolloquium * * * ************************************************************************ When: Donnerstag, 15. November 2018, 16.15 Uhr Where: Room 9222, Building E3, Ahornstr. 55 Referent: Prof. Anja Feldmann, Ph.D. Director at the Max Planck Institute for Informatics in Saarbrücken Title: The Internet: Opportunities and Challenges Abstract: While the Internet is a hugely successful, human made artifact that has changed the society fundamentally, it has become a complex system with many challenges. In this talk, I will outline some of them and also point out a number of surprises in terms of our mental models of the Internet that we develop over the years. Next, I will focus on the evolution of the Internet and discuss methods for detecting Internet infrastructure outages and combat major DDoS attacks. I will end with an outlook on how we may evolve the Internet to tackle the future challenges of ubiquitous data availability from sensors and devices everywhere. Bio: Anja Feldmann studied computer science at Universität Paderborn in Germany and received my degree in 1990. After that she continued her studies at Carnegie Mellon University, where she earned a M.Sc. in 1991 and, four years later, a Ph.D. The next four years Anja did research work at AT&T Labs Research, before holding professor positions at Saarland University and the Technical University Munich. Since 2006, she has been professor of Internet Network Architectures at Telekom Innovation Laboratories at Technische Universität Berlin. In May 2012, she was elected the first woman on the employer side of the Supervisory Board of SAP. Since the beginning of 2018 Anja Feldmann is a director at the Max Planck Institute for Informatics in Saarbrücken and Honorar Professor at TU Berlin and Universität des Saarlandes.

1 0

Oberseminar 28.11.
by Blundell, Inga 29 Oct '18

29 Oct '18

+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +********************************************************************** Zeit: Mittwoch, 28. November 2018, 10.00 Uhr Ort: E1, Raum 4312, Ahornstr. 55 Referentin: Inga Blundell Thema: Algorithmic solver selection for systems of differential equations in human brain cell models for the domain specific language NESTML Abstract: The fast advancements in neuroscience and the multitude of newly developed neuron models require a language to describe neurons by means of systems of differential equations. The capability of implementing new models in precise agreement with their mathematical definition and subsequently running computationally efficient simulations is essential for progress on the theoretical foundation of neuroscience. The use of abstract modelling languages like NESTML enables neuroscientists to formally specify their models and to automatically produce high level simulation code that runs efficiently on various computer architectures. An important requirement to these modelling languages is the automatic generation of efficient and precise integrations schemes for differential equations that describe the dynamical behaviour of neuron models. An algorithmic approach to this requirement will be presented in this talk. Es laden ein: Die Dozenten der Informatik ------------------------------------------------------------------------------------------------ ------------------------------------------------------------------------------------------------ Forschungszentrum Juelich GmbH 52425 Juelich Sitz der Gesellschaft: Juelich Eingetragen im Handelsregister des Amtsgerichts Dueren Nr. HR B 3498 Vorsitzender des Aufsichtsrats: MinDir Dr. Karl Eugen Huthmacher Geschaeftsfuehrung: Prof. Dr.-Ing. Wolfgang Marquardt (Vorsitzender), Karsten Beneke (stellv. Vorsitzender), Prof. Dr.-Ing. Harald Bolt, Prof. Dr. Sebastian M. Schmidt ------------------------------------------------------------------------------------------------ ------------------------------------------------------------------------------------------------

1 0

Informatik-Kolloquium
by Fachgruppensprecher 24 Oct '18

24 Oct '18

This Friday Zeynep Akata will give a talk about “Explaining and Representing Novel Concepts With Minimal Supervision”. You are kindly invited. Please see the details below. Best regards, Martin Grohe ————— Title: Explaining and Representing Novel Concepts With Minimal Supervision Speaker: Zeynep Akata (University of Amsterdam) Time and Place: Friday, October 26th, 14:15, AH I Abstract: Clearly explaining a rationale for a classification decision to an end-user can be as important as the decision itself. Existing approaches for deep visual recognition are generally opaque and do not output any justification text; contemporary vision-language models can describe image content but fail to take into account class-discriminative image properties which justify visual predictions. In this talk, I will present my past and current work on Zero-Shot Learning, Vision and Language for Generative Modeling and Explainable Artificial Intelligence where we show (1) how to generalize image classification models to cases when no visual training data is available, (2) how to generate images and image features using detailed visual descriptions, and (3) how our models focus on discriminating properties of the visible object, jointly predict a class label, explain why/not the predicted label is chosen for the image. ---------------------------------------------------------------- Prof. Dr. Martin Grohe | Fachgruppe Informatik http://www.informatik.rwth-aachen.de/ | Ahornstr. 55, 52074 Aachen, Germany | RWTH Aachen University Phone ++49 241 80-21701 / Fax -22215 |

1 0

Einladung Informatik-Oberseminar
by Matthias Terber 22 Oct '18

22 Oct '18

+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +********************************************************************** Zeit: Montag, 29. Oktober 2018, 10:00 Uhr Ort: Raum 2202, i11, Ahornstr. 55 Referent: Matthias Terber, M. Sc. Thema: Praxisorientierte Verwendung und Evaluierung synchroner Programmierung in reaktiven, eingebetteten Systemen Abstract: Durch die große Dominanz der Programmiersprache C im industriellen Bereich, werden die Probleme von reaktiven, eingebetteten Systemen üblicherweise mit konventioneller, sequentieller Programmierung adressiert. Diese bietet jedoch keine spezifische Unterstützung für die Beschreibung von reaktivem Verhalten, wodurch Entwicklung, Verständlichkeit und Wartbarkeit der Software erschwert werden. Synchrone Programmiersprachen könnten eine vielversprechende Lösung darstellen, um den Entstehungsprozess von Software zu vereinfachen und deren Qualität zu verbessern. Bis heute ist der Einsatz von synchroner Programmierung jedoch nur auf sehr spezielle industrielle Anwendungsfälle beschränkt; ihre praktische Anwendung und deren Nutzen werden in existierender Literatur kaum behandelt. In dieser Arbeit wird eine Fallstudie durchgeführt, welche die Anwendbarkeit und Eignung des synchronen Programmierparadigmas anhand eines konkreten, existierenden Smart Devices aus der Industrie untersucht. Mit Fokus auf die reaktive Domäne werden die technischen Herausforderungen für die Entwicklung sowie die Qualitätsprobleme der bestehenden Softwarelösung herausgearbeitet. Basierend auf der synchronen Sprache Céu wird eine synchrone Neuimplementierung skizziert. Diese veranschaulicht den Einsatz von synchroner Programmierung und zeigt deren Vorteile für die Softwareentwicklung. Schließlich glauben wir, dass diese Arbeit grundsätzlich einen praktikablen Weg aufzeigt, wie sich die Qualität eingebetteter Software in industriellen Anwendungen verbessern lässt. Es laden ein: Die Dozenten der Informatik

1 0

Einladung: Oberseminar Herr Tim Lange
by Tim Lange 27 Sep '18

27 Sep '18

************************************************************************ ** * Einladung * * * Informatik-Oberseminar * * ************************************************************************ Zeit: Freitag, 5. Oktober 2018, 10:00 Uhr Ort: Gebäude E2, B-IT-Seminarraum 5053.1, Ahornstr. 55 Referent: Herr Tim Lange, M.Sc. Titel: IC3 Software Model Checking Abstract: Many real-world systems are becoming ever smaller in size and more powerful, such that software becomes more complex. The risk of ubiquitous softwares' misbehaviour and the resulting damage therefore grows dramatically. In order to prevent such erroneous behaviour, model checking, a formal verification technique for determining functional properties of information and communication systems, has proven to be highly useful. For proving mathematical properties, one of the first methods to be taught in schools is induction. With the concept of proving a concrete induction base and a general induction step it is considered a very simple and intuitive, yet powerful proof method. However, finding an inductive formulation for difficult properties can be an extremely hard task. When humans try to solve this problem, they naturally produce a set of smaller, simple lemmas that together imply the desired property. Each of these lemmas holds relative to some subset of previously established lemmas by invoking the knowledge to prove the new lemma. This incremental approach to proving complex properties using sets of small inductive lemmas was first applied to model checking of hardware systems in the IC3 algorithm and has proven to outperform all known approaches to hardware model checking. This talk aims at applying the principles of incremental, inductive verification laid by the IC3 algorithm to software model checking for industrial control software with special attention to the control-flow induced by the program under consideration. For this purpose, basic concepts are introduced and an in-depth explanation of the IC3 algorithm and its different building blocks (search phase, generalization and propagation) is given. Based on these prerequisites, the novel IC3CFA algorithm is presented. In this algorithm, the control-flow of the program is explicitly modelled as an automaton, while the variable valuations are handled symbolically, thus using the best of both worlds. Following the search phase of IC3CFA, solutions for applying generalization to IC3CFA are presented. Finally, the performance of the IC3CFA algorithm and all proposed improvements is extensively evaluated on a set of well-recognised benchmarks. Es laden ein: Die Dozenten der Informatik

1 0

Talk by Juergen Gall, Wed 19.09. 15h in UMIC 025
by Bastian Leibe 18 Sep '18

18 Sep '18

Hi everybody, We're happy to announce the following talk by Prof. Juergen Gall (University of Bonn), which will take place tomorrow, Wednesday, at 15:00h in room UMIC 025. Anybody interested is welcome to attend. Please feel free to forward the announcement. Best regards, Bastian Leibe Speaker: Prof. Juergen Gall (Uni Bonn) Time: Wed. 19.09.2018, 15:00h Place: UMIC 025 Title: Analyzing and Anticipating Human Behavior in Videos -- _______________________________________________________________ Prof. Dr. Bastian Leibe Informatik 8 (Computer Vision) UMIC Research Centre RWTH Aachen University Mies-van-der-Rohe-Strasse 15 office: 124 DE-52074 Aachen phone: +49-241-80 20762 Germany mailto:leibe@vision.rwth-aachen.de _______________________________________________________________

1 0

Einladung: Informatik-Oberseminar Sebastian Freitag
by Freitag, Sebastian 13 Sep '18

13 Sep '18

*********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * *********************************************************************** Zeit: Donnerstag, 27. September 2018, 09:30 Uhr Ort: Seminarraum 003 des IT-Centers, Kopernikusstr. 6 Referent: Sebastian Freitag, M. Sc. Titel: Supported Navigation in Immersive Virtual Environments Abstract: Navigation - the process of getting from one location in a virtual scene to another - is one of the most important and fundamental types of interaction in Virtual Reality, as it is part of most use cases and applications in some way or another. However, there is no single navigation technique that is suitable and appropriate for all use cases, as there is typically a different set of requirements for each application, and all techniques come with their own set of drawbacks. Therefore, the selection of a navigation technique for any use case is usually a trade-off decision. Therefore, this work investigates and proposes navigation support techniques to mitigate the negative aspects of these trade-offs. First, ways to manipulate a user's movement to increase the share of real walking relative to the overall amount of navigation are examined. In this context, a navigation technique is presented that repositions the user while they travel in order to maximize the interaction space for real walking at the target location. Furthermore, it is investigated whether rotation gain (the manipulation of the mapping between physical and virtual head rotations), which can be used for techniques such as redirected walking, is usable in screen-based setups such as CAVE-like environments. Second, the work proposes navigation support techniques based on an automated analysis of the virtual scene, that are aimed at making navigation more efficient. To this end, we analyze scene visibility - which parts of the scene are visible from any viewpoint - and the evaluation of the quality of such a viewpoint. In this context, the work compares different measures to estimate viewpoint quality, contributing several novel methods, and introduces an approach for approximating scene visibility efficiently by restricting the computation to navigable areas of a scene. It is further shown that these techniques can be used successfully to increase the efficiency of navigation, proposing a technique to adjust travel speed automatically, reducing cognitive load, an approach to find intermediate target locations during long-distance travel to reduce cybersickness, and an assistance technique that improves cognitive map buildup during exploration. Es laden ein: Die Dozenten der Informatik

1 0