Computer Science Colloquium
Technical University of Darmstadt
Symbolic Verification of Graph Transformation Systems with Hardware Model CheckersWed 01.03.2017, 13:00, 60 minutes
Computer Science Building, HS 19
AbstractIn 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.
BioSebastian 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.
Invited by Assoz.-Prof. Dr. Martina Seidl
The Computer Science Colloquium is organized by the Department of Coputer Science at JKU, the Österreichische Gesellschaft für Informatik (ÖGI) and the Österreichische Computergesellschaft (OCG).