research interests

My research focusses on foundations and solutions for contemporary ubiquitous everyday, everywhere software — addressing today's and tomorrow's demand for safe, secure, reliable, correct, distributable, fault-tolerant, modular, reliable, maintainable, testable, resilient and efficient software systems. My central target is automatic, algorithmic and "auto-magic" support for the software engineering of today's ubiquitous concurrent, asynchronous and distributed systems. These challenge the software engineer to obtain a deeper understanding of the underlying concurrency and parallelism to assure high quality software, which, ideally, can be proven to be correct "by design".

principal research axes

• specification, verification and validation of the correctness (safety, security, etc.) of complex, safety-critical software systems written in state-of-the-art programming languages and APIs that are based on dynamic asynchronous concurrent distributed computation models
• automatic verification and self-healing of code on the runtime level
• formal methods for the designer of the underlying concurrency abstractions
• graph-based models as theoretical common ground
• diagrammatic languages as pragmatic lingua franca
• applying formal methods on the software engineering process itself to assure the safety and security of the software "by design"

keywords

actor model, abstraction and refinement techniques, bounded phase/context approximation, CEGAR, communicating automata models, compositional approaches, counter automata, diagrammatic logics, distributed and concurrent graph algorithms, dynamic systems of pushdown automata, fifo queues (reliable & unbounded), formal diagrammatic reasoning systems, formal specification languages, formal semantics, game theory, imperfect information games, graph-based models for software engineering, graphs as models (inside/outside computer science), graph transformation systems, graph rewriting, hyperedge replacement grammars, interpolation, logics, McScM, message sequence charts, network analysis, (extended) Petri nets, orchestration of components, partial order semantics, policy reasoning, protocol verification, queue automata, secure software engineering, template-based approaches, temporal logics, (Mazurkiewicz) traces, treewidth, runtime analysis, SCOOP, Spider Diagrams, Spark, VAS(S), web services, WSTS;