By Alexandre Madeira, HASLab/INESC TEC and University of Minho.

Abstract. We discuss in this talk a powerful logic to support the development of dynamic systems on various levels of abstraction, from property specifications concerning, e.g., safety and liveness requirements, to constructive specifications representing concrete programs. This is achieved by combining features of both hybrid and dynamic logics in the same formalism: regular expressions of actions – inherent to dynamic logic – allow the specification of abstract requirements; nominals – a feature of hybrid logic – allow to specify concrete relational structures. A systematic translation from a process algebra into a constructive fragment of this logic is provided. The verification of abstract properties in the concrete models provides a proof method for refinement correctness w.r.t. model class inclusion.

Keywords. Software engineering, formal specification and development, hybrid dynamic logic.

About the speaker. Alexandre Madeira holds a PhD degree from the MAPi, a joint doctoral program in Computer Science of the Universities of Minho, Aveiro and Porto. He is currently a member of HASLab/INESC TEC & University of Minho where he is developing his postdoc project “Dynamic Logics for Every Season” with an individual FCT grant. The project is hosted in HASLab and CIDMA under the scientific supervision of Lus S. Barbosa (Informatics Dep. of UMinho) and Manuel A. Martins (Mathematics Dep. of UAveiro). Throughout his career as a researcher, Alexandre worked on several areas in logic for specific software, namely, in variants of modal logics. Alexandre has published in many conferences and journals in his field, and he was awarded the IBM Scientific Prize in 2013 for his work on logics for software reconfigurability.

LOCATION AND TIME

Address:  University of Minho, Gualtar campus, Braga, Portugal.

Building. Departamento de Informatica, Building 07.

Coffee session: at 1:30PM-2PM, Sala de Estar, 4th floor.

Talks session: at 2PM-2:30PM, Auditório 1, ground floor.