Formal Methods Group at Informatics Departament/PUC-Rio

O TecMF tem por objetivo a pesquisa, o desenvolvimento e a aplicação de tecnologia formal, isto é, que utiliza modelos matemáticos , lógicos e baseados em conhecimento, no apoio ao processo de desenvolvimento de software em todas as suas fases. Gostamos de aplicar Teoria da Prova, Teoria das Categorias, Sistemas Lógicos e Prova Assistida de Teoremas em Ciência da Computação em geral, particularmente em desenvolvimento e validação de sistemas, modelos de computação e complexidade computacional.

O grupo desenvolveu técnicas e ferramentas em transformação de programas, de 1993 a 2001, na geração de programas a partir de especificações de alto nível tanto quanto a sua aplicação ao problema de código legado. De de 2002 a 2012, o grupo desenvolveu técnicas e modelos lógico/formais com o objetivo de modelagem e validação de sistemas antecipatórios e com semânticas baseadas em Jogos e outros modelos de racionalidade., juntamente com um verificadore de modelos baseados em jogos. Usamos Teoria das Categhorias na modelagem e esppecificação de interoperabilidade formal em arquiteturas de software e sistemas baseados em conhecimento, ou ontologias. A partir de 2008 desenvolvemos lógicas e modelos para a representação de conhecimeto legal (Legal Ontologies) e normativo. Aplicações em refinamento e análise formal de conformidade de bases de conhecimento normativo para o mercado de segurança da informação, resolução de paradoxos legais e putras aplicações mais sofisticadas. Atualmente o grupo está bastante envolvido em torno da complexidade computacional de provas de teoremas e obtenção de provas curtas em lógica proposicional.

Talks

2019

2018

2016:

2015:

2014:

2013:

2012:

2011:

2010:

2009:

2007:

2006:

Events

TecMF: FrontPage (last edited 2020-10-16 18:23:36 by EdwardHermann)