December 2023 - informatik-vortraege

Einladung: Informatik-Oberseminar Moritz Ibing
by Moritz Ibing 10 Dec '23

10 Dec '23

+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +********************************************************************** Zeit: Freitag, 22. Dezember 2023, 11.00 Uhr Ort: Gebäude E3, Seminarraum 118, Ahornstr. 55 Referent: Moritz Ibing M.Sc. Lehrstuhl Informatik 8 Thema: Localized Control over the Latent Space of Neural Networks Abstract: Neural networks (NNs) are prevalent today when it comes to analyzing (classifying, segmenting, detecting, etc.) or generating data in all kinds of modalities (text, images, 3D shapes, etc.). They are so useful in these areas, because they have great representation power, while being easy to optimize and generalizing well to unseen data. However, their complexity makes them hard to interpret and modify. Neural networks are usually used to compute a mapping between the data space and a so-called latent space. Often we are interested in local properties of such a mapping. For example, we might want to slightly change the embedding of a data point to achieve a different classification. Such local modifications however are difficult, as NNs usually have globally entangled properties. In this work we will propose ideas how to deal with this problem. Local control is especially of importance for shape representations. It has been shown that NNs are well suited to represent these e.g. as parametric or implicit functions. However, when a global function is used, local supervision is hard to model. We therefore impose additional structure on the latent space of functional representations, making them easier to work with and more expressive. Such a structured representation makes downstream tasks easier, as we are more versatile regarding the shapes we can represent, we can make use of its regularity for the network design, and it allows a compressed encoding that can help to reduce memory consumption. Our focus will be on general shape generation, but we will also present more specific applications like shape completion or super-resolution among others. Our approaches set the state-of-the-art among generative models both in previously used metrics and a newly introduced measure we adapt for this purpose. Es laden ein: die Dozentinnen und Dozenten der Informatik

1 0

Einladung: Informatik-Oberseminar Henri Lotze
by Henri Lotze 05 Dec '23

05 Dec '23

+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +********************************************************************** Zeit: Montag, 13. November 2023, 09.30 Uhr Ort: Informatikzentrum, E3, 2. Etage, Raum 9222 Referent: Henri Lotze M.Sc. Lehr- und Forschungsgebiet Theoretische Informatik Thema: Going Offline -- Delays, Reservations and Predictions in Online Computation Abstract: The study of classical online computation builds upon a rather simple model. The input to a given problem is not known in advance, decisions have to made immediately upon the arrival of a new element and these decisions are irrevocable. While this model is very well suitable to compute worst case bounds to a broad range of problems, there are some problems which are not well suited for this analysis. Naturally, problems that do not admit a constant approximation ratio in their offline formulation do not admit a constant competitive ratio in the worst case in the online formulation. However, some problems that are approximable still do not admit a constant competitive ratio when analyzed in the online case. For a subset of these problems, such as the Online Simple Knapsack problem and the class of general F-Node- and F-Edge-Deletion problems, the reason for this seems to be that a single, specific bad decision by an algorithm can be arbitrarily punished by an adversary. In this talk, we explore modifications of the classical online model with the aim to find natural models that on the one hand cover a large range of problems and on the other hand work against pathological kinds of instances that restrict an algorithm from obtaining a constant competitive ratio. To this end, we study three modifications of the classical online model. The models that we study are that of "Late Accepts" -- with Advice --, which allows to postpone decisions in online minimization problems until a current partial solution does not uphold a certain property anymore. The second one is that of "Reservations", in which any decision may be postponed for a cost proportional to the gain of an item. Finally, the model of "Bounded Predictions" allows an online algorithm to see the complete instance in advance, with a caveat: There is noise on the instance -- controlled by an adversary -- and each element may actually deviate from its prediction, up to factor that is known to the algorithm. We are able to partially classify the advice complexity of the complete class of both F-Node-Deletion and F-Edge-Deletion problems. We give tight bounds on the competitive ratio for the Online Simple Knapsack problem with Reservations for the whole range of possible reservation costs, i.e. for a factor between 0 and 1. Finally, we give partially tight bounds for the Online Simple Knapsack problem with Bounded Predictions for the whole range of possible noise factors on the size of the items. Es laden ein: die Dozentinnen und Dozenten der Informatik

2 1

[sekretariate] Einladung: Informatik-Oberseminar Jana Berger
by Elke Ohlenforst 04 Dec '23

04 Dec '23

+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +********************************************************************** Zeit: Mittwoch, 13. Dezember 2023, 16:00 Uhr Ort: Informatikzentrum Ahornstr. 55, Raum 5053.2 (B-IT) Referentin: Jana Berger M.Sc. Lehrstuhl Informatik 2 Thema: Applying Software Model Checking: Experiences and Advancements Abstract: We present a comprehensive investigation into the applicability of formal methods for software model checking, with a particular emphasis on the automotive sector. The work is grounded in a practical study carried out with Ford Motor Company, offering a basis for the exploration and enhancement of both commercial and academic model checking tools. In the first part of the study, we collaborated with Ford Motor Company to formalise their natural language requirements for two automotive case studies employing the commercial C code model checker, BTC EmbeddedPlatform. Our investigation focused on the verification of auto-generated C code from Simulink models, analysing the associated challenges and providing practical recommendations for both engineers and tool developers. Building on this foundation, we then applied academic C code model checkers to the same case studies, comparing their performance against BTC EmbeddedPlatform. This comparison yielded a fresh set of insights and recommendations aimed at enhancing academic model checking tools. The second part of this work addresses the development of new tools and methods aimed at advancing the state of the art in software model checking. First, we designed NITWIT, a novel violation witness validator based on C code interpretation. This approach yields fast execution with a minimal memory footprint and is agnostic of existing model checkers. Next, we developed a tool for writing specifications with formal semantics, tailored specifically for the automotive industry. This tool is capable of auto-generating (a) specifications in Simulink, BTC and pure C code for verification, streamlining the formal verification process, and (b) natural language representations with fixed semantics for stakeholders and non-experts to review and use. Finally, to better facilitate the testing and benchmarking of C code model checkers, we built a tool that generates C code. The style of the generated code borrows from the two case studies, thus providing a valuable resource for stress-testing model checkers while respecting non-disclosure agreements, offering a wide variety of controllable code metrics, features and transformers. In summary, this thesis provides new and relevant insights as well as novel tools aimed at improving the application and comparison of software model checking, particularly in the context of the automotive industry. It offers practical solutions to real-world challenges, and helps to bridge the gap between commercial and academic approaches to software model checking. Es laden ein: die Dozentinnen und Dozenten der Informatik

1 0