Speaker / Predavač:
Hugo Torres Vieira
Title / Naslov:
From Verification to Synthesis of Communication Centered Systems
Abstract / Sažetak:
Formal analysis of Software systems has proved to be of crucial importance in the delivery of reliable systems. There has been a significant research effort in the last decades dedicated to the development of techniques and tools that allow to ensure some correctness properties of programs. Moreover, such approaches have explored in depth precise relations between implementations and specifications, in particular via specification logics and type systems. In this talk we present ongoing work on how to exploit such relations between programs and specifications aiming at the synthesis of correct by construction programs based on types that may serve as easier faster to write program specifications. In particular, our aim is to automatically generate the communication skeleton for message-passing programs based on behavioral type systems.