DEI Talks | Formal Verification of Distributed Systems por Julien Brunel e David Chemouil

Julien Brunel e David Chemouil são investigadores seniores na ONERA, em Toulouse, especializados em formal specification and verification. Juntamente com Nuno Macedo e Alcino Cunha (INESC TEC) conceberam a 6ª versão (até há pouco tempo designada Electrum) da linguagem e ferramenta Alloy (originalmente proposta pelo MIT). Nos últimos anos, Julien Brunel e David Chemouil têm vindo a estudar também a verificação de algoritmos distribuídos.

Segundo os investigadores “a recent highlight is the first mechanical proof of correctness of the distributed maintenance algorithm of the Chord peer-to-peer protocol, as well as formal techniques for the complete, semi-automatic verification of infinite-state systems, such as distributed algorithms”.

Junte-se a nós no dia 8 de Abril, às 14:30, na sala I-105 da FEUP, para a apresentação deste trabalho

 Abstract:

The verification of distributed systems is challenging because these systems combine a rich structure, a high number of elements and a non-trivial temporal evolution. A trade-off between automation and completeness of the verification has to be made. In particular, one can use theorem provers, which offer complete confidence but tend to require considerable expertise and effort. Another option is to use model checkers, which offer complete automation, but cannot handle complex data structures and configurations.

In this talk, they will present recent work on verification techniques for distributed systems that are automatic and “as complete as possible”, or complete and “as automatic as possible”. They will illustrate their work with the analysis of Chord, a scalable distributed hash table.

DEI Talks | JUMPING FINITE AUTOMATA por Prof. Alexander Meduna

Prof. Alexander Meduna (nascido em 1957 em Olomouc, República Checa) é um cientista informático teórico e especialista em desenho de compiladores, linguagens formais e autómatos. É professor de Informática na Brno University of Technology.

Anteriormente, ensinou informática teórica em várias universidades europeias e americanas, incluindo a Universidade do Missouri, onde passou uma década a ensinar tópicos avançados de teoria da linguagem formal. Escreveu mais de noventa artigos relacionados com teoria da computação.

Junte-se a nós no dia 7 de Abril, às 14:30, na sala I-105 da FEUP, para a apresentação de JUMPING FINITE AUTOMATA

Abstract:

This talk proposes a new investigation area in automata theory — jumping finite automata. These automata work like classical finite automata except that they read input words discontinuously — that is, after reading a symbol, they can jump over some symbols within the words and continue their computation from there. The talk gives several results concerning jumping finite automata in terms of commonly investigated areas of automata theory, such as closure properties. Most importantly, it achieves several results that demonstrate differences between jumping finite automata and classical finite automata. In its conclusion, the talk  formulates several open problems and suggests future investigation areas.

O seu último livro é o Handbook of Mathematical Models for Languages and Computation

Meduna, Alexander; Tomko, Martin, Horacek, Petr (2019)

The Institution of Engineering and Technology, Stevenage, UK, ISBN: 978-1-78561-660-0

https://www.amazon.ae/Handbook-Mathematical-Models-Languages-Computation/dp/1785616595

Alguns dos livros anteriores:

  • Meduna, Alexander (2000). Automata and Languages: Theory and Applications. Springer Science & Business Media. ISBN 9781852330743.
  • Meduna, Alexander (2007). Elements of Compiler Design. CRC Press. ISBN 9781420063233.
  • Meduna, Alexander (2014). Formal Languages and Computation: Models and Their Applications. CRC Press. ISBN 9781466513457.
  • Meduna, Alexander; Švec, Martin (2005). Grammars with Context Conditions and Their Applications. John Wiley & Sons. ISBN 9780471736554.
  • Meduna, Alexander; Techet, Jiří (2010). Scattered Context Grammars and Their Applications. WIT Press. ISBN 9781845644260.
  • Meduna, Alexander; Zemek, Petr (2014). Regulated Grammars and Automata. Springer. ISBN 9781493903696.
  • Meduna, Alexander; Soukup, Ondřej (2017). Modern Language Models and Computation: Theory with Applications. Springer. ISBN 9783319630991.

CreativityTalks | Prof. António Sampaio da Nóvoa será o próximo convidado

Há muitos “futurismos” que sugerem uma educação sem escolas, baseada nas imensas possibilidades das tecnologias e da inteligência artificial. Estes “futurismos” ganharam força com a pandemia e as diferentes formas de isolamento a que temos estado sujeitos. Mas a educação não se faz em “confinamento”, exige sempre uma relação, um encontro, um trabalho conjunto. Não é o momento de anunciar a “morte da escola”, mas antes a inventar de novo.

Inventar de novo a Escola” será  o tema da 6ª Creativity Talk, apresentado pelo Professor *António Sampaio da Nóvoa, no dia 17 de março, às 18:00, no Anfiteatro Nobre da FEUP (B032).

A sessão será moderada por Amélia Lopes, Professora Catedrática e Presidente do Conselho Cientifico da Faculdade de Psicologia e de Ciências da Educação da Universidade do Porto.

A participação presencial na palestra requer uma inscrição (gratuita) no Eventbrite (lugares disponíveis à lotação da sala pela ordem de registo).

Se não conseguir comparecer presencialmente na sessão, poderá assistir através do seguinte endereço: https://youtu.be/V2I0h0EQBO0

*Bio

António Sampaio da Nóvoa é Professor Catedrático da Universidade de Lisboa. É Doutor em História pela Universidade de Paris IV-Sorbonne e Doutor em Ciências da Educação pela Universidade de Genebra. Foi Reitor da Universidade de Lisboa entre 2006 e 2013. Foi Embaixador de Portugal junto da UNESCO entre 2018 e 2021.

DEI Talks | The Digital Score – “What’s really going on {in} here?” por Prof. Craig Vear

Craig Vear é Professor e Investigador na Universidade de Montfort onde é também Diretor do Laboratório de IA e Robótica Criativa no Instituto de Tecnologias Criativas. A sua investigação é naturalmente híbrida, pois reúne os campos da música, desempenho digital, tecnologias criativas, inteligência artificial, criatividade, jogos, realidade mista e robótica. Tem estado envolvido em investigação baseada na prática com tecnologias emergentes há quase três décadas, e foi editor do The Routledge International Handbook of Practice-Based Research, publicado em 2022. A sua recente monografia The Digital Score: creativity, musicianship and innovation, foi publicada pela Routledge em 2019, sendo também editor da série The Springer’s Cultural Computing Series. Em 2021 recebeu uma bolsa de 2 milhões de euros da ERC Consolidator Grant para continuar a desenvolver a sua pesquisa Digital Score – digiscore.dmu.ac.uk

Junte-se a nós no dia 24 de fevereiro, às 14:30, na sala B024 da FEUP, e assista à apresentação e discussão deste projeto –  Investigating Technological Transformation of the Music Score (DigiScore).

A secção de abertura posicionará a partitura digital entre uma compreensão mais ampla da função e do objetivo de todas as partituras: a de uma interface de comunicação entre músicos. Depois de definir aquilo que assinala uma partitura digital como uma proposta diferente, resumirá as finalidades e objetivos da investigação do projeto DigiScore. Irá posicionar esta investigação entre os princípios centrais do fluxo, da fenomenologia, da incorporação e do efeito dos meios de comunicação, e delinear o foco da investigação como procura de sentido a partir do interior dos atos criativos da partitura digital musicking (Small 1989). A secção final delineará alguns dos novos conhecimentos atuais, e apresentará questões-chave que discutirá com os presentes na sala como forma de permitir a sua voz no desenvolvimento destes investigadores e na expansão da comunidade de investigação nesta área.