Computer Science Colloquium
Im Rahmen des Informatik-Kolloquiums, das von den Instituten des Fachbereichs Informatik, der Österreichischen Gesellschaft für Informatik (ÖGI), der Arbeitsgemeinschaft für Datenverarbeitung (ADV) sowie der Österreichischen Computergesellschaft (OCG) abgehalten wird, spricht
Technical University of Darmstadt
über das Thema:
Symbolic Verification of Graph Transformation Systems with Hardware Model Checkers
Zeit: 2017-03-01 13:00:00.0, 60 Minuten
Ort: Computer Science Building, HS 19
In this talk I present a novel symbolic bounded model checking approach to test reachability properties of model-driven software implementations. Given a concrete initial state of a software system, a type graph, and a set of graph transformations, which describe the system's structure and its behavior, the system is verified against a reachability property. This reachability property is expressed in terms of a graph constraint. Without any user intervention, the presented approach exploits state-of-the-art model checking technologies successfully used in hardware industry and reports the result back to the user. I demonstrate the efficiency of the approach based on a case study.
Sebastian Gabmeyer is a post-doc at TU Darmstadt since January 2016. He finished his PhD on model checking based verification techniques for graph transformations under the supervision of Gerti Kappel and Martina Seidl in 2015. After a brief intermezzo in industry he joined the Security Engineering Group led by Stefan Katzenbeisser where he works on hardware based cryptography like Physical Unclonable Functions and remote software attestation.
Einladender: Assoz.-Prof. Dr. Martina Seidl