Detail

From Verification To Development of Message Passing Programs

Formal analysis of software systems is of crucial importance in the delivery of reliable systems. In the last decades there has been a significant research effort dedicated to the development of verification techniques and tools that allow to ensure correctness properties of programs. Noticeably, such approaches have explored in depth precise relations between implementations and specifications, in particular via specification logics and type systems. Such rich precise relations can be instrumental in the establishment of new software development methodologies, as they bridge crisper and faster to write specifications with implementations that are more error prone. In this talk we present a small tale on how type-system based verification techniques inspired a change of focus from verification tools to
development methods centered on global protocol specifications. Such specifications originate in type languages designed to capture the interaction of multiple parties in a structured way, but their usage as a verification artifact has been progressing to a different nature, as they are now being used as the main programming artifact.