The GReTA Graph TRansformation Theory and Applications virtual seminar series aims to serve as a platform for the international graph rewriting community, to promote recent developments and trends in the field, and to permit a regular networking and interaction between members of this community. Seminars are held twice a month in the form of Zoom sessions (some of which will be live-streamed to YouTube).

Several options are available to receive regular updates on the GReTA seminars:

Seminars

Java Bytecode Verification and Manipulation based on Model Driven Engineering

Program transformations are frequently developed, e.g., to realize programming language extensions or dynamic program analyses such as profiling. They are typically implemented by manipulating bytecode as the availability of source code is not guaranteed. There are standard libraries such as ASM that are typically used for implementing Java bytecode manipulations. To check their correctness, they are usually tested by applying them to different programs, running the manipulated programs and observing their behaviors. As part of the second step, the Java virtual machine verifies the bytecode, which can uncover errors in the bytecode introduced by the manipulation. That approach uses different technologies that are not well linked making the process of developing and testing bytecode manipulations difficult.

In this talk, we intend to perform bytecode manipulation by using concepts and techniques of model-driven engineering. We are convinced that the declarative nature of model transformation rules allows the debugging and analyzing of bytecode manipulations in more details than classically done. Following this path, a meta-model for bytecode is needed including OCL constraints for bytecode verification. We show that basing bytecode manipulation on model transformation can provide more immediate guidance and feedback to the developer, especially when model transformation is formally based on graph transformation. Bytecode verification can take place directly in the manipulated model with the help of OCL checking, eliminating the need to use multiple technologies. In some cases, it is even possible to automatically determine application conditions under which bytecode manipulations are correct by construction; then bytecode verification after a bytecode manipulation can be avoided altogether.

Confluence of Graph Transformation

Confluence has been studied for graph transformation since several decades now. Confluence analysis has been applied, for example, to determining uniqueness of model transformation results in model-driven engineering. It is strongly related to conflict analysis for graph transformation, i.e. detecting and inspecting all possible conflicts that may occur for a given set of graph transformation rules. The latter finds applications, for example, in software analysis and design. Both conflict and confluence analysis rely on the existence and further analysis of a finite and representative set of conflicts for a given set of graph transformation rules.

Traditionally, the set of critical pairs has been shown to constitute such a set. It is representative in the sense that for each conflict a critical pair exists, representing the conflict in a minimal context, such that it can be extended injectively to this conflict (M-completeness). Recently, it has been shown that initial conflicts constitute a considerably reduced subset of critical pairs, being still representative in a slightly different way. In particular, for each conflict there exists a unique initial conflict that can be extended (possibly non-injectively) to the given conflict (completeness). Compared to the set of critical pairs, the smaller set of initial conflicts allows for more efficient conflict as well as confluence analysis.

We continue by demonstrating that initial conflicts (critical pairs) are minimally complete (resp. minimally M-complete), and thus are both optimally reduced w.r.t. representing conflicts in a minimal context via general (resp. injective) extension morphisms. We proceed with showing that it is impossible to generalize this result to the case of rules with application conditions (equivalent to FOL on graphs). We therefore revert to a symbolic setting, where finiteness and minimal (M-)completeness can again be guaranteed. Finally, we describe important special cases (e.g. rules with negative application conditions), where we are able to obtain minimally complete (resp. M-complete) sets of conflicts in the concrete setting again.

How to participate

The GReTA seminars are hosted via Zoom. For security reasons, participation in a given seminar requires a registration (via the link provided in the announcement of the seminar). Upon completion of the registration form (asking for the name, affiliation and email address), a personalized Zoom meeting link will be sent. For convenience, sessions will be open 15 minutes prior to the beginning of the seminar.

Please make sure that you have the latest Zoom client version installed, in particular if you wish to participate in the after-talk discussions (since these will make use of the breakout rooms feature, see here for usage instructions). If possible, please consider joining already during the 15 minutes prior to a given seminar, to ensure your Zoom setup is functioning properly.

Alternatively, if you prefer not to participate via Zoom, some seminars will be live-streamed to YouTube, where it will be possible to ask questions via the YouTube commenting functionality.

Seminar “etiquette”

Each seminar will be hosted by a chairperson who will introduce the speaker, watch incoming questions and who will decide if and when to interrupt the speaker for questions, or which questions should be postponed to after the talk.

After-seminar discussions

After each seminar, the main Zoom session will remain open for additional 30 minutes in order to allow for discussions and networking. Depending on the number of participants, it will be a possibility to gather into small breakout sessions as well.

Meet the GReTA Team

Organisers

Avatar

Jean Krivine

CNRS Researcher in Computer Science

Avatar

Nicolas Behr

CNRS Researcher in Computer Science

Avatar

Reiko Heckel

Professor in Software Engineering

Scientific Committee

Avatar

Andrea Corradini

Professor of Computer Science

Avatar

Barbara König

Professor of Computer Science

Avatar

Berthold Hoffmann

Bremen Senior Lecturer (emer.)

Avatar

Daniel Merkle

Professor of Computer Science

Avatar

Dan R. Ghica

Professor of Semantics of Programming Languages

Avatar

Detlef Plump

Associate Professor of Computer Science

Avatar

Eswaran Subrahmanian

Research Professor

Avatar

Fabio Gadducci

Professor of Computer Science

Avatar

Fernando Orejas

Professor of Computer Science

Avatar

Frank Drewes

Professor of Computer Science

Avatar

Gabriele Taentzer

Professor of Computer Science

Avatar

Hans-Jörg Kreowski

Professor in Computer Science (emer.)

Avatar

Jérôme Feret

Research fellow at INRIA

Avatar

Leen Lambers

Senior Researcher

Avatar

Maribel Fernandez

Professor in Computer Science

Avatar

Mark Minas

Professor of Computer Science

Avatar

Matthias Tichy

Professor in Software Engineering

Avatar

Paolo Baldan

Associate Professor of Computer Science

Avatar

Paolo Bottoni

Professor of Computer Science

Avatar

Paweł Sobociński

Professor of Trustworthy Software Technologies

Avatar

Rachid Echahed

CNRS Researcher in Computer Science

Avatar

Russ Harmer

CNRS Researcher in Computer Science

Avatar

Steffen Zschaler

Senior Lecturer in Computer Science

Avatar

Timo Kehrer

Professor of Computer Science

Avatar

Vincent Danos

Professor, Directeur de Recherches at CNRS