informatik-vortraege September 2018

informatik-vortraege@lists.rwth-aachen.de

4 participants
4 discussions

by Tim Lange

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

4 years, 8 months

Talk by Juergen Gall, Wed 19.09. 15h in UMIC 025

by Bastian Leibe

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 _______________________________________________________________

4 years, 8 months

Einladung: Informatik-Oberseminar Sebastian Freitag

by Freitag, Sebastian

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

4 years, 8 months

Einladung: Informatik-Oberseminar Harold Bruintjes

by Harold Bruintjes

4 years, 8 months

2023

2022

2021

2020

2019

2018

informatik-vortraege September 2018