Computer Science ColloquiumIm 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 CheckersZeit: Wed 1.3.2017, 13:00, 60 Minuten
Ort: Computer Science Building, HS 19
ZusammenfassungIn 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.
VortragenderSebastian 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
Liste aller Vorträge