Descarga plt formal methods resources - plt formal methods resources Descarga de código fuente

plt formal methods resources

Otro código fuente

1.0.0

Descargar

Teoría del lenguaje de programación y métodos formales: recursos

Imagen Courtsey: Grupo Forsyte

Los métodos formales son técnicas matemáticas que se utilizan para el diseño, verificación y especificaciones de problemas de software y hardware. Se trata esencialmente de un subconjunto de investigaciones sobre la teoría del lenguaje de programación que se utilizan para estudiar problemas complejos de informática.

El análisis por métodos formales implica básicamente estos pasos:

Formal Specification
Formal Proofs
Model Checking
Abstraction

El desarrollo de pruebas formales y la verificación del modelo se realizan principalmente mediante demostradores de teoremas interactivos, a menudo denominados asistentes de pruebas. La abstracción consiste en crear relaciones estructuralmente sólidas entre partes de modelos.

Este es mi intento de seleccionar una lista de materiales de lectura, videos y herramientas útiles acompañados de algunos desafíos futuros en el campo.

NOTA :

He intentado que el contenido se centre más en la investigación actual y la aplicación industrial. Las personas que buscan una colección puramente académica deben consultar Métodos formales en educación - Jeremy Avigad.
Se espera que el lector tenga algunos conocimientos básicos de teoría de tipos . Puede encontrar una visión más académica aquí learn-tt.

Contenido

Libros y conferencias
Blogs
MOOC
Herramientas
Proyectos
Próximos desafíos
- Relacionados con la seguridad
  - Seguridad del software
  - Privacidad diferencial
  - Aplicaciones en seguridad de la cadena de bloques
  - Desafíos para hacer que la IA sea segura
  - Cree sistemas ciberfísicos seguros
- Resumen Interpretación enfocada
- Investigación del lenguaje de programación relacionada
  - Programación probabilística
  - Desarrollo del lenguaje de programación cuántica
  - Refinamiento del lenguaje utilizando métodos formales.
Industrias relacionadas y nuevas empresas

Libros y conferencias

Fundamentos de software : recomiendo encarecidamente esto como material de partida para profundizar en este campo. El libro es muy útil para desarrollar conceptos básicos y sirve como una muy buena introducción al campo. Se proporcionan conceptos bellamente ilustrados con ejemplos para practicar en todo momento, lo que hace que el aprendizaje interactivo de teoremas sea divertido.
FRAP - Adam Chlipala : un libro que le ayuda a comprender y razonar la corrección formal de los programas. Los ejemplos de estructuras de datos y algoritmos inspirados en el lenguaje imperativo ( C ) ayudan enormemente a comenzar a pensar en su verificación formal.
Programación certificada con tipos dependientes - Adam Chlipala : uno de los mejores theoretical books para aprender a demostrar teoremas usando coq.
Verificación formal - Jacques Fleuriot : este es un curso que implica la demostración de teoremas utilizando algunas herramientas más desarrolladas como solucionadores SAT y SMT.
Interpretación abstracta - Patrick Cousot El mejor material disponible sobre la teoría de la Interpretación abstracta. Proporciona un análisis matemático completo y puro de las mutaciones del programa. ¡¡Se explica y demuestra el comportamiento del programa como una relación en continua modificación entre diferentes estructuras matemáticas abstractas!!.
Lógica y prueba: introducción a CMU y Lean : este es un curso diseñado en CMU y también sirve como material introductorio para la demostración de teoremas en Lean.

Si cree que necesita más conocimientos teóricos, consulte la Nota anterior.

Blogs

Comenzando con métodos formales
K Framework y esfuerzos de verificación formal en Blockchain
Pact Formal Verification para contratos inteligentes Blockchain: Impresionante blog breve que explica la metodología de Pact FV con una pequeña introducción a la verificación formal según los primeros principios.
Hacia una IA robusta y verificada: pruebas de especificaciones, capacitación sólida y verificación formal - DeepMind
El desafío de la verificación y prueba del aprendizaje automático - Ian GoodFellow y Nicolas Papernot

MOOC

Verificación formal de software - edX
Comprobación de modelos cuantitativos - Coursera
Cyber Physical Systems : Curso impartido por UC Berkeley, enfocado en el uso de métodos de verificación para el modelado de sistemas Cyper Physical (CPS).
Lenguajes de programación - Coursera

Herramientas

Asistentes de prueba

coq: El demostrador de teoremas más popular y ampliamente utilizado. Admite muchas funciones, incluida la extracción de ML y el empaquetado de proyectos (creación de proyectos y Makefile). Hay mucho material how-to disponible que utiliza coq para la formalización. Cualquiera puede encontrar estos 100 teoremas muy interesantes en Coq.
lean: un demostrador de teoremas bastante nuevo de Microsoft Research . Tiene un buen tutorial interactivo, es fácil comenzar con él.
Verificador de modelos PRISM: es un verificador de modelos desarrollado por la Universidad de Oxford.
Nuprl: demostrador de teoremas de Cornell en el marco del proyecto de lógica de refinamiento de pruebas.
Agda: una asistente de prueba bastante madura. Tiene características similares a Coq. Fácil de aprender después de algo de experiencia en coq.
Isabelle: Es un viejo demostrador de teoremas. Tiene una buena implementación de la lógica central pero carece de otras características relacionadas con UX.
VCC: un verificador mecánico para programas C concurrentes de Microsoft.
TLA+: lenguaje de alto nivel para modelado de lenguajes y sistemas (especialmente concurrentes y distribuidos).

Solucionadores SAT/SMT/SMC

Solucionadores SAT:

MiniSat.

Solucionadores SMT:

Z3
CVC4
MatemáticasSAT5
SMTInterpol
Princesa

Solucionadores SMC:

Publicación

Solucionadores híbridos

Los asistentes de prueba tienen implementaciones muy sólidas de la lógica del programa. A veces, puede que no sea tácticamente posible realizar pruebas complejas únicamente utilizándolas. Por lo tanto, la investigación actual combina este principio de razonamiento basado en lógica sólida con potentes solucionadores SMT y SMC para facilitar el desarrollo de pruebas. Algunos ejemplos se encuentran a continuación:

Festrella(F*)
- Es posible extraer código F* a C usando KreMLin.
SMTCoq

Proyectos

La mayoría de los proyectos son más o menos desarrollo de los respectivos demostradores de teoremas o SAT/SMT/SMC/solucionadores y, por lo tanto, se pueden buscar allí. Estos son algunos de otros proyectos desarrollados activamente.

DeepSpec es un proyecto general que se centra en la creación de sistemas de software verificados. Se trabaja activamente en los siguientes subproyectos principales:
- compert
- LLVM verificado (VeLLVM)
- Cadena de herramientas de software verificada (VST)
ikos es un compilador de C confiable y libre de errores basado en la teoría de la interpretación abstracta.
Proyecto Everest: es un proyecto de investigación que tiene como objetivo crear un ecosistema HTTPS seguro y verificado.
CertiCrypt: Es un proyecto centrado en modelar criptografía de clave pública utilizando el asistente de prueba coq.
Iris: Iris es un marco lógico de separación concurrente de orden superior implementado y verificado en el asistente de prueba Coq.
VeriDeep: verificación de seguridad de redes neuronales profundas
VeHICal: Proyecto centrado en desarrollar las bases del codiseño verificado de interfaces y control para sistemas ciberfísicos humanos.
FastSMT: herramienta para mejorar su solucionador SMT aprendiendo a optimizar su rendimiento para su conjunto de datos de fórmulas. Está desarrollado por el laboratorio SRI, ETH Zurich, construido sobre el solucionador Z3 SMT.
fm4cps: métodos formales para sistemas físicos cibernéticos, esfuerzos conjuntos de INRIA y ECNU shanghai.

Próximos desafíos

Relacionados con la seguridad

Seguridad del software
- Lecturas
  - Métodos formales de seguridad, taller NSF
  - Relación simbólica entre métodos formales y seguridad
  - Artículos de investigación del Proyecto Everest
  - Métodos formales en seguridad del software
  - Métodos formales para sistemas informáticos seguros y protegidos
  - La solidez computacional del cifrado formal
  - Estructuras de seguridad utilizando métodos formales
  - Verificación de primitiva criptográfica
  - Certificación formal de pruebas criptográficas basadas en juegos
  - Certificación formal de pruebas criptográficas basadas en código.
- Vídeos
  - Especificación profunda para Dropbox
  - DSL para cálculos multipartitos seguros verificados en F*
  - Uso de métodos formales para el desarrollo de sistemas altamente seguros
  - Seguridad a través de Métodos FORMALES y Arquitectura Segura (CERIAS - Purdue University)
  - Técnicas basadas en lenguaje para criptografía y privacidad.
Privacidad diferencial
- Lecturas
  - Verificación formal de privacidad diferencial para sistemas interactivos
  - Métodos formales de privacidad
  - LightDP: hacia la automatización de las pruebas de privacidad diferenciales
  - EasyCrypt: privacidad diferencial computacional verificada con aplicaciones para medidores inteligentes
  - Demostrando la privacidad diferencial en la lógica de Hoare
  - Programación bayesiana diferencialmente privada
  - Acoplamiento probabilístico avanzado para privacidad diferencial
- Vídeos
  - Métodos formales y pruebas de propiedades de privacidad - 1
  - Métodos formales y pruebas de propiedades de privacidad - 2
  - Métodos formales y pruebas de propiedades de privacidad - 3
  - Demostrando privacidad diferencial usando tipos relacionales
Aplicaciones en seguridad de la cadena de bloques
Métodos formales para cadenas de bloques : este es el primer taller centrado en el uso de métodos formales en la tecnología Block Chain. Será el 11 de octubre de 2019 .
CertiK : Es una startup enfocada en utilizar métodos formales para hacer que las blockchains sean verificablemente seguras.
- Lecturas
  - Cómo el análisis formal y la verificación añaden seguridad a los sistemas basados en Blockchain - Tutorial @ MIT
  - Contratos inteligentes y oportunidades para métodos formales.
  - K Framework y esfuerzos de verificación formal en Blockchain una impresionante colección de material explicativo sobre K framework y su aplicación en la verificación de sistemas Blockchain.
  - Pact Formal Verification para contratos inteligentes Blockchain: Impresionante blog breve que explica la metodología de Pact FV con una pequeña introducción a la verificación formal según los primeros principios.
  - Blockchains Temoporales: un análisis formal
  - Validación de contratos inteligentes descentralizados mediante teoría de juegos y métodos formales
- Vídeos
  - Diseño formal, implementación y verificación de lenguajes BlockChain
  - CertiK: plataforma de verificación formal de contratos inteligentes (revisión)
  - Simplicidad: un nuevo lenguaje para blockchains
Desafíos para hacer que la IA sea segura
FLoC 2018: La Cumbre del Aprendizaje Automático se encuentra con los métodos formales
Aprendizaje automático verificado - Universidad Radboud de Nijmegen : curso universitario sobre el uso de métodos de verificación en aprendizaje automático.
Los métodos formales se encuentran con el aprendizaje automático - Universidad RWTH Aachen : seminario de 2018 sobre avances en el aprendizaje automático verificablemente seguro utilizando métodos formales.
- Lecturas
  - Hacia una inteligencia artificial verificada - S. Seshia
  - Hacia una IA robusta y verificada: pruebas de especificaciones, capacitación sólida y verificación formal - DeepMind
  - Desarrollo de sistemas de aprendizaje automático sin errores con matemáticas formales
  - Mezclando métodos formales, aprendizaje automático e interacción persona-computadora
  - Aprendizaje automático en métodos formales
  - Aprendizaje automático y métodos formales
  - Algoritmos para verificar redes neuronales profundas
  - Verificación de seguridad de redes neuronales profundas
  - El desafío de la verificación y prueba del aprendizaje automático - Ian GoodFellow y Nicolas Papernot
  - Verificación de propiedades de redes neuronales profundas binarizadas
  - Reluplex: un solucionador SMT eficiente para verificar redes neuronales profundas
  - Verificación de redes de avance lineal por partes
  - Desafíos en la verificación de algoritmos de aprendizaje por refuerzo
  - Aplicación de métodos formales en el aprendizaje por refuerzo - Galois Inc.
  - Hacia la demostración de la robustez adversa de las redes neuronales profundas
- Vídeos
  - Verificación de seguridad para redes neuronales profundas -ICST 2018
  - Verificación de seguridad para redes neuronales profundas - Marta Kwiatkowska - CAV 2017
  - Verificación de seguridad para redes neuronales profundas -INRIA
  - Reglas de verificación del aprendizaje automático, desde errores basados en datos hasta IA explicable
  - Verificación de programas de aprendizaje automático
  - Reluplex: un solucionador SMT eficiente para verificar redes neuronales profundas - Video de la conferencia
  - Desarrollo de modelos de aprendizaje automático sin errores utilizando Certigrad - Daniel Selsam
Cree sistemas ciberfísicos seguros
VeHICal : Proyecto centrado en desarrollar las bases del codiseño verificado de interfaces y control para sistemas ciberfísicos humanos.
fm4cps : métodos formales para sistemas físicos cibernéticos, esfuerzos conjuntos de INRIA y ECNU shanghai.
- Lecturas
  - Diseño de sistemas ciberfísicos: fundamentos formales, métodos y cadenas de herramientas integradas
  - Nuevas fronteras en los métodos formales: aprendizaje, sistemas ciberfísicos, educación y más
  - Verificación de modelos estadísticos para sistemas ciberfísicos
  - Verificación formal de sistemas ciberfísicos de transporte
  - Verificación de sistemas ciberfísicos
  - Verificación y validación en sistemas ciberfísicos: desafíos de investigación y un camino a seguir
  - Detección de anomalías en sistemas ciberfísicos: un enfoque de métodos formales
  - Verificación composicional de sistemas ciberfísicos autoadaptativos
- Vídeos
  - Una carta de métodos formales para sistemas ciberfísicos e Internet industrial de las cosas
  - Verificación formal de sistemas ciberfísicos
  - Monitoreo de sistemas ciberfísicos

Resumen Interpretación enfocada

Certificación de robustez rápida y eficaz: proyecto DeepZ - para certificar la robustez de redes neuronales basándose en una interpretación abstracta.
AI2: Certificación de seguridad y robustez de redes neuronales con interpretación abstracta
Impulsar la certificación de robustez de redes neuronales: utiliza la interpretación abstracta en su metodología.

Investigación del lenguaje de programación relacionada

Programación probabilística
- Lecturas
  - Una introducción a la programación probabilística
  - Verificación formal de programas probabilísticos de orden superior
  - Programación lógica probabilística y redes bayesianas
  - Funciones probabilísticas y oráculos criptográficos en lógica de orden superior - Andreas Lochbihler
  - Verificación relacional probabilística de implementaciones criptográficas
  - Las pruebas de acoplamiento son programas de productos probabilísticos.
  - Acoplamiento probabilístico avanzado para privacidad diferencial
  - Métodos formales de programación probabilística
  - Métodos formales para programas probabilísticos: diapositivas de conferencias.
  - Programación probabilística: verdadero desafío de verificación
  - FairSquare: Verificación probabilística de la equidad del programa
  - VPHL: una lógica de corrección parcial verificada para programas probabilísticos
  - Unificando lógica y probabilidad
- Vídeos
  - Verificación formal de programas probabilísticos de orden superior: vídeo de la conferencia POPL 2019
  - Programación lógica probabilística y sus aplicaciones - Luc De Raedt, Lovaina
Desarrollo del lenguaje de programación cuántica
- Lecturas
  - Qwire: Verificación formal de programas cuánticos en Coq
  - Una lógica para la verificación formal de programas cuánticos
  - Técnicas de acoplamiento para razonar sobre programas cuánticos
  - Verificación formal versus incertidumbre cuántica
  - Modelo de verificación de protocolos cuánticos recursivos
- Vídeos
  - Computación cuántica con capacidad de misión para verificación y validación de software (VV) - CMU
  - Dominique Unruh: Verificación formal de la criptografía cuántica
Refinamiento de idiomas utilizando métodos formales.

Esto trata particularmente de mejorar ciertas propiedades (como el paralelismo y la concurrencia) de los lenguajes de programación existentes. Se pueden buscar muchas cosas fácilmente con respecto a esto ya que, después de todo, esta es la única razón más importante para estudiar la teoría PL. Todas las conferencias enumeradas aquí ACM SIGPLAN tienen la mayoría de artículos de investigación sobre el desarrollo de lenguajes de programación. Échales un vistazo.