plt formal methods resources herunterladen - plt formal methods resources Quellcode herunterladen

plt formal methods resources

Anderer Quellcode

1.0.0

Herunterladen

Programmiersprachentheorie und formale Methoden – Ressourcen

Bild Courtsey: Forsyte-Gruppe

Formale Methoden sind mathematische Techniken, die zum Entwurf, zur Überprüfung und zur Spezifikation von Software- und Hardwareproblemen verwendet werden. Hierbei handelt es sich im Wesentlichen um einen Teilbereich der Forschung zur Programmiersprachentheorie , der zur Untersuchung komplexer Informatikprobleme eingesetzt wird.

Die Analyse mit formalen Methoden umfasst im Wesentlichen die folgenden Schritte:

Formal Specification
Formal Proofs
Model Checking
Abstraction

Die formale Beweisentwicklung und Modellprüfung erfolgt hauptsächlich mithilfe interaktiver Theorembeweiser, die oft als Beweisassistenten bezeichnet werden. Bei der Abstraktion handelt es sich um die Schaffung strukturell sinnvoller Beziehungen zwischen Teilen von Modellen.

Hier ist mein Versuch, eine Liste nützlicher Lesematerialien, Videos und Tools zusammenzustellen, begleitet von einigen bevorstehenden Herausforderungen auf diesem Gebiet.

NOTIZ :

Ich habe versucht, den Inhalt stärker auf aktuelle Forschung und industrielle Anwendung zu konzentrieren. Wer eine rein akademische Sammlung sucht, muss sich an „Formal Methods in Education – Jeremy Avigad“ wenden.
Vom Leser werden Grundkenntnisse der Typentheorie erwartet. Einen eher akademischen Einblick finden Sie hier learn-tt.

Inhalt

Bücher & Vorträge
Blogs
MOOCs
Werkzeuge
Projekte
Kommende Herausforderungen
- Sicherheitsbezogen
  - Softwaresicherheit
  - Differenzielle Privatsphäre
  - Anwendungen in der Blockchain-Sicherheit
  - Herausforderungen bei der Sicherstellung von KI
  - Erstellen Sie sichere cyberphysische Systeme
- Abstrakte Interpretation fokussiert
- Programmiersprachenforschung im Zusammenhang
  - Probabilistische Programmierung
  - Entwicklung der Quantenprogrammiersprache
  - Sprachverfeinerung mit formalen Methoden
Verwandte Branchen und Startups

Bücher & Vorträge

Software-Grundlagen : Ich empfehle dies dringend als Ausgangsmaterial, um tief in dieses Gebiet einzutauchen. Das Buch ist sehr hilfreich beim Aufbau grundlegender Konzepte und dient als sehr fundierte Einführung in das Fachgebiet. Überall werden wunderschön illustrierte Konzepte mit Beispielen zum Üben bereitgestellt, so dass das Lernen mit interaktiven Theoremen Spaß macht.
FRAP – Adam Chlipala : Ein Buch, das Ihnen hilft, die formale Korrektheit von Programmen zu verstehen und zu begründen. Beispiele für Datenstrukturen und Algorithmen, die von der Imperativsprache ( C ) inspiriert sind, helfen ungemein dabei, über deren formale Verifizierung nachzudenken.
Zertifizierte Programmierung mit abhängigen Typen – Adam Chlipala : Eines der besten theoretical books zum Erlernen des Beweisens von Theoremen mit coq.
Formale Verifikation – Jacques Fleuriot : Dies ist ein Kurs, der die Beweisführung von Theoremen mit einigen weiter entwickelten Werkzeugen wie SAT- und SMT-Lösern beinhaltet.
Abstrakte Interpretation – Patrick Cousot Das beste verfügbare Material zur Theorie der abstrakten Interpretation. Es bietet eine vollständige und rein mathematische Analyse von Programmmutationen. Das Programmverhalten als sich ständig verändernde Beziehung zwischen verschiedenen abstrakten mathematischen Strukturen wird erklärt und bewiesen!!
Logik und Beweis – Einführung in CMU und Lean : Dieser Kurs wurde an der CMU entwickelt und dient auch als Einführungsmaterial für den Theorembeweis in Lean

Wenn Sie der Meinung sind, dass Sie weitere theoretische Einblicke benötigen, lesen Sie bitte den obigen Hinweis.

Blogs

Erste Schritte mit formalen Methoden
K Framework und Bemühungen zur formalen Verifizierung in Blockchain
Formale Pact-Verifizierung für intelligente Blockchain-Verträge: Toller kurzer Blog, der die Methodik des Pact FV erklärt und eine kleine Einführung in die formale Verifizierung nach ersten Prinzipien gibt.
Auf dem Weg zu robuster und verifizierter KI: Spezifikationstests, robustes Training und formale Verifizierung – DeepMind
Die Herausforderung der Verifizierung und des Testens maschinellen Lernens – Ian GoodFellow und Nicolas Papernot

MOOCs

Formale Softwareüberprüfung – edX
Quantitative Modellprüfung – Coursera
Cyber Physical Systems : Kurs von UC Berkeley, der sich auf die Verwendung von Verifizierungsmethoden zur Modellierung von Cyper Physical Systems (CPS) konzentriert.
Programmiersprachen - Coursera

Werkzeuge

Beweisassistenten

coq: Der beliebteste und am weitesten verbreitete Theorembeweiser. Es unterstützt viele Funktionen, einschließlich ML-Extraktion und Projektpaketierung (Projekt- und Makefile-Erstellung). Es gibt zahlreiche how-to , die coq zur Formalisierung verwenden. Jeder könnte diese 100 Theoreme in Coq sehr interessant finden.
Lean: Ein ziemlich neuer Theorembeweis von Microsoft Research . Verfügt über ein schönes interaktives Tutorial, das den Einstieg erleichtert.
PRISM-Modellprüfer: Es handelt sich um einen Modellprüfer, der von der Universität Oxford entwickelt wurde.
Nuprl: Theorem Prover von Cornell im Rahmen des Proof Refinement Logic Project.
Agda: Eine ziemlich ausgereifte Proof-Assistentin. Hat ähnliche Funktionen wie Coq. leicht zu erlernen nach einiger Erfahrung in COQ.
Isabelle: Es ist ein alter Theorembeweis. Verfügt über eine gute Implementierung der Kernlogik, es fehlen jedoch andere UX-bezogene Funktionen.
VCC: Ein mechanischer Prüfer für gleichzeitige C-Programme von Microsoft.
TLA+: Hochsprache zur Modellierung von Sprachen und Systemen (insbesondere gleichzeitig und verteilt).

SAT/SMT/SMC-Löser

SAT-Löser:

MiniSat.

SMT-Löser:

Z3
CVC4
MatheSAT5
SMTInterpol
Prinzessin

SMC-Löser:

Veröffentlichung

Hybridlöser

Proof-Assistenten verfügen über sehr starke Implementierungen von Programmlogiken. Manchmal ist es taktisch möglicherweise nicht möglich, komplexe Beweise allein durch deren Verwendung durchzuführen. Daher kombiniert die aktuelle Forschung dieses Prinzip des starken logischen Denkens mit leistungsstarken SMT- und SMC-Lösern, um die Beweisentwicklung zu erleichtern. Einige Beispiele finden Sie hier unten:

Fstar(F*)
- Mit KremLin ist es möglich, F*-Code nach C zu extrahieren.
SMTCoq

Projekte

Die meisten Projekte sind mehr oder weniger eine Weiterentwicklung der jeweiligen Theorembeweiser oder SAT/SMT/SMC/Löser und können daher dort nachgeschlagen werden. Dies sind einige andere Projekte, die aktiv entwickelt werden.

DeepSpec ist ein Dachprojekt, das sich auf den Aufbau verifizierter Softwaresysteme konzentriert. Folgende große Teilprojekte werden aktiv bearbeitet:
- Compcert
- Verifiziertes LLVM (VeLLVM)
- Verifizierte Software ToolChain (VST)
ikos ist ein zuverlässiger , fehlerfreier C-Compiler, der auf der Theorie der abstrakten Interpretation basiert.
Projekt Everest: Es handelt sich um ein Forschungsprojekt, das darauf abzielt, ein sicheres und verifiziertes HTTPS-Ökosystem zu schaffen.
CertiCrypt: Es handelt sich um ein Projekt, das sich auf die Modellierung der Public-Key-Kryptographie mithilfe des COQ-Proof-Assistenten konzentriert.
Iris: Iris ist ein Concurrent Separation Logic Framework höherer Ordnung, das im Beweisassistenten Coq implementiert und verifiziert wird.
VeriDeep – Sicherheitsüberprüfung tiefer neuronaler Netze
VeHICal: Das Projekt konzentrierte sich auf die Entwicklung der Grundlagen für verifiziertes Co-Design von Schnittstellen und Steuerung für menschliche cyber-physische Systeme.
FastSMT – Tool zur Erweiterung Ihres SMT-Lösers, indem Sie lernen, seine Leistung für Ihren Formeldatensatz zu optimieren. Es wurde vom SRI-Labor der ETH Zürich entwickelt und basiert auf dem Z3 SMT-Löser.
fm4cps – Formale Methoden für Cyber Physical Systems, gemeinsame Bemühungen von INRIA und ECNU Shanghai.

Kommende Herausforderungen

Sicherheitsbezogen

Softwaresicherheit
- Lesungen
  - Formale Methoden für Sicherheit, NSF-Workshop
  - Symbolische Beziehung zwischen formalen Methoden und Sicherheit
  - Projekt-Everest-Forschungspapiere
  - Formale Methoden in der Softwaresicherheit
  - Formale Methoden für sichere Computersysteme
  - Die rechnerische Solidität der formalen Verschlüsselung
  - Sicherheitsstrukturen mit formalen Methoden
  - Überprüfung des kryptografischen Primitivs
  - Formelle Zertifizierung spielbasierter kryptografischer Beweise
  - Formelle Zertifizierung codebasierter kryptografischer Beweise
- Videos
  - Umfangreiche Spezifikation für Dropbox
  - DSL für verifizierte sichere Mehrparteienberechnungen in F*
  - Verwendung formaler Methoden zur Entwicklung hochsicherer Systeme
  - Sicherheit durch formale Methoden und sichere Architektur (CERIAS – Purdue University)
  - Sprachbasierte Techniken für Kryptographie und Datenschutz
Differenzielle Privatsphäre
- Lesungen
  - Formale Überprüfung der differenziellen Privatsphäre für interaktive Systeme
  - Formale Methoden für den Datenschutz
  - LightDP – Auf dem Weg zur Automatisierung differenzieller Datenschutznachweise
  - EasyCrypt – Verifizierter rechnergestützter differenzieller Datenschutz mit Anwendungen für Smart Meter
  - Beweis der differenziellen Privatsphäre in der Hoare-Logik
  - Differenziell private Bayes'sche Programmierung
  - Erweiterte probabilistische Kopplung für differenzielle Privatsphäre
- Videos
  - Formale Methoden und Nachweise von Privatsphäreneigenschaften - 1
  - Formale Methoden und Nachweise von Privatsphäreneigenschaften - 2
  - Formale Methoden und Nachweise von Privatsphäreneigenschaften - 3
  - Nachweis der differenziellen Privatsphäre mithilfe relationaler Typen
Anwendungen in der Blockchain-Sicherheit
Formale Methoden für Blockchains : Dies ist der erste Workshop, der sich auf die Verwendung formaler Methoden in der Blockchain-Technologie konzentriert. Es wird am 11. Oktober 2019 sein.
CertiK : Es ist ein Startup, das sich auf den Einsatz formaler Methoden konzentriert, um Blockchains nachweislich sicher zu machen.
- Lesungen
  - Wie formale Analyse und Verifizierung Blockchain-basierten Systemen Sicherheit verleihen – Tutorial @ MIT
  - Intelligente Verträge und Möglichkeiten für formale Methoden
  - K-Framework und Bemühungen zur formalen Verifizierung in Blockchain. Eine großartige Sammlung von erklärendem Material zum K-Framework und seiner Anwendung bei der Verifizierung von Blockchain-Systemen.
  - Formale Pact-Verifizierung für intelligente Blockchain-Verträge: Toller kurzer Blog, der die Methodik des Pact FV erklärt und eine kleine Einführung in die formale Verifizierung nach ersten Prinzipien gibt.
  - Temporale Blockchains – eine formale Analyse
  - Validierung dezentraler Smart Contracts durch Spieltheorie und formale Methoden
- Videos
  - Formaler Entwurf, Implementierung und Verifizierung von Blockchain-Sprachen
  - CertiK – Plattform zur formellen Verifizierung intelligenter Verträge (Rezension)
  - Einfachheit – Eine neue Sprache für Blockchains
Herausforderungen bei der Gewährleistung der KI-Sicherheit
FLoC 2018 – Summit of Machine Learning trifft auf formale Methoden
Verifiziertes maschinelles Lernen – Radboud-Universität Nijmegen : Universitätskurs zur Verwendung von Verifizierungsmethoden im maschinellen Lernen.
Formale Methoden treffen auf maschinelles Lernen – RWTH Aachen : Seminar 2018 über Fortschritte im nachweislich sicheren maschinellen Lernen mit formalen Methoden.
- Lesungen
  - Auf dem Weg zur verifizierten künstlichen Intelligenz – S. Seshia
  - Auf dem Weg zu robuster und verifizierter KI: Spezifikationstests, robustes Training und formale Verifizierung – DeepMind
  - Entwicklung fehlerfreier Systeme für maschinelles Lernen mit formaler Mathematik
  - Eine Mischung aus formalen Methoden, maschinellem Lernen und Mensch-Computer-Interaktion
  - Maschinelles Lernen in formalen Methoden
  - Maschinelles Lernen und formale Methoden
  - Algorithmen zur Überprüfung tiefer neuronaler Netze
  - Sicherheitsüberprüfung tiefer neuronaler Netze
  - Die Herausforderung der Verifizierung und des Testens maschinellen Lernens – Ian GoodFellow und Nicolas Papernot
  - Überprüfung der Eigenschaften binarisierter tiefer neuronaler Netze
  - Reluplex: Ein effizienter SMT-Löser zur Überprüfung tiefer neuronaler Netze
  - Überprüfung stückweise linearer Feed-Forward-Netzwerke
  - Herausforderungen bei der Verifizierung von Reinforcement-Learning-Algorithmen
  - Anwendung formaler Methoden beim Reinforcement Learning - Galois Inc.
  - Auf dem Weg zum Beweis der gegnerischen Robustheit tiefer neuronaler Netze
- Videos
  - Sicherheitsüberprüfung für tiefe neuronale Netze –ICST 2018
  - Sicherheitsüberprüfung für tiefe neuronale Netze – Marta Kwiatkowska – CAV 2017
  - Sicherheitsüberprüfung für tiefe neuronale Netze – INRIA
  - Regeln der maschinellen Lernverifizierung, von datengesteuerten Fehlern bis hin zu erklärbarer KI
  - Verifizierung von Programmen für maschinelles Lernen
  - Reluplex: Ein effizienter SMT-Löser zur Überprüfung tiefer neuronaler Netze – Konferenzvideo
  - Entwicklung fehlerfreier Modelle für maschinelles Lernen mit Certigrad – Daniel Selsam
Erstellen Sie sichere CyberPhysical Systems
VeHICal : Das Projekt konzentrierte sich auf die Entwicklung der Grundlagen für verifiziertes Co-Design von Schnittstellen und Steuerung für menschliche cyber-physische Systeme.
fm4cps – Formale Methoden für Cyber Physical Systems, gemeinsame Bemühungen von INRIA und ECNU Shanghai.
- Lesungen
  - Cyber-Physical Systems Design: Formale Grundlagen, Methoden und integrierte Werkzeugketten
  - Neue Grenzen formaler Methoden: Lernen, Cyber-Physische Systeme, Bildung und darüber hinaus
  - Statistische Modellprüfung für Cyber-Physical Systems
  - Formale Verifizierung von Cyber-Physical-Systemen im Transportwesen
  - Verifizierung von Cyber-Physical Systems
  - Verifizierung und Validierung in Cyber-Physical Systems: Forschungsherausforderungen und ein Weg nach vorne
  - Anomalieerkennung in cyber-physischen Systemen: Ein formaler Methodenansatz
  - Zusammensetzungsüberprüfung selbstadaptiver cyber-physikalischer Systeme
- Videos
  - Eine formale Methodencharta für cyber-physikalische Systeme und das industrielle Internet der Dinge
  - Formale Verifizierung von Cyber-Physical Systems
  - Überwachung Cyber-Physischer Systeme

Abstrakte Interpretation fokussiert

Schnelle und effektive Robustheitszertifizierung: Projekt DeepZ – zur Zertifizierung der Robustheit neuronaler Netzwerke basierend auf abstrakter Interpretation.
AI2: Sicherheits- und Robustheitszertifizierung neuronaler Netze mit abstrakter Interpretation
Steigerung der Robustheitszertifizierung neuronaler Netze: Verwendet abstrakte Interpretation in seiner Methodik.

Bezug zur Programmiersprachenforschung

Probabilistische Programmierung
- Lesungen
  - Eine Einführung in die probabilistische Programmierung
  - Formale Verifizierung probabilistischer Programme höherer Ordnung
  - Probabilistische Logikprogrammierung und Bayesianische Netzwerke
  - Wahrscheinlichkeitsfunktionen und kryptografische Orakel in der Logik höherer Ordnung – Andreas Lochbihler
  - Probabilistische relationale Verifizierung kryptografischer Implementierungen
  - Kopplungsbeweise sind probabilistische Produktprogramme
  - Erweiterte probabilistische Kopplung für differenzielle Privatsphäre
  - Formale Methoden für die probabilistische Programmierung
  - Formale Methoden für Wahrscheinlichkeitsprogramme: Vorlesungsfolien
  - Probabilistische Programmierung – echte Verifizierungsherausforderung
  - FairSquare: Probabilistische Überprüfung der Programmfairness
  - VPHL: Eine verifizierte Teilkorrektheitslogik für probabilistische Programme
  - Logik und Wahrscheinlichkeit vereinen
- Videos
  - Formale Verifizierung von Wahrscheinlichkeitsprogrammen höherer Ordnung – POPL 2019-Konferenzvideo
  - Probabilistische Logikprogrammierung und ihre Anwendungen – Luc De Raedt, Leuven
Entwicklung der Quantenprogrammiersprache
- Lesungen
  - Qwire: Formale Verifizierung von Quantenprogrammen in Coq
  - Eine Logik zur formalen Verifizierung von Quantenprogrammen
  - Kopplungstechniken zum Nachdenken über Quantenprogramme
  - Formale Verifizierung vs. Quantenunsicherheit
  - Modellprüfung rekursiver Quantenprotokolle
- Videos
  - Einsatzfähiges Quantencomputing zur Softwareverifizierung und -validierung (VV) – CMU
  - Dominique Unruh: Formale Verifizierung der Quantenkryptographie
Sprachverfeinerung mit formalen Methoden

Dabei geht es insbesondere um die Verbesserung bestimmter Eigenschaften (wie Parallelität und Parallelität) bestehender Programmiersprachen. Vieles lässt sich diesbezüglich leicht nachschlagen, da dies schließlich der einzig wichtigste Grund ist, sich mit der PL-Theorie zu beschäftigen. Alle hier aufgeführten Konferenzen von ACM SIGPLAN bieten die meisten Forschungsarbeiten zur Entwicklung von Programmiersprachen. Schauen Sie sich diese an.