Cookies Policy
The website need some cookies and similar means to function. If you permit us, we will use those means to collect data on your visits for aggregated statistics to improve our service. Find out More
Accept Reject
  • Menu
About
Download Photo HD

About

Alexandre is a member  HASLab INESC TEC currently developing the postdoc project "dynamic logics for every season" supported by the FCT (Portuguese Foundation for Science and technology) with the individual grant SFRH /BPD/103004/2014. The project is hosted in HASLab INESC TEC and CIDMA over the scientific supervision of Luís S. Barbosa (Informatics Dep. of Univ. Minho) and Manuel A. Martins(Mathematics Dep. of Univ. Aveiro).

Alexandre is also coordinating the FCT R&D project DaLí: Dynamic logics for cyber-physical systems: towards contract based design.

Research interest:

- Mathematical Foundations of Software Engineering

- Algebraic and logical methods for software development

- Parametric generation of Modal/Hybrid/Dynamic Logics

- Process Algebra 

Interest
Topics
Details

Details

  • Name

    Alexandre Castro Madeira
  • Role

    External Research Collaborator
  • Since

    01st November 2011
  • Nationality

    Portugal
  • Contacts

    +351253604440
    alexandre.c.madeira@inesctec.pt
002
Publications

2020

Introducing Synchrony in Fuzzy Automata

Authors
Gomes, L; Madeira, A; Barbosa, LS;

Publication
Electronic Notes in Theoretical Computer Science

Abstract

2020

DaLi - Dynamic Logic, new trends and applications

Authors
Benevides, MRF; Madeira, A;

Publication
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING

Abstract

2020

A Fuzzy Modal Logic for Fuzzy Transition Systems

Authors
Jain, M; Madeira, A; Martins, MA;

Publication
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE

Abstract
This paper intends to contribute with a new fuzzy modal logic to model and reason about transition systems involving uncertainty in behaviours. Our formalism supports fuzziness at transitions and on the proposition symbols assignment levels. Against of other approaches in the literature, our bisimulation and bisimilarity notions generalise the analogous standard notions of classic modal logic and of process algebras. Moreover, the outcome of our logic is also fuzzy, with the semantic interpretation of connectives supported by the Godel algebra.

2019

Taming Hierarchical Connectors

Authors
Proença, J; Madeira, A;

Publication
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Abstract
Building and maintaining complex systems requires good software engineering practices, including code modularity and reuse. The same applies in the context of coordination of complex component-based systems. This paper investigates how to verify properties of complex coordination patterns built hierarchically, i.e., built from composing blocks that are in turn built from smaller blocks. Most existing approaches to verify properties flatten these hierarchical models before the verification process, losing the hierarchical structure. We propose an approach to verify hierarchical models using containers as actions; more concretely, containers interacting with their neighbours. We present a dynamic modal logic tailored for hierarchical connectors, using Reo and Petri Nets to illustrate our approach. We realise our approach via a prototype implementation available online to verify hierarchical Reo connectors, encoding connectors and formulas into mCRL2 specifications and formulas. © 2019, IFIP International Federation for Information Processing.

2019

Generalising KAT to Verify Weighted Computations

Authors
Gomes, L; Madeira, A; Soares Barbosa, L;

Publication
SCIENTIFIC ANNALS OF COMPUTER SCIENCE

Abstract
Kleene algebra with tests (KAT) was introduced as an algebraic structure to model and reason about classic imperative programs, i.e. sequences of discrete transitions guarded by Boolean tests. This paper introduces two generalisations of this structure able to express programs as weighted transitions and tests with outcomes in non necessarily bivalent truth spaces: graded Kleene algebra with tests (GKAT) and a variant where tests are also idempotent (I-GKAT). In this context, and in analogy to Kozen's encoding of Propositional Hoare Logic (PHL) in KAT we discuss the encoding of a graded PHL in I-GKAT and of its while-free fragment in GKAT. Moreover, to establish semantics for these structures four new algebras are defined: FSET(T), FREL(K,T) and FLANG(K,T) over complete residuated lattices K and T, and M (n, A) over a GKAT or I-GKAT A. As a final exercise, the paper discusses some program equivalence proofs in a graded context.

Supervised
thesis

2018

Contracts on-demand

Author
Leandro Rafael Moreira Gomes

Institution
UM

2016

Contracts on-demand

Author
Leandro Rafael Moreira Gomes

Institution
UM

2015

Validação do IEC 61131-3 Programmable Logical Controllers em KeyMaera

Author
Yoan David Ribeiro

Institution
UM