************************************************************************
**
* 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
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
_______________________________________________________________
***********************************************************************
*
*
* 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
************************************************************************
*
*
* Einladung
*
*
* Informatik-Oberseminar
*
*
************************************************************************
Zeit: Donnerstag, 27. September 2018, 10.30 Uhr
Ort: E1, Raum 5053.2, Ahornstr. 55
Referent: Harold Bruintjes, M.Sc.
Topic: Model-Based Reliability Analysis of Aerospace Systems
Abstract:
In order to provide reliable and safe systems in the aerospace domain,
despite increased complexity and stronger demands on capabilities, new
model-based system and software engineering approaches have to be
developed. The COMPASS project, an international research project
involving RWTH, ESA, FBK and various industrial partners, delivers a
toolset for precisely this purpose.
In this talk, the approach taken by the COMPASS toolset is discussed, in
particular with regard to its most recent advancements. After an
introduction, the talk will focus on new results in requirements
formalization, the use of statistical model checking, the capabilities
of the toolset itself and its application to a case study.
COMPASS offers a multitude of analyses pertaining to correctness,
safety, reliability and fault management, backed by a single modeling
formalism derived from AADL. More information about COMPASS can be
found on its website: http://www.compass-toolset.org .
Es laden ein: Die Dozenten der Informatik