Cookies
Usamos cookies para melhorar nosso site e a sua experiência. Ao continuar a navegar no site, você aceita a nossa política de cookies. Ver mais
Aceitar Rejeitar
  • Menu
Sobre
Download foto HD

Sobre

Short Bio (EN):

Alexandre Madeira é um membro do HASLab - INESC TEC que está  a desenvolver o projecto de pós-doutoramento  "dynamic logics for every season" suportado por uma bolsa individual BPD FCT (SFRH /BPD/103004/2014). O projecto é acolhido no HASLab - INESC TEC e no centro CIDMA sob orientação científica de Luís S. Barbosa (Dep. Informática, Univ. Minho) e Manuel A. Martins (Dep. Matemática da Univ. Aveiro).   O Alexandre é ainda o Investigador Responsável do projecto R&D da FCT "DaLí: Dynamic logics for cyber-physical systems: towards contract based design".   Interesses de Investigação:   - Fundamentos Matemáticos para a Engenharia de Software   - Métodos Lógicos e Algébricos para o Sesenvolvimento de Software   - Geração Paramétrica de Lógicas Modais/Hibridas/Dinamicas   - Algebra de Processos    

Tópicos
de interesse
Detalhes

Detalhes

  • Nome

    Alexandre Castro Madeira
  • Cluster

    Informática
  • Desde

    01 novembro 2011
002
Publicações

2020

Introducing Synchrony in Fuzzy Automata

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

Publicação
Electronic Notes in Theoretical Computer Science

Abstract

2020

A Fuzzy Modal Logic for Fuzzy Transition Systems

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

Publicação
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.

2020

DaLi - Dynamic Logic, new trends and applications

Autores
Benevides, MRF; Madeira, A;

Publicação
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING

Abstract

2019

Taming Hierarchical Connectors

Autores
Proença, J; Madeira, A;

Publicação
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

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

Publicação
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.

Teses
supervisionadas

2018

Contracts on-demand

Autor
Leandro Rafael Moreira Gomes

Instituição
UM

2016

Contracts on-demand

Autor
Leandro Rafael Moreira Gomes

Instituição
UM

2015

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

Autor
Yoan David Ribeiro

Instituição
UM