Categorical and Logical Methods in Model Transformation – CLIMT

There are many different methods which contribute to improving software
quality. They range from requirement techniques, architecture design,
specification languages and programming languages to testing and program
verification techniques. Such methods are often specific to a programming
paradigm. Rule-based programming and high-level replacement systems constitute
one of the most promising abstract programming paradigms. The merits of string
and term rewriting are well known, in particular when it comes to applying
verification techniques. However, several real-life problems cannot be
encoded easily by means of trees but need more powerful structures such as
graphs. Graphs are actually common mathematical structures which are visual
and intuitive. They constitute a natural and high-level way for system
modeling in several areas of science including computer science (such as
Model Driven Engineering and security analysis), life sciences, business
processes, etc.

The goal of the project CLIMTconsists in developing new very high level
frameworks to formally design and prove rule-based programs which
handle complex structures modeled as graphs. To achieve this goal, we
plan to organize our investigation according to three lines of research:

1. The first line consists in investigating new classes of graph
transformation systems with particular emphasis on new features such as
cloning and inductive attributes. Here, category theory provides a
declarative setting, abstracting away from particular implementation methods
or logical frameworks.

2.The abstract setting will be concretized in a second line of
research which consists in devising new logics and proof techniques
dedicated to express and to perform semi-automatically the proofs of
correctness and properties of the considered rewriting systems. The
emphasis here is on developing a notion of graph transformation
programs, on deriving a logic for reasoning about these programs,
and on formalizing this logic in an interactive proof assistant,
thus permitting machine-supported verification of graph
transformations.

3. In a third line, we aim at offering substantial proof automation, by
extracting proof obligations to be simplified by focused tactics or to be
proved by specialized decision procedures or solvers, such as SAT or SMT
solvers. Particular emphasis will be put on avoiding the generation of
redundant proof obligations in the first place. On the basis of the previously developed
formalization, the soundness of these optimizations can be ensured.


This project will be an opportunity to gather complementary skills in
graph transformation, automated theorem proving, type theory and logic in order to
propose new formal methods, efficient techniques and specific tools
for the development and certification of rule-based programs operating
on graphs.