Alfio Ricardo de Brito Martini

Possui graduação em Bacharelado em Matematica Aplicada à Informàtica pela Universidade Luterana do Brasil (1992), mestrado em Computação pela Universidade Federal do Rio Grande do Sul (1994) e doutorado em Ciência da Computação pela Technische Universität Berlin (1999). Trabalha principalmente nos seguintes temas: métodos formais, teoria das categorias, sistemas lógicos na ciência da computação e prova interativa de teoremas.

Informações coletadas do Lattes em 23/09/2025

Acadêmico

Formação acadêmica

Doutorado em Ciência da Computação

1995 - 1998

Technische Universität Berlin, TUBerlin
Título: Relating Arrows Between Institutions in a Categorical Framework
Orientador: Hartmut Ehrig
Coorientador: Uwe Egbert Wolter. Bolsista do(a): Conselho Nacional de Desenvolvimento Científico e Tecnológico, CNPq, Brasil. Palavras-chave: Teoria das Categorias; Especificação Formal; Semântica Formal.Grande área: Ciências Exatas e da TerraGrande Área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Matemática da Computação / Especialidade: Teoria das Categorias. Grande Área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Matemática da Computação / Especialidade: Especificação Formal. Setores de atividade: Informática.

Mestrado em Computação

1992 - 1994

Universidade Federal do Rio Grande do Sul
Título: Uma Introducao à Teoria das Categorias e sua Aplicacao à Ciência da Computacão,Ano de Obtenção: 1995
Orientador: Daltro José Nunes
Bolsista do(a): Conselho Nacional de Desenvolvimento Científico e Tecnológico, CNPq, Brasil. Palavras-chave: Teoria das Categorias; Especificação Formal; Semântica Formal.Grande área: Ciências Exatas e da TerraSetores de atividade: Informática.

Graduação em Bacharelado em Matematica Aplicada à Informàtica

1989 - 1992

Universidade Luterana do Brasil

Idiomas

Inglês

Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.

Alemão

Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.

Áreas de atuação

Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Matemática da Computação/Especialidade: Especificação Formal.

Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Matemática da Computação/Especialidade: Lógica Matemática.

Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Matemática da Computação/Especialidade: Teoria das Categorias.

Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Matemática da Computação/Especialidade: Semântica Formal.

Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Matemática da Computação/Especialidade: Teoria da Computacao.

Participação em eventos

Spring School 2016 on Logic and Verification. 2016. (Seminário).

4th World Congress and School on Universal Logic. A Fibred and Indexed Semantics for a Hoare-like Logic. 2013. (Congresso).

XIV Encontro Brasileiro de Lógica.XIV Brazilian Logic Conference. 2006. (Encontro).

2nd Congress on Logic Applied to Technology. 2nd Congress on Logic Applied to Technology, LAPTEC2001, 12-14 Novembro, São Paulo, Brasil. 2001. (Congresso).

4th Brazilian Workshop on Formal Methods. 4th Brazilian Workshop On Formal Methdos. 2001. (Congresso).

7th International Conference on Algebraic Methodology and Software Technology (AMAST98). 7th International Conference on Algebraic Methodology and Software Technology. 1999. (Congresso).

13th International Workshop on Algebraic Development Techniques. WADT98. 1998. (Congresso).

European Joint Conference on Theory and Practice of Sofware. European Joint Conference on Theory and Practice of Software, ETAPS98. 1998. (Congresso).

Category Theory in Computer Science. CTCS97. 1997. (Congresso).

Dagstuhl-Seminar on Logic for System Engineering.Dagstuhl. 1997. (Seminário).

Formalism-Logic-Institution Relating, Translating and Structuring. 1997. (Encontro).

Formal Methods Europe 96. 1996. (Congresso).

Formalism-Logic-Institution Relating, Translating and Structuring. 1995. (Encontro).

International Workshop on Structures in Concurrency Theory. 1995. (Congresso).

Participação em bancas

Aluno: RODRIGO BORN VIEIRA

MARTINI, Alfio Ricardo de BritoHAEUSLER, Edward Hermann; PIMENTA, Marcelo. CaTRes-Ferramenta de Apoio à Pesquisa e Ensino em Teoria das Categorias. 2006. Dissertação (Mestrado em Computação) - Universidade Federal do Rio Grande do Sul.

Aluno: Sirlei Inês Sulzbach

MARTINI, Alfio Ricardo de Brito; DIVÉRIO, Tiarajú Asmuz; MOREIRA, Álvaro Freitas. Definição, Especificação Formal e Análise de Complexidade do Jogo Diferencial. 2005. Dissertação (Mestrado em Computação) - Universidade Federal do Rio Grande do Sul.

Aluno: Gleison Samuel do Nascimento

MARTINI, Alfio Ricardo de Brito; NUNES, Daltro; RIBEIRO, Leila. Identificação de Nomes Ativos em Agentes-pi Baseada em Tipos. 2005. Dissertação (Mestrado em Computação) - Universidade Federal do Rio Grande do Sul.

Aluno: Marnes Augusto Hoff

MARTINI, Alfio Ricardo de Brito; COSTA, Antônio Carlos da Rocha; TOSCANI, Laira Vieira. Grafos Internos e Multirrelações como Spans - Propriedades e Composicionalidade. 2005. Dissertação (Mestrado em Computação) - Universidade Federal do Rio Grande do Sul.

Aluno: Karina Girardi Rocha

MARTINI, Alfio Ricardo de Brito; COSTA, Antônio Carlos da Rocha; LAMB, Luis. Categoria de Grafos Parciais com Homorfismos Totais: Teoria e Aplicações. 2005. Dissertação (Mestrado em Computação) - Universidade Federal do Rio Grande do Sul.

Aluno: Christine Vieira

MARTINI, Alfio Ricardo de Brito. Investigação e Aplicação de Algumas Operações Categoriais entre Atores de uma Animação Baseados em Autômatos Finitos com Saída. 2004. Dissertação (Mestrado em Computação) - Universidade Federal do Rio Grande do Sul.

Aluno: Afonso Henrique Corrêa Sales

MARTINI, Alfio Ricardo de Brito. Formalismos Estruturados de Modelagens para Sistemas Markovianos Complexos. 2003. Dissertação (Mestrado em Ciência da Computação) - Pontifícia Universidade Católica do Rio Grande do Sul.

Aluno: Simone André da Costa

MARTINI, Alfio Ricardo de Brito; MENEZES, Paulo Blauth;HAEUSLER, Edward Hermann. Estudo dos Espaços Coerentes do Ponto de Vista da Teoria dos Topos. 2001. Dissertação (Mestrado em Computação) - Universidade Federal do Rio Grande do Sul.

Aluno: Carlos Antonio Pereira Campani

MARTINI, Alfio Ricardo de Brito; VELOSO, Paulo; OLIVEIRA NETO, Manuel Menezes de. Avaliação da Compressão de Dados e da Qualidade de Imagem em Modelos de Animação Gráfica para a Web. 2005. Tese (Doutorado em Computação) - Universidade Federal do Rio Grande do Sul.

Aluno: Ana Paula Lüdtke Ferreira

MARTINI, Alfio Ricardo de Brito; MOREIRA, Álvaro Freitas; MARTINS, Anamaria; NUNES, Daltro José. Object Oriented Graph Grammars. 2005. Tese (Doutorado em Computação) - Universidade Federal do Rio Grande do Sul.

Aluno: Renata Hax Sander Reiser

MARTINI, Alfio Ricardo de Brito; MENEZES, P. B.;HAEUSLER, Edward Hermann. A Máquina Geométrica: Um Modelo Computacional para Concorrência e Não-Determinismo Usando como Estrutura Espaços Coerentes. 2002. Tese (Doutorado em Computação) - Universidade Federal do Rio Grande do Sul.

Aluno: Tiago Mourão

MARTINI, Alfio Ricardo de Brito; PIMENTA, M. S.. SimCat: Um Simulador Gráfico de Teoria das Categorias para a Internet. 2001. Trabalho de Conclusão de Curso (Graduação em Bacharelado em Ciência da Computação) - Universidade Federal do Rio Grande do Sul.

Aluno: Leonardo Penczek

MARTINI, Alfio Ricardo de Brito. hyper-Automaton. 2000. Trabalho de Conclusão de Curso (Graduação em Bacharelado em Ciência da Computação) - Universidade Federal do Rio Grande do Sul.

MARTINI, Alfio Ricardo de Brito. Membro do Comitê de Programa do Simpósio Brasileiro de Linguagens de Programação - SBLP2006. 2006. Instituto Militar de Engenharia.

MARTINI, Alfio Ricardo de Brito. Membro do Comitê de Programa - SBLP2005. 2005. Universidade de Pernambuco.

MARTINI, Alfio Ricardo de Brito. Membro do Comitê de Programa do SBLP2004. 2004. Universidade Federal Fluminense.

MARTINI, Alfio Ricardo de Brito. Membro de Comitê de Programa - VODCA2004 (Views on Designing Complex Architectures). 2004. Universitá degli Studi di Pisa.

MARTINI, Alfio Ricardo de Brito. Membro de comitê de programa do Simpósio Brasileiro de Linguagens de Programação. 2003. Pontifícia Universidade Católica de Minas Gerais.

MARTINI, Alfio Ricardo de Brito. Membro de comitê de programa do Simpósio Brasileiro de Linguagens de programação. 2002. Pontifícia Universidade Católica do Rio de Janeiro.

Orientou

Juliana Kaizer Vizzotto

Interoperabilidade Logica atraves de Mapeamentos entre Instituicoes; 2001; Dissertação (Mestrado em Computação) - Universidade Federal do Rio Grande do Sul, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Alfio Ricardo de Brito Martini;

Fernando Trindade

Aplicação Web de Governança de TI para Organizações Públicas; 2018; Trabalho de Conclusão de Curso; (Graduação em Sistemas de Informação) - Pontifícia Universidade Católica do Rio Grande do Sul; Orientador: Alfio Ricardo de Brito Martini;

Jader Adalberto F

da Cunha;Davi Ritter Aroldi; Aplicativo de Interação Educacional entre Professores e Alunos - ASKAPP; 2017; Trabalho de Conclusão de Curso; (Graduação em Sistemas de Informação) - Pontifícia Universidade Católica do Rio Grande do Sul; Orientador: Alfio Ricardo de Brito Martini;

Tiago da Silva Cunha

Análise e Verificação de Especificações Z com Alloy e Isabelle; 2010; Trabalho de Conclusão de Curso; (Graduação em Ciência da Computação) - Pontifícia Universidade Católica do Rio Grande do Sul; Orientador: Alfio Ricardo de Brito Martini;

Emanuel Verardi Neto

Modelagem, Verificação e Prototipação do Protocolo de Segurança TLS; 2006; Trabalho de Conclusão de Curso; (Graduação em Ciência da Computação) - Pontifícia Universidade Católica do Rio Grande do Sul; Orientador: Alfio Ricardo de Brito Martini;

Meickel Freiberger Schaefer

Em Direção a um Modelo Formal para a Semântica Web; 2006; Trabalho de Conclusão de Curso; (Graduação em Ciência da Computação) - Pontifícia Universidade Católica do Rio Grande do Sul; Orientador: Alfio Ricardo de Brito Martini;

Felipe Pasquali

Um Interpretador para Especificação e Execução de Algoritmos; 2005; Trabalho de Conclusão de Curso; (Graduação em Ciência da Computação) - Pontifícia Universidade Católica do Rio Grande do Sul; Orientador: Alfio Ricardo de Brito Martini;

Miguel Orlandi

Modelagem e Análise do Protocolo de Needhamm-Schroeder através de CSP; 2005; 0 f; Trabalho de Conclusão de Curso; (Graduação em Ciência da Computação) - Pontifícia Universidade Católica do Rio Grande do Sul; Orientador: Alfio Ricardo de Brito Martini;

Andrea Scherer

Especificação Formal de Sistemas de Software: Exemplos, Aplicações e Verificações; 2001; Trabalho de Conclusão de Curso; (Graduação em Bacharelado em Ciência da Computação) - Universidade Luterana do Brasil; Orientador: Alfio Ricardo de Brito Martini;

Produções bibliográficas

WOLTER, U. ; MARTINI, Alfio Ricardo de Brito ; HAEUSLER, E. H. . Towards a uniform presentation of logical systems by indexed categories and adjoint situations. JOURNAL OF LOGIC AND COMPUTATION , v. 25, p. 57-93, 2015.
MARTINI, Alfio Ricardo de Brito ; WOLTER, Uwe ; HAEUSLER, Edward Hermann . Fibred and Indexed Categories for Abstract Model Theory. Logic Journal of the IGPL , v. 15, p. 707-739, 2007.
HAEUSLER, Edward Hermann ; MARTINI, Alfio Ricardo de Brito ; WOLTER, Uwe . Some Models of Heterogeneous and Distributed Specifications based on Universal Constructions. In: J.-Y. Béziau;A. Costa-Leite. (Org.). Perspectives on Universal Logic. Monza: Polimetrica, 2007, v. , p. 297-318.
MARTINI, ALFIO . Programming Language Semantics with Isabelle/HOL. In: 2013 2nd WorkshopSchool on Theoretical Computer Science (WEIT), 2013, Rio Grande. 2013 2nd Workshop-School on Theoretical Computer Science. p. 14-21.
MARTINI, Alfio Ricardo de Brito ; HAEUSLER, Edward Hermann ; WOLTER, Uwe . Reasons and Ways to Cope with a Spectrum of Logics. In: Laptec 2001, 2001, Sao Paulo. Frontiers of Artificial Intelligence and its Applications, 2001. v. 71. p. 148-155.
MARTINI, Alfio Ricardo de Brito ; HAEUSLER, Edward Hermann ; WOLTER, Uwe . A Taste on Putting Logical Systems Together. In: IV Brazilian Workshop on Formal Methods, 2001, Rio de Janeiro. IV Brazilian Workshop on Formal Methods, 2001. p. 95-100.
RHODE, M. G. ; MARTINI, Alfio Ricardo de Brito . Relating Z and the Logic of Transition Specifications. In: IV Brazilian Workshop on Formal Methods, 2001, Rio de Janeiro. IV Brazilian Workshop on Formal Methods, 2001. p. 89-94.
VIZZOTTO, J. K. ; MARTINI, Alfio Ricardo de Brito . Reutilizando Provas atraves de Mapeamentos entre Instituicoes. In: IV Brazilian Workshop on Formal Methods, 2001, Rio de Janeiro. IV Brazilian Workshop on Formal Methods. p. 101-106.
MARTINI, Alfio Ricardo de Brito ; WOLTER, Uwe . A Single Perspective on Arrows between Institutions. In: AMAST´98, 1999, Manaus. Lecture Notes in Computer Science. Manaus - Brazil, 1999. v. 1548. p. 486-501.
EHRIG, H. ; MARTINI, Alfio Ricardo de Brito ; WOLTER, Uwe . Categorical Concepts for Logical Systems and Formal Specifications in Computer Science. In: ISpecial issue in honour of Prof. Dieter Pumplun, 1998, Hagen. Seminar's Report from the Departament of Mathematics from FernUniversitaet Hagen. Hagen, Germany: FernUniversitaet, 1998. v. 63. p. 131-148.
MARTINI, Alfio Ricardo de Brito ; WOLTER, Uwe . A Systematic Study of Mappings between Institutions. In: International Workshop on Algebraic Development Techniques, 1998, Tarquinia. Lecture Notes in Computer Science. Berlin: Springer Verlag, 1997. v. 1376. p. 300-315.
WOLTER, Uwe ; MARTINI, Alfio Ricardo de Brito . Shedding New Light in the World of Logical Systems. In: Category Theory in Computer Science, 1997, Genova. Lecture Notes in Computer Science. Berlin: Springer Verlag, 1997. v. 1290. p. 159-176.
MARTINI, ALFIO . An Introduction to Interactive Theorem Proving with Isabelle/HOL. In: I Workshop Escola de Inverno em Teoria da Computação, 2017, Niterói. Livro de resumos: I WEITC/I Workshop Escola de Inverno em Teoria da Computação, 2017. p. 14-14.
PIANTA, J. ; Kudiess, Barbara ; Martini, A. . Proving Total Correctness of a Sorting Algorithm with Hoare Logic and Temporal Logic of Actions. In: I Workshop Escola de Inverno em Teoria da Computação (In English), 2017, Niterói. Livro de Resumos: I WEITC I Workshop Escola de Inverno em Teoria da Computação, 2017. p. 41-41.
Martini, A. . An Introduction to Interactive Theorem Proving with Isabelle/HOL. 2017. (Apresentação de Trabalho/Conferência ou palestra).
PIANTA, J. P. R. ; KUDIESS, B. ; Martini, A. . Proving Total Correctness of a Sorting Algorithm wit Hoare Logic and Temporal Logic of Actions. 2017. (Apresentação de Trabalho/Conferência ou palestra).
Martini, A. . Uma Introdução à Prova Interativa de Teoremas com Isabelle/HOL. 2013. (Apresentação de Trabalho/Conferência ou palestra).
MARTINI, ALFIO . Métodos Formais para Ciência da Computação 2018 (Apostila).
MARTINI, ALFIO . Lógica, Métodos Indutivos & Raciocínio Automátizado para Ciência da Computação 2018 (Apostila).
MARTINI, Alfio Ricardo de Brito ; RHODE, M. G. . Transition Specifications and the Algebraic Core of the Z-Notation 1996 (Relatório Técnico (TR 96-31)).
MARTINI, Alfio Ricardo de Brito ; ERMEL, C. . A Taste of Categorical Petri Nets 1996 (Relatório Técnico (TR 96-9)).
MARTINI, Alfio Ricardo de Brito . Category Theory and the Simply-Typed Lambda Calculus 1996 (Relatório Técnico (TR 96-7)).
MARTINI, Alfio Ricardo de Brito ; EHRIG, H. ; NUNES, Daltro . Graph Grammars - An Introduction to the Double-Pushout Approach 1996 (Relatório Técnico (TR 96-6)).
MARTINI, Alfio Ricardo de Brito . Elements of Basic Category Theory 1996 (Relatório Técnico (TR 96-5)).

Outras produções

MARTINI, Alfio Ricardo de Brito . WEIT 2017 - 4º Workshop-Escola de Informática Teórica. 2017.

MARTINI, Alfio Ricardo de Brito . WEIT 2015- 3º Workshop-Escola de Informática Teórica. 2015.

Projetos de pesquisa

2016 - Atual

Grupo DDC - Dependable Distributed Computing, Descrição: Objetivos da pesquisa: Propor, avaliar e experimentar sistemas concorrentes e distribuídos de alto desempenho e alta disponibilidade. Objetos de pesquisa: Sistemas distribuídos de alto desempenho e disponibilidade. Algoritmos distribuídos. Ambientes assíncronos. Tolerância a Falhas. Replicação. Modelos de consistência. Técnicas de durabilidade, recuperação e reconfiguração. Técnicas de programação para alto desempenho e confiabilidade. Demonstração de corretude de algoritmos concorrentes e distribuídos. Metodologias: Prototipação, Simulação, Especificação formal e análise. Aplicações: Algoritmos distribuídos de coordenação para: computação em nuvem (Google-Datastore e Microsoft-Azure-Tables); sistemas de gerenciamento de dados (Cassandra, Amazon-DynamoDB, Facebook-RocksDB, Oracle-NoSQL-Database); mecanismos de sincronização (Google-File-System, MapReduce, Google-DNS, Apache-ZooKeeper); comunicação confiável de alto desempenho (Paxos, Zab, Raft); entre outros. Financiamento: neste momento contamos com financiamento através do projeto CAPES PVE que tem como visitante estrangeiro o pesquisador Fernando Pedone e agrega a equipe de pesquisadores externos supra-citados. O projeto financia missões nacionais, internacionais, visitas do Prof. Pedone a universidades brasileiras, com especial atenção à PUCRS que é a instituição coordenadora do Projeto.. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) / Mestrado acadêmico: (4) / Doutorado: (1) . , Integrantes: Alfio Ricardo de Brito Martini - Integrante / Fernando Luis Dotti - Coordenador / Julio Henrique Pereira Machadi - Integrante / Fernando Lopes Pedone - Integrante.

Histórico profissional

Experiência profissional

2002 - 2019

Pontifícia Universidade Católica do Rio Grande do Sul

Vínculo: Professor Adjunto c/ Doutorado, Enquadramento Funcional: Dedicação Exclusiva (DE), Regime: Dedicação exclusiva.

Atividades

08/2002 - 01/2019
Pesquisa e desenvolvimento , Faculdade de Informática, .,Linhas de pesquisa
08/2002 - 01/2019
Ensino, Ciência da Computação, Nível: Graduação,Disciplinas ministradas, Lógica para Computação, Métodos Formais para Computação, Paradigmas de Modelos Formais, Sistemas Formais, Teoria da Computabilidade
12/2011 - 12/2017
Direção e administração, Faculdade de Informática, .,Cargo ou função, Coordenador do Curso de Ciência da Computação.
12/2005 - 03/2010
Outras atividades técnico-científicas , Faculdade de Informática, Faculdade de Informática.,Atividade realizada, Tutor do grupo PET Informática.

1999 - 2002

Universidade Luterana do Brasil

Vínculo: Professor Adjunto c/ Doutorado, Enquadramento Funcional: Horista, Carga horária: 40

Atividades

03/2000 - 07/2002
Pesquisa e desenvolvimento , Faculdade de Matemática, .,Linhas de pesquisa
08/1999 - 07/2002
Ensino, Bacharelado em Ciência da Computação, Nível: Graduação,Disciplinas ministradas, Linguagens Formais, Lógica de Predicados, Semântica Formal, Teoria da Computação

1999 - 2001

Universidade Federal do Rio Grande do Sul

Vínculo: Bolsista recém-doutor, Enquadramento Funcional: , Carga horária: 40

Atividades

03/1999 - 12/2001
Pesquisa e desenvolvimento , Instituto de Informática, .,Linhas de pesquisa
03/1999 - 12/2001
Ensino, Bacharelado em Ciência da Computação, Nível: Graduação,Disciplinas ministradas, Especificação Formal, Semântica Formal, Teoria das Categorias, Linguagens Formais