Unduh plt formal methods resources - plt formal methods resources Unduh kode sumber

plt formal methods resources

Kode sumber lainnya

1.0.0

Unduh

Teori Bahasa Pemrograman & Metode Formal - Sumber

Gambar Courtsey : Grup Forsyte

Metode formal adalah teknik matematika yang digunakan untuk desain, verifikasi dan spesifikasi masalah perangkat lunak dan perangkat keras. Ini pada dasarnya adalah bagian dari penelitian Teori Bahasa Pemrograman yang digunakan untuk mempelajari masalah ilmu komputer yang kompleks.

Analisis dengan Metode Formal pada dasarnya melibatkan langkah-langkah berikut:

Formal Specification
Formal Proofs
Model Checking
Abstraction

Pengembangan pembuktian formal dan pengecekan model terutama dilakukan dengan menggunakan pembukti teorema interaktif yang sering disebut sebagai Asisten pembuktian. Abstraksi menciptakan hubungan yang baik secara struktural antar bagian model.

Berikut adalah upaya saya untuk menyusun daftar bahan bacaan, video, dan alat yang berguna disertai dengan beberapa tantangan yang akan datang di lapangan.

CATATAN :

Saya telah mencoba membuat konten lebih fokus pada penelitian terkini dan aplikasi industri. Orang yang mencari koleksi akademis murni harus mengacu pada Metode Formal dalam Pendidikan - Jeremy Avigad.
Pembaca diharapkan memiliki pengetahuan dasar tentang Teori Tipe . Wawasan yang lebih akademis dapat ditemukan di sini pelajari-tt.

Isi

Buku & Ceramah
Blog
MOOC
Peralatan
Proyek
Tantangan Mendatang
- Terkait Keamanan
  - Keamanan Perangkat Lunak
  - Privasi Diferensial
  - Aplikasi dalam Keamanan Rantai Blok
  - Tantangan dalam Membuat AI aman
  - Ciptakan Sistem CyberFisik yang Aman
- Interpretasi Abstrak terfokus
- Terkait penelitian Bahasa Pemrograman
  - Pemrograman Probabilistik
  - Pengembangan Bahasa Pemrograman Kuantum
  - Penyempurnaan Bahasa menggunakan metode formal
Industri & Startup Terkait

Buku & Ceramah

Landasan Perangkat Lunak : Saya sangat menyarankan ini sebagai bahan awal untuk mendalami bidang ini. Buku ini sangat membantu dalam membangun konsep-konsep dasar dan berfungsi sebagai pengenalan yang sangat baik terhadap bidang tersebut. Konsep-konsep yang diilustrasikan dengan indah dengan contoh-contoh untuk dipraktikkan disediakan sepanjang pembuatan teorema interaktif yang membuktikan pembelajaran menyenangkan.
FRAP - Adam Chlipala : Sebuah buku yang membantu Anda memahami dan memberi alasan kebenaran formal suatu program. Contoh struktur data dan algoritme yang terinspirasi dari bahasa Imperatif ( C ) sangat membantu untuk mulai memikirkan verifikasi formalnya.
Pemrograman Bersertifikat dengan Tipe Ketergantungan - Adam Chlipala : Salah satu theoretical books terbaik untuk mempelajari pembuktian teorema menggunakan coq.
Verifikasi Formal - Jacques Fleuriot : Ini kursus yang melibatkan pembuktian teorema menggunakan beberapa alat yang lebih maju seperti pemecah SAT dan SMT.
Interpretasi Abstrak - Patrick Cousot Materi terbaik yang tersedia tentang teori Interpretasi Abstrak. Ini memberikan analisis matematis yang lengkap dan murni tentang mutasi program. Perilaku Program sebagai hubungan yang terus-menerus memodifikasi antara struktur matematika abstrak yang berbeda dijelaskan dan dibuktikan!!.
Logika dan Pembuktian - Pengenalan CMU & Lean : Mata kuliah ini dirancang di CMU dan juga berfungsi sebagai bahan pengantar pembuktian teorema di Lean

Jika Anda merasa memerlukan lebih banyak wawasan teoritis, silakan lihat Catatan di atas.

Blog

Memulai dengan metode formal
Kerangka K & upaya verifikasi formal di Blockchain
Verifikasi Formal Pakta untuk kontrak pintar Blockchain : Blog pendek yang luar biasa menjelaskan metodologi Pakta FV dengan pengenalan kecil pada verifikasi formal berdasarkan prinsip pertama.
Menuju AI yang Kuat dan Terverifikasi: Pengujian Spesifikasi, Pelatihan yang Kuat, dan Verifikasi Formal - DeepMind
Tantangan verifikasi dan pengujian pembelajaran mesin - Ian GoodFellow & Nicolas Papernot

MOOC

Verifikasi Perangkat Lunak Formal - edX
Pemeriksaan Model Kuantitatif - Coursera
Sistem Fisik Cyber : Kursus oleh UC Berkeley, berfokus pada penggunaan metode verifikasi untuk pemodelan sistem Fisik Cyper (CPS).
Bahasa Pemrograman - Coursera

Peralatan

Asisten Bukti

coq: Pembukti teorema yang paling populer dan banyak digunakan. Ini mendukung banyak fitur termasuk ekstraksi ML, pengemasan Proyek (pembuatan Proyek dan Makefile). Ada banyak materi how-to yang tersedia yang menggunakan coq untuk formalisasi. Siapa pun mungkin menganggap 100 Teorema di Coq ini sangat menarik.
lean: Pepatah Teorema yang cukup baru oleh Microsoft Research . Memiliki tutorial interaktif yang bagus, mudah untuk memulai.
Pemeriksa model PRISM : Ini adalah pemeriksa model yang dikembangkan oleh Universitas Oxford.
Nuprl : Pembuktian Teorema oleh Cornell dalam Proyek Logika Penyempurnaan Bukti.
Agda : Asisten Pembuktian yang cukup Dewasa. Memiliki fitur yang mirip dengan Coq. mudah dipelajari setelah beberapa pengalaman di coq.
Isabelle: Itu adalah teorema lama Pepatah. Memiliki implementasi logika inti yang bagus tetapi tidak memiliki fitur terkait UX lainnya.
VCC : Pemverifikasi mekanis untuk program C bersamaan oleh Microsoft.
TLA+ : Bahasa Tingkat Tinggi untuk bahasa dan sistem pemodelan (terutama yang konkuren & terdistribusi).

Pemecah SAT/SMT/SMC

Pemecah SAT:

MiniSat.

Pemecah SMT:

Z3
CVC4
MatematikaSAT5
SMTInterpol
Putri

Pemecah SMC:

Publikasi

Pemecah Hibrid

Proof Assitant memiliki implementasi logika program yang sangat kuat. Terkadang secara taktis tidak mungkin melakukan pembuktian yang rumit hanya dengan menggunakan pembuktian tersebut. Oleh karena itu, penelitian saat ini menggabungkan prinsip penalaran berbasis logika yang kuat dengan pemecah SMT dan SMC yang kuat untuk memudahkan pengembangan bukti. Beberapa contohnya ada di bawah ini:

Bintang F(F*)
- Dimungkinkan untuk mengekstrak kode F* ke C menggunakan KreMLin.
SMTCoq

Proyek

Sebagian besar proyek kurang lebih merupakan pengembangan dari masing-masing pembukti teorema atau pemecah SAT/SMT/SMC/ dan karenanya dapat dilihat di sana. Ini adalah beberapa proyek lain yang dikembangkan secara aktif.

DeepSpec adalah proyek payung yang berfokus pada pembangunan sistem perangkat lunak terverifikasi. Sub-proyek utama berikut ini secara aktif dikerjakan:
- Kompensasi
- LLVM Terverifikasi (VeLLVM)
- ToolChain Perangkat Lunak Terverifikasi (VST)
ikos adalah kompiler C bebas bug yang andal berdasarkan teori interpretasi abstrak.
Proyek Everest: Ini adalah proyek penelitian yang bertujuan menciptakan ekosistem HTTPS yang aman dan terverifikasi.
CertiCrypt: Ini adalah proyek yang berfokus pada pemodelan kriptografi kunci publik menggunakan asisten bukti coq.
Iris: Iris adalah Kerangka Logika Pemisahan Serentak Tingkat Tinggi yang diimplementasikan dan diverifikasi dalam asisten pembuktian Coq.
VeriDeep - Verifikasi Keamanan Jaringan Neural Dalam
VeHICal : Proyek yang berfokus pada pengembangan fondasi desain bersama antarmuka dan kontrol yang terverifikasi untuk sistem cyber-fisik manusia.
FastSMT - Alat untuk meningkatkan pemecah SMT Anda dengan belajar mengoptimalkan kinerjanya untuk kumpulan data rumus Anda. Ini dikembangkan oleh lab SRI, ETH Zurich yang dibangun di atas pemecah Z3 SMT.
fm4cps - Metode formal untuk Sistem Fisik Cyber, upaya bersama oleh INRIA dan ECNU shanghai.

Tantangan Mendatang

Terkait Keamanan

Keamanan Perangkat Lunak
- Bacaan
  - Metode Formal untuk Keamanan, lokakarya NSF
  - Hubungan Simbolis antara Metode Formal dan Keamanan
  - Makalah Penelitian Proyek-Everest
  - Metode Formal dalam Keamanan Perangkat Lunak
  - Metode Formal untuk Sistem Komputer yang Aman dan Terjamin
  - Kesehatan Komputasi Enkripsi Formal
  - Struktur Keamanan menggunakan Metode Formal
  - Verifikasi Primitif Kriptografi
  - Sertifikasi Formal bukti Kriptografi berbasis Game
  - Sertifikasi formal bukti kriptografi berbasis kode
- Video
  - Spesifikasi Mendalam untuk Dropbox
  - DSL untuk Komputasi Multipartai Aman Terverifikasi di F*
  - Menggunakan Metode Formal untuk pengembangan Sistem yang Sangat Aman
  - Keamanan melalui Metode FOrmal dan Arsitektur Aman (CERIAS - Universitas Purdue)
  - Teknik berbasis bahasa untuk Kriptografi dan Privasi
Privasi Diferensial
- Bacaan
  - Verifikasi Formal Privasi Diferensial untuk Sistem Interaktif
  - Metode Formal untuk Privasi
  - LightDP - Menuju otomatisasi Bukti Privasi Diferensial
  - EasyCrypt - Privasi Diferensial Komputasi Terverifikasi dengan Aplikasi pada Smart Meter
  - Membuktikan Privasi Diferensial dalam Logika Hoare
  - Pemrograman Bayesian Privat Diferensial
  - Kopling Probabilistik Tingkat Lanjut untuk Privasi Diferensial
- Video
  - Metode Formal dan bukti sifat privasi - 1
  - Metode Formal dan bukti sifat privasi - 2
  - Metode Formal dan bukti sifat privasi - 3
  - Membuktikan privasi Diferensial menggunakan Tipe Relasional
Aplikasi dalam Keamanan Rantai Blok
Metode Formal untuk Block Chains : Ini adalah lokakarya pertama yang berfokus pada penggunaan metode formal dalam teknologi Block Chain. Itu akan terjadi pada 11 Oktober 2019 .
CertiK : Ini adalah startup yang berfokus pada penggunaan metode formal untuk membuat blockchain aman secara verifikasi.
- Bacaan
  - Bagaimana Analisis dan Verifikasi Formal Menambah Keamanan pada Sistem Berbasis Blockchain - Tutorial @ MIT
  - Kontrak cerdas dan peluang untuk metode formal
  - Kerangka K & upaya verifikasi formal di Blockchain Kumpulan materi penjelasan yang luar biasa tentang kerangka K dan penerapannya dalam memverifikasi sistem Blockchain.
  - Verifikasi Formal Pakta untuk kontrak pintar Blockchain : Blog pendek yang luar biasa menjelaskan metodologi Pakta FV dengan pengenalan kecil pada verifikasi formal berdasarkan prinsip pertama.
  - Blockchain Tempoporal - analisis formal
  - Validasi Kontrak Cerdas Terdesentralisasi melalui Teori Permainan dan Metode Formal
- Video
  - Desain Formal, Implementasi dan Verifikasi Bahasa BlockChain
  - CertiK - Platform verifikasi formal kontrak pintar (ulasan)
  - Kesederhanaan - Bahasa baru untuk blockchain
Tantangan dalam membuat AI aman
FLoC 2018- Summit of Machine Learning memenuhi metode formal
Pembelajaran Mesin Terverifikasi - Radboud University Nijmegen : Kursus universitas tentang penggunaan metode verifikasi dalam Pembelajaran Mesin.
Metode Formal bertemu Pembelajaran Mesin - RWTH Aachen University : seminar tahun 2018 tentang kemajuan Pembelajaran Mesin yang Sangat Aman dan Terverifikasi menggunakan metode formal.
- Bacaan
  - Menuju Kecerdasan Buatan Terverifikasi - S. Seshia
  - Menuju AI yang Kuat dan Terverifikasi: Pengujian Spesifikasi, Pelatihan yang Kuat, dan Verifikasi Formal - DeepMind
  - Mengembangkan Sistem Pembelajaran Mesin BugFree dengan Matematika Formal
  - Menggabungkan metode Formal, Pembelajaran Mesin & Interaksi Manusia dengan Komputer
  - Pembelajaran Mesin dalam Metode Formal
  - Pembelajaran Mesin dan Metode Formal
  - Algoritma untuk Memverifikasi Jaringan Neural Dalam
  - Verifikasi Keamanan Jaringan Neural Dalam
  - Tantangan verifikasi dan pengujian pembelajaran mesin - Ian GoodFellow & Nicolas Papernot
  - Memverifikasi Properti Jaringan Neural Dalam Binarisasi
  - Reluplex: Pemecah SMT yang Efisien untuk Memverifikasi Jaringan Neural Dalam
  - Verifikasi Jaringan Maju Umpan Linier Sepotong-sepotong
  - Tantangan dalam Verifikasi Algoritma Reinforcement Learning
  - Menerapkan Metode Formal dalam Pembelajaran Penguatan - Galois Inc.
  - Menuju Membuktikan Kekokohan Permusuhan Jaringan Syaraf Dalam
- Video
  - Verifikasi Keamanan untuk Jaringan Neural Dalam -ICST 2018
  - Verifikasi Keamanan untuk Jaringan Neural Dalam - Marta Kwiatkowska - CAV 2017
  - Verifikasi Keamanan untuk Jaringan Neural Dalam -INRIA
  - Aturan Verifikasi Pembelajaran Mesin, mulai dari bug berbasis data hingga AI yang dapat dijelaskan
  - Verifikasi Program Pembelajaran Mesin
  - Reluplex: Pemecah SMT yang Efisien untuk Memverifikasi Jaringan Neural Dalam - Video Konferensi
  - Mengembangkan model Machine Learning Bebas Bug menggunakan Certigrad - Daniel Selsam
Ciptakan Sistem CyberPhysical yang aman
VeHICal : Proyek yang berfokus pada pengembangan fondasi desain bersama antarmuka dan kontrol yang terverifikasi untuk sistem cyber-fisik manusia.
fm4cps - Metode formal untuk Sistem Fisik Cyber, upaya bersama oleh INRIA dan ECNU shanghai.
- Bacaan
  - Desain Sistem Cyber-Fisik: Fondasi Formal, Metode, dan Rantai Alat Terintegrasi
  - Perbatasan Baru dalam Metode Formal: Pembelajaran, Sistem Siber-Fisik, Pendidikan, dan Lainnya
  - Pemeriksaan Model Statistik untuk Sistem Cyber-Fisik
  - Verifikasi Formal Sistem Fisik Siber Transportasi
  - Verifikasi Sistem Cyber-Fisik
  - Verifikasi dan Validasi dalam Sistem Cyber-Fisik: Tantangan Penelitian dan Jalan ke Depan
  - Deteksi Anomali dalam Sistem Cyber-Fisik: Pendekatan Metode Formal
  - Verifikasi Komposisi Sistem Cyber-Fisik Adaptif Mandiri
- Video
  - Piagam Metode Formal untuk Sistem Cyber-Fisik dan Internet of Things Industri
  - Verifikasi Formal Sistem Cyber Fisik
  - Memantau Sistem Fisik Cyber

Interpretasi Abstrak terfokus

Sertifikasi Kekokohan yang Cepat dan Efektif : proyek DeepZ - untuk mensertifikasi ketahanan jaringan saraf berdasarkan interpretasi abstrak.
AI2 : Sertifikasi Keamanan dan Kekokohan Jaringan Syaraf Tiruan dengan Interpretasi Abstrak
Meningkatkan Kekokohan Sertifikasi Jaringan Neural : Menggunakan Interpretasi Abstrak dalam metodologinya.

Terkait Penelitian Bahasa Pemrograman

Pemrograman Probabilistik
- Bacaan
  - Pengantar Pemrograman Probabilistik
  - Verifikasi Formal program Probabilistik Tingkat Tinggi
  - Pemrograman Logika Probabilistik dan Jaringan Bayesian
  - Fungsi probabilistik dan Oracle Kriptografi dalam Logika Tingkat Tinggi - Andreas Lochbihler
  - Verifikasi Relasional Probabilistik dari implementasi Kriptografi
  - Bukti Kopling adalah program produk Probabilistik
  - Kopling Probabilistik Tingkat Lanjut untuk Privasi Diferensial
  - Metode Formal untuk Pemrograman probabilistik
  - Metode formal untuk program probabilistik : Slide kuliah
  - Pemrograman Probabilistik - Tantangan Verifikasi Sejati
  - FairSquare : Verifikasi Probabilistik Kewajaran Program
  - VPHL: Logika Koreksi Parsial yang Terverifikasi untuk Program Probabilistik
  - Menyatukan Logika dan Probabilitas
- Video
  - Verifikasi Formal Program Probabilistik Tingkat Tinggi - video konferensi POPL 2019
  - Pemrograman logika probabilistik dan aplikasinya - Luc De Raedt, Leuven
Pengembangan Bahasa Pemrograman Kuantum
- Bacaan
  - Qwire : Verifikasi Formal Program Kuantum di Coq
  - Logika untuk Verifikasi Formal Program Kuantum
  - Teknik Kopling untuk Penalaran tentang Program Kuantum
  - Verifikasi Formal vs Ketidakpastian Kuantum
  - Model Memeriksa Protokol Kuantum Rekursif
- Video
  - Komputasi Kuantum yang mampu menjalankan misi untuk Verifikasi dan Validasi Perangkat Lunak (VV) - CMU
  - Dominique Unruh: Verifikasi Formal Kriptografi Kuantum
Penyempurnaan Bahasa menggunakan metode formal

Hal ini khususnya berkaitan dengan peningkatan properti tertentu (seperti Paralelisme & Konkurensi) dari bahasa pemrograman yang ada. Banyak hal yang dapat dengan mudah dicari sehubungan dengan hal ini karena bagaimanapun juga ini adalah satu-satunya alasan terpenting untuk mempelajari teori PL. Semua konferensi yang terdaftar di sini ACM SIGPLAN memiliki sebagian besar makalah penelitian tentang pengembangan bahasa pemrograman, silakan periksa.