plt formal methods resources Download - plt formal methods resources download do código-fonte

plt formal methods resources

Outro código-fonte

1.0.0

Baixar

Teoria da Linguagem de Programação e Métodos Formais - Recursos

Cortesia de imagem: grupo Forsyte

Métodos formais são técnicas matemáticas usadas para projeto, verificação e especificações de problemas de software e hardware. Estes são essencialmente um subconjunto de pesquisas em Teoria da Linguagem de Programação que estão sendo usados para estudar problemas complexos de ciência da computação.

A análise por métodos formais envolve basicamente estas etapas:

Formal Specification
Formal Proofs
Model Checking
Abstraction

O desenvolvimento formal da prova e a verificação do modelo são feitos principalmente usando provadores de teoremas interativos, geralmente chamados de assistentes de prova. Abstração é a criação de relações estruturalmente sólidas entre partes de modelos.

Aqui está minha tentativa de fazer a curadoria de uma lista de materiais de leitura, vídeos e ferramentas úteis, acompanhada por alguns desafios futuros na área.

OBSERVAÇÃO :

Tentei tornar o conteúdo mais focado na pesquisa atual e na aplicação industrial. Quem procura acervo puramente acadêmico deve consultar Métodos Formais em Educação - Jeremy Avigad.
Espera-se que o leitor tenha algum conhecimento básico de Teoria dos Tipos . Uma visão mais acadêmica pode ser encontrada aqui learn-tt.

Conteúdo

Livros e Palestras
Blogues
MOOCs
Ferramentas
Projetos
Próximos Desafios
- Relacionado à segurança
  - Segurança de Software
  - Privacidade Diferencial
  - Aplicações em Segurança Block Chain
  - Desafios para tornar a IA segura
  - Crie sistemas ciberfísicos seguros
- Interpretação abstrata focada
- Pesquisa em linguagem de programação relacionada
  - Programação Probabilística
  - Desenvolvimento de linguagem de programação quântica
  - Refinamento da linguagem usando métodos formais
Indústrias e startups relacionadas

Livros e Palestras

Fundamentos de software : Aconselho fortemente isso como material de partida para se aprofundar neste campo. O livro é muito útil na construção de conceitos básicos e serve como uma introdução muito sólida ao campo. Conceitos lindamente ilustrados com exemplos para praticar são fornecidos em todo o conteúdo, tornando o teorema interativo que prova o aprendizado divertido.
FRAP - Adam Chlipala : Um livro que ajuda você a compreender e raciocinar sobre a correção formal dos programas. Exemplos inspirados em linguagem imperativa ( C ) de estruturas de dados e algoritmos ajudam imensamente a começar a pensar sobre sua verificação formal.
Programação Certificada com Tipos Dependentes - Adam Chlipala : Um dos melhores theoretical books para aprender a provar teoremas usando coq.
Verificação Formal - Jacques Fleuriot : Este é um curso que envolve a prova de teoremas usando algumas ferramentas mais desenvolvidas, como solucionadores SAT e SMT.
Interpretação Abstrata - Patrick Cousot O melhor material disponível sobre a teoria da Interpretação Abstrata. Ele fornece uma análise matemática completa e pura das mutações do programa. O comportamento do Programa como uma relação continuamente modificadora entre diferentes estruturas matemáticas abstratas é explicado e comprovado!!.
Lógica e Prova - Introdução ao CMU e Lean : Este é um curso desenvolvido na CMU e também serve como material introdutório para prova de teoremas no Lean

Se você acha que precisa de mais insights teóricos, consulte a nota acima.

Blogues

Introdução aos métodos formais
Estrutura K e esforços de verificação formal em Blockchain
Verificação formal do Pacto para contratos inteligentes Blockchain: blog curto incrível explicando a metodologia do Pacto FV com uma pequena introdução à verificação formal pelos primeiros princípios.
Rumo a uma IA robusta e verificada: testes de especificações, treinamento robusto e verificação formal - DeepMind
O desafio da verificação e teste do aprendizado de máquina - Ian GoodFellow e Nicolas Papernot

MOOCs

Verificação formal de software - edX
Verificação de modelo quantitativo - Coursera
Sistemas Ciberfísicos : Curso pela UC Berkeley, focado no uso de métodos de verificação para modelagem de sistemas Cyper Physical (CPS).
Linguagens de programação - Coursera

Ferramentas

Assistentes de prova

coq: O provador de teoremas mais popular e amplamente utilizado. Ele suporta muitos recursos, incluindo extração de ML, empacotamento de projeto (criação de projeto e Makefile). Há muitos materiais how-to disponíveis que usam coq para formalização. Qualquer um pode achar estes 100 Teoremas em Coq muito interessantes.
lean: Um provador de teoremas relativamente novo da Microsoft Research . Tem um bom tutorial interativo, é fácil de começar.
Verificador de modelo PRISM: É um verificador de modelo desenvolvido pela Universidade de Oxford.
Nuprl: Provador de Teoremas de Cornell no âmbito do Projeto Lógica de Refinamento de Prova.
Agda: Um assistente de prova bastante maduro. Possui recursos semelhantes ao Coq. fácil de aprender depois de alguma experiência em coq.
Isabelle: É um antigo provador de teoremas. Possui uma boa implementação da lógica central, mas carece de outros recursos relacionados à UX.
VCC: Um verificador mecânico para programas C simultâneos da Microsoft.
TLA+: Linguagem de alto nível para modelagem de linguagens e sistemas (especialmente simultâneos e distribuídos).

Solucionadores SAT/SMT/SMC

Solucionadores SAT:

MiniSat.

Solucionadores SMT:

Z3
CVC4
MatemáticaSAT5
SMTInterpol
Princesa

Solucionadores SMC:

Publicação

Solucionadores Híbridos

Os Proof Assitants têm implementações muito fortes de lógica de programa. Às vezes pode não ser taticamente possível realizar provas complexas apenas usando-as. Portanto, a pesquisa atual combina este princípio de forte raciocínio baseado em lógica com poderosos solucionadores SMT e SMC para facilitar o desenvolvimento de provas. Alguns exemplos estão aqui abaixo:

Festrela(F*)
- É possível extrair o código F* para C usando KreMLin.
SMTCoq

Projetos

A maioria dos projetos são mais ou menos desenvolvimento dos respectivos provadores de teoremas ou SAT/SMT/SMC/solucionadores e, portanto, podem ser consultados lá. Estes são alguns de outros projetos desenvolvidos ativamente.

DeepSpec é um projeto abrangente que se concentra na construção de sistemas de software verificados. Os seguintes subprojetos principais são trabalhados ativamente:
- Compert
- LLVM verificado (VeLLVM)
- Cadeia de ferramentas de software verificada (VST)
ikos é um compilador C confiável e livre de bugs, baseado na teoria da interpretação abstrata.
Projeto Everest: É um projeto de pesquisa que visa criar um ecossistema HTTPS seguro e verificado.
CertiCrypt: É um projeto focado na modelagem de criptografia de chave pública utilizando o assistente de prova coq.
Iris: Iris é uma estrutura lógica de separação simultânea de ordem superior implementada e verificada no assistente de prova Coq.
VeriDeep - Verificação de segurança de redes neurais profundas
VeHICal: Projeto focado no desenvolvimento das bases do co-design verificado de interfaces e controle para sistemas ciber-físicos humanos.
FastSMT - Ferramenta para aprimorar seu solucionador SMT, aprendendo como otimizar seu desempenho para seu conjunto de dados de fórmulas. Ele é desenvolvido pelo laboratório SRI, ETH Zurich, construído sobre o solucionador Z3 SMT.
fm4cps - Métodos formais para sistemas ciberfísicos, esforços conjuntos do INRIA e ECNU Xangai.

Próximos Desafios

Relacionado à segurança

Segurança de Software
- Leituras
  - Métodos formais de segurança, workshop NSF
  - Relação Simbólica entre Métodos Formais e Segurança
  - Artigos de pesquisa do Projeto-Everest
  - Métodos formais em segurança de software
  - Métodos formais para sistemas de computadores seguros e protegidos
  - A solidez computacional da criptografia formal
  - Estruturas de segurança usando métodos formais
  - Verificação de Primitivo Criptográfico
  - Certificação formal de provas criptográficas baseadas em jogos
  - Certificação formal de provas criptográficas baseadas em código
- Vídeos
  - Especificação profunda para Dropbox
  - DSL para computação multipartidária segura e verificada em F*
  - Usando Métodos Formais para Desenvolvimento de Sistemas Altamente Seguros
  - Segurança através de Métodos Formais e Arquitetura Segura (CERIAS - Purdue University)
  - Técnicas baseadas em linguagem para criptografia e privacidade
Privacidade Diferencial
- Leituras
  - Verificação formal de privacidade diferencial para sistemas interativos
  - Métodos formais de privacidade
  - LightDP - Para automatizar provas diferenciais de privacidade
  - EasyCrypt - Privacidade diferencial computacional verificada com aplicações para medidor inteligente
  - Provando privacidade diferencial na lógica Hoare
  - Programação Bayesiana Diferencialmente Privada
  - Acoplamento Probabilístico Avançado para Privacidade Diferencial
- Vídeos
  - Métodos formais e provas de propriedades de privacidade - 1
  - Métodos formais e provas de propriedades de privacidade - 2
  - Métodos formais e provas de propriedades de privacidade - 3
  - Provando privacidade diferencial usando tipos relacionais
Aplicações em Segurança Block Chain
Métodos formais para Block Chains : Este é o primeiro workshop focado no uso de métodos formais na tecnologia Block Chain. Será no dia 11 de outubro de 2019 .
CertiK : É uma startup focada no uso de métodos formais para tornar blockchains comprovadamente seguros.
- Leituras
  - Como a análise e verificação formal adicionam segurança a sistemas baseados em Blockchain - Tutorial no MIT
  - Contratos inteligentes e oportunidades para métodos formais
  - Estrutura K e esforços de verificação formal em Blockchain, uma coleção incrível de material explicativo sobre a estrutura K e sua aplicação na verificação de sistemas Blockchain.
  - Verificação formal do Pacto para contratos inteligentes Blockchain: blog curto incrível explicando a metodologia do Pacto FV com uma pequena introdução à verificação formal pelos primeiros princípios.
  - Blockchains Temporais – uma análise formal
  - Validação de Contratos Inteligentes Descentralizados através da Teoria dos Jogos e Métodos Formais
- Vídeos
  - Design formal, implementação e verificação de linguagens BlockChain
  - CertiK - plataforma de verificação formal de contrato inteligente (revisão)
  - Simplicidade – Uma nova linguagem para blockchains
Desafios para tornar a IA segura
FLoC 2018- Summit of Machine Learning encontra métodos formais
Aprendizado de Máquina Verificado - Radboud University Nijmegen : Curso universitário sobre o uso de métodos de verificação em Aprendizado de Máquina.
Métodos formais encontram aprendizado de máquina - RWTH Aachen University : seminário de 2018 sobre avanços em aprendizado de máquina comprovadamente seguro usando métodos formais.
- Leituras
  - Rumo à Inteligência Artificial Verificada - S. Seshia
  - Rumo a uma IA robusta e verificada: testes de especificações, treinamento robusto e verificação formal - DeepMind
  - Desenvolvendo Sistemas de Aprendizado de Máquina BugFree com Matemática Formal
  - Misturando métodos formais, aprendizado de máquina e interação humano-computador
  - Aprendizado de máquina em métodos formais
  - Aprendizado de máquina e métodos formais
  - Algoritmos para verificação de redes neurais profundas
  - Verificação de segurança de redes neurais profundas
  - O desafio da verificação e teste do aprendizado de máquina - Ian GoodFellow e Nicolas Papernot
  - Verificando propriedades de redes neurais profundas binarizadas
  - Reluplex: um solucionador SMT eficiente para verificação de redes neurais profundas
  - Verificação de redes de feed forward linear por partes
  - Desafios na verificação de algoritmos de aprendizagem por reforço
  - Aplicando Métodos Formais em Aprendizagem por Reforço - Galois Inc.
  - Para provar a robustez adversária de redes neurais profundas
- Vídeos
  - Verificação de segurança para redes neurais profundas -ICST 2018
  - Verificação de segurança para redes neurais profundas - Marta Kwiatkowska - CAV 2017
  - Verificação de segurança para redes neurais profundas -INRIA
  - Regras de verificação de aprendizado de máquina, desde bugs baseados em dados até IA explicável
  - Verificação de programas de aprendizado de máquina
  - Reluplex: um solucionador SMT eficiente para verificação de redes neurais profundas - Vídeo de conferência
  - Desenvolvendo modelos de aprendizado de máquina sem erros usando Certigrad - Daniel Selsam
Crie sistemas ciberfísicos seguros
VeHICal : Projeto focado no desenvolvimento das bases do co-design verificado de interfaces e controle para sistemas ciber-físicos humanos.
fm4cps - Métodos formais para sistemas ciberfísicos, esforços conjuntos do INRIA e ECNU Xangai.
- Leituras
  - Projeto de Sistemas Ciber-Físicos: Fundações Formais, Métodos e Cadeias de Ferramentas Integradas
  - Novas fronteiras em métodos formais: aprendizagem, sistemas ciberfísicos, educação e muito mais
  - Verificação de modelo estatístico para sistemas ciberfísicos
  - Verificação formal de sistemas ciberfísicos de transporte
  - Verificação de Sistemas Ciber-Físicos
  - Verificação e validação em sistemas ciberfísicos: desafios de pesquisa e um caminho a seguir
  - Detecção de anomalias em sistemas ciberfísicos: uma abordagem de métodos formais
  - Verificação Composicional de Sistemas Ciber-Físicos Autoadaptativos
- Vídeos
  - Uma Carta de Métodos Formais para Sistemas Ciberfísicos e Internet das Coisas Industrial
  - Verificação formal de sistemas ciberfísicos
  - Monitoramento de sistemas ciberfísicos

Interpretação abstrata focada

Certificação de Robustez Rápida e Eficaz: projeto DeepZ - para certificação de robustez de redes neurais com base em interpretação abstrata.
AI2: Certificação de Segurança e Robustez de Redes Neurais com Interpretação Abstrata
Aumentando a Certificação de Robustez de Redes Neurais: Utiliza Interpretação Abstrata em sua metodologia.

Pesquisa em linguagem de programação relacionada

Programação Probabilística
- Leituras
  - Uma introdução à programação probabilística
  - Verificação formal de programas probabilísticos de ordem superior
  - Programação Lógica Probabilística e Redes Bayesianas
  - Funções probabilísticas e oráculos criptográficos em lógica de ordem superior - Andreas Lochbihler
  - Verificação Relacional Probabilística de Implementações Criptográficas
  - Provas de acoplamento são programas de produtos probabilísticos
  - Acoplamento Probabilístico Avançado para Privacidade Diferencial
  - Métodos Formais para Programação Probabilística
  - Métodos formais para programas probabilísticos: slides de aula
  - Programação Probabilística – Verdadeiro Desafio de Verificação
  - FairSquare: verificação probabilística da justiça do programa
  - VPHL: uma lógica de correção parcial verificada para programas probabilísticos
  - Unificando Lógica e Probabilidade
- Vídeos
  - Verificação formal de programas probabilísticos de ordem superior - vídeo da conferência POPL 2019
  - Programação lógica probabilística e suas aplicações - Luc De Raedt, Leuven
Desenvolvimento de linguagem de programação quântica
- Leituras
  - Qwire: Verificação formal de programas quânticos em Coq
  - Uma lógica para verificação formal de programas quânticos
  - Técnicas de acoplamento para raciocínio sobre programas quânticos
  - Verificação Formal vs Incerteza Quântica
  - Modelo de verificação de protocolos quânticos recursivos
- Vídeos
  - Computação quântica com capacidade de missão para verificação e validação de software (VV) - CMU
  - Dominique Unruh: Verificação formal da criptografia quântica
Refinamento de linguagens usando métodos formais

Trata-se particularmente de melhorar certas propriedades (como paralelismo e simultaneidade) de linguagens de programação existentes. Muito pode ser facilmente pesquisado a respeito disso, pois, afinal, esta é a única razão mais importante para estudar a teoria PL. Todas as conferências listadas aqui ACM SIGPLAN possuem a maioria dos artigos de pesquisa sobre desenvolvimento de linguagens de programação, verifique-os.