informatik-vortraege September 2023

informatik-vortraege@lists.rwth-aachen.de

3 Teilnehmer
3 Diskussionen

[sekretariate] Einladung Informatik-Oberseminar Jera Hensel

von Elke Ohlenforst

+********************************************************************** * * *Einladung * * * *Informatik-Oberseminar * * * +********************************************************************** Zeit: Donnerstag, 12. Okt. 2023, 09:00 Uhr Ort: Informatikzentrum der RWTH Aachen University, Gebäude E3, 2. Etage, Raum 9222 Referent: Jera Hensel, M.Sc. Lehr- und Forschungsgebiet Informatik 2 Thema: Automated Termination Analysis of C Programs Abstract: The termination behavior of a program is a crucial property when reasoning about its correctness and safety. Non-termination and also undesired termination can lead to serious consequences such as system crashes and security vulnerabilities. Therefore, we are interested in techniques to (dis)prove termination of programs to make software systems more secure and reliable. Analyzing the termination behavior of C programs is especially challenging since C combines concepts of higher programming languages with pointers and explicit memory management. In this talk, we summarize our improvements of a termination analysis approach that is especially powerful for C programs with memory allocation and explicit pointer arithmetic, but which was limited to rather small non-recursive programs without recursive data structures, where all integers were interpreted as unbounded (mathematical) integers. This approach uses symbolic execution with abstraction to convert the analyzed program to an integer transition system (ITS) with the property that termination of this ITS implies termination of the C program. Thus, after this transformation, existing techniques for ITSs can be applied to prove termination of the program. We lift the above mentioned restrictions by new techniques that only require adaptions of the symbolic execution rules and the abstraction methods, but use the same transformation to ITSs as before. Moreover, we briefly show how this approach is modified to prove non-termination. We implemented all extensions in our tool AProVE and evaluate them in comparison with other leading termination tools. Es laden ein: die Dozentinnen und Dozenten der Informatik -- Elke Ohlenforst Softwaremodellierung und Verifikation Lehrstuhl Informatik 2, RWTH Aachen Ahornstr. 55, D-52074 Aachen/Germany Tel.: +49 (0)241 80-21201 email:ohlenforst@informatik.rwth-aachen.de https://moves.rwth-aachen.de/

9 Monate, 1 Woche

[Informatik-assistenten] Einladung: Informatik-Oberseminar Dzenan

von Dzafic, Dzenan

+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +********************************************************************** Zeit: Donnerstag, 14. September 2023, 15.00 Uhr Ort: Informatikzentrum, H, 2. Etage, Raum 2202. Referent: Dzenan Dzafic, M. Sc. Lehrstuhl Informatik 11 (Embedded Software) Thema: Fahrassistenz für Elektrorollstühle Abstract: In der heutigen Gesellschaft unterstützen Smartphone-Apps die Menschen in den meisten Bereichen. Seien es Planungen von täglichen Aktivitäten oder die spezifische Suche nach Information. Ein weiterer sehr großer Anwendungsbereich ist die Frage: “Wie kommt ein Mensch von A nach B?”. Bei den meisten Menschen kommen Navigationsapps wie z.B. Google-Maps etc. zum Einsatz. Für über zwei Millionen der Deutschen ist dies nicht immer möglich[1] [2], da Menschen mit einer schweren Behinderung andere Anforderung haben. Denn viele Wege sind nicht barrierefrei, die Akkukapazität des Elektrollstuhls ist beschränkt und damit auch ihre Reichweite, oder der Bodenbelag ist für ihren Rollstuhl so uneben, dass eine erhöhte Kippgefahr besteht. Zusatzlich dazu bewirken einige Bodenbelage eine drastische Senkung des Komforts für den Rollstuhlfahrer, der stark darauf durchgeschüttelt wird. Genau an diesem Punkt setzt diese Arbeit mit den Projekt eNav an. eNav ist ein Navigationssysstem für Rollstuhlfahrer mit dem Ziel die Lebensqualität von Menschen mit Mobilitätseinschränkung zu erhöhen. Dabei steht neben der Barrierefreiheit auch der Energieverbrauch des Elektrorollstuhls im Vordergrund. Das System informiert den Benutzer über den Energieverbrauch, sodass dieser nicht mitten auf dem Weg stehen bleibt. Die Entwicklung des eNav Systems zeigt, wie es möglich ist das Kartenmaterial aufzubereiten, um mit eNav barrierefreies energieeffizientes Routen zu ermöglichen und was dafür notwendig ist. Die Beschaffung und Erzeugung der dafür benötigten Datenquellen spielt hier eine zentrale Rolle. Ein dafür modifizierter A*-Algorithmus sorgt dann für energieeffizientes Routen. Das Multimodale Dynamische Routing verkürzt die Reisezeit und reduziert den Energieverbrauch, indem es den öffentlichen Nahverkehr einbezieht. Eine Untersuchung zeigt, dass in der Stadt Aachen in 41% allen untersuchten Routen eine energieeffizientere Route im Vergleich zur kürzesten Route existiert. Der Benutzer kann die Vorteile von eNav mit Hilfe eines Routenplaners und einer Navigations-App nutzen. Es laden ein: die Dozentinnen und Dozenten der Informatik _______________________________________________ Informatik-assistenten mailing list -- informatik-assistenten(a)lists.rwth-aachen.de To unsubscribe send an email to informatik-assistenten-leave(a)lists.rwth-aachen.de https://lists.rwth-aachen.de/postorius/lists/informatik-assistenten.lists.r… ________________________________________________ Dzenan Dzafic, M. Sc. RWTH RWTH Aachen University Embedded Software (Lehrstuhl für Informatik 11) Ahornstrasse 55, 52074 Aachen, Germany Office: Room 2309 (Building H) Tel.: +49 241 80 21159 Mobile: +49 173 5720384 Fax: +49 241 80 21150 Email: dzafic(a)embedded.rwth-aachen.de Web: https://embedded.rwth-aachen.de/

9 Monate, 3 Wochen

Einladung Informatik-Oberseminar Till Hofmann

von Stephanie Jansen

********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * *********************************************************************** Zeit: Mittwoch, 20. September 2023, 14:00 Uhr Ort: Informatikzentrum, 5053.2 (B-IT) Zoom:https://rwth.zoom-x.de/j/63749614813 Referent: Till Hofmann, M.Sc. Thema: Towards Bridging the Gap between High-Level Reasoning and Execution on Robots Abstract: When reasoning about actions, e.g., by means of task planning or agent programming with Golog, the robot's actions are typically modeled on an abstract level, where complex actions such as picking up an object are treated as atomic primitives with deterministic effects and preconditions that only depend on the current state. However, executing such an action on a robot is a complex task involving multiple steps with additional temporal preconditions and timing constraints. Furthermore, the action may be noisy, e.g., producing erroneous sensing results and not always having the desired effects. While these aspects are typically ignored in reasoning tasks, they need to be dealt with during execution. In this thesis, we propose several approaches towards closing this gap. Based on a variant of the situation calculus that incorporates metric time and metric temporal logic, we propose modeling the robot platform with timed automata and temporal constraints to describe the connection between the high-level actions and the robot platform. We then describe two approaches towards transforming the high-level program. First, we view the transformation as a synthesis problem, where the task is to synthesize a controller that executes the program while satisfying the specification, independent of the environment's choices. We show that the synthesis problem is decidable, describe an algorithm to construct a controller, and evaluate the approach in two robotics scenarios. While this approach supports controlling Golog programs against a specification with timing constraints, the synthesis problem has non-primitive recursive complexity and therefore does not scale well. For this reason, we describe a second approach based on some simplifying assumptions which allow us to view the transformation problem as a reachability problem on timed automata, which can be solved with state-of-the-art tools. We demonstrate the effectiveness and scalability of the approach in a number of scenarios. Finally, we turn towards noisy sensors and effectors. Based on DS, a probabilistic variant of the situation calculus that allows modeling the agent's degree of belief, we describe an abstraction framework for Golog programs with noisy actions. In this framework, a high-level and non-stochastic program is mapped to a more detailed and stochastic low-level program. As the high-level program is non-stochastic, we may use non-probabilistic reasoning methods such as task planning. At the same time, by mapping the abstract actions to low-level programs, we may still deal with uncertainty during execution. We define a suitable notion of bisimulation that guarantees the equivalence between the high-level and low-level programs and demonstrate the approach with an example. Es laden ein: die Dozentinnen und Dozenten der Informatik -- Stephanie Jansen Faculty of Mathematics, Computer Science and Natural Sciences HLTPR - Human Language Technology and Pattern Recognition RWTH Aachen University Theaterstraße 35-39 D-52062 Aachen Tel: +49 241 80-21601 sek(a)hltpr.rwth-aachen.de www.hltpr.rwth-aachen.de

9 Monate, 4 Wochen

2024

2023

2022

2021

2020

2019

2018

informatik-vortraege September 2023