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.