SISTER

Project SISTER was about Reduction Systems: synthesis, refinement and verification of behavioural models.

The goal of this project was to obtain a general methodological framework for the synthesis and improvement of behavioral semantics, and their application in reasoning and verification methods for computational systems. The problem of systematically deriving behavioral semantics from reduction-based semantics was been the subject of the previous project PRIN 2005 ART, of which the current project was proposed as a natural continuation, mainly to lay the foundations for the introduction of abstract reasoning and verification techniques. For this aim, the project started from methodologies for the synthesis of behavioral semantics, moved to the development of analysis and refinement techniques of these semantics, and finally dealt with the definition of general verification and reasoning techniques. Thus, differently from the ART project, the methodological aspect was not limited to the definition of behavioral semantic models, but it was also extended to the improvement of such models, and to the definition of verification techniques, keeping in any case the same generality and abstraction level of the synthesis techniques already studied.

In this project I was principal investigator of the Udine site.

A lot of nice category theory also here, with also concrete applications. Yup, we were doing ACT before it was called ACT.