plt formal methods resources

ทฤษฎีภาษาการเขียนโปรแกรมและวิธีการอย่างเป็นทางการ - แหล่งข้อมูล

Image Courtsey : กลุ่ม Forsyte

วิธีการอย่างเป็นทางการเป็นเทคนิคทางคณิตศาสตร์ที่ใช้ในการออกแบบ การตรวจสอบ และข้อกำหนดเฉพาะของปัญหาซอฟต์แวร์และฮาร์ดแวร์ สิ่งเหล่านี้เป็นส่วนย่อยของ การวิจัยทฤษฎีภาษาการเขียนโปรแกรม ที่ใช้ศึกษาปัญหาวิทยาการคอมพิวเตอร์ที่ซับซ้อน

การวิเคราะห์โดยวิธีทางการโดยทั่วไปเกี่ยวข้องกับขั้นตอนเหล่านี้:

1. Formal Specification
2. Formal Proofs
3. Model Checking
4. Abstraction

การพัฒนาการพิสูจน์อย่างเป็นทางการและการตรวจสอบแบบจำลองจะดำเนินการโดยใช้ผู้พิสูจน์ทฤษฎีบทเชิงโต้ตอบซึ่งมักเรียกว่าผู้ช่วยการพิสูจน์ นามธรรมคือการสร้างความสัมพันธ์ที่ดีเชิงโครงสร้างระหว่างส่วนต่างๆ ของแบบจำลอง

นี่คือความพยายามของฉันในการรวบรวมรายการสื่อการอ่าน วิดีโอ และเครื่องมือที่เป็นประโยชน์ ควบคู่ไปกับความท้าทายที่จะเกิดขึ้นในภาคสนาม

บันทึก :

1. ฉันพยายามทำให้เนื้อหาเน้นไปที่การวิจัยในปัจจุบันและการประยุกต์ใช้ในอุตสาหกรรมมากขึ้น ผู้ที่กำลังมองหาคอลเลคชันทางวิชาการล้วนๆ ต้องอ้างอิงวิธีการอย่างเป็นทางการในการศึกษา - Jeremy Avigad

2. ผู้อ่านคาดว่าจะมีความรู้พื้นฐานเกี่ยวกับ ทฤษฎีประเภท อยู่บ้าง สามารถดูข้อมูลเชิงลึกทางวิชาการเพิ่มเติมได้ที่นี่ Learn-tt

สารบัญ

• หนังสือและการบรรยาย
• บล็อก
• MOOC
• เครื่องมือ
• โครงการ
• ความท้าทายที่จะเกิดขึ้น
  • ความปลอดภัยที่เกี่ยวข้อง
    • ความปลอดภัยของซอฟต์แวร์
    • ความเป็นส่วนตัวที่แตกต่างกัน
    • แอปพลิเคชันใน Block Chain Security
    • ความท้าทายในการทำให้ AI ปลอดภัย
    • สร้างระบบ CyberPhysical ที่ปลอดภัย
  • เน้นการตีความเชิงนามธรรม
  • การวิจัยภาษาการเขียนโปรแกรมที่เกี่ยวข้อง
    • การเขียนโปรแกรมความน่าจะเป็น
    • การพัฒนาภาษาโปรแกรมควอนตัม
    • การปรับแต่งภาษาโดยใช้วิธีการอย่างเป็นทางการ
• อุตสาหกรรมและสตาร์ทอัพที่เกี่ยวข้อง

หนังสือและการบรรยาย

• รากฐานซอฟต์แวร์ : ฉันขอแนะนำอย่างยิ่งให้สิ่งนี้เป็นเนื้อหาเริ่มต้นสำหรับการดำน้ำลึกในสาขานี้ หนังสือเล่มนี้มีประโยชน์มากในการสร้างแนวคิดพื้นฐานและเป็นการแนะนำที่ดีในสาขานี้ แนวคิดที่มีภาพประกอบสวยงามพร้อมตัวอย่างให้ฝึกฝนตลอดทั้งการสร้างทฤษฎีบทแบบโต้ตอบพิสูจน์ความสนุกสนานในการเรียนรู้

• FRAP - Adam Chlipala : หนังสือที่ช่วยให้คุณเข้าใจและให้เหตุผลถึงความถูกต้องของโปรแกรมอย่างเป็นทางการ ตัวอย่างโครงสร้างข้อมูลและอัลกอริธึมที่ได้รับแรงบันดาลใจจากภาษาที่จำเป็น ( C ) ช่วยได้อย่างมากในการเริ่มคิดถึงการตรวจสอบอย่างเป็นทางการ

• การเขียนโปรแกรมที่ผ่านการรับรองพร้อมประเภทการพึ่งพา - Adam Chlipala : หนึ่งใน theoretical books ที่ดีที่สุดในการเรียนรู้ทฤษฎีบทการพิสูจน์โดยใช้ coq

• การตรวจสอบอย่างเป็นทางการ - Jacques Fleuriot : หลักสูตรนี้เกี่ยวข้องกับการพิสูจน์ทฤษฎีบทโดยใช้เครื่องมือที่ได้รับการพัฒนาเพิ่มเติม เช่น ตัวแก้ปัญหา SAT และ SMT

• การตีความบทคัดย่อ - Patrick Cousot เนื้อหาที่ดีที่สุดที่มีอยู่ในทฤษฎีการตีความบทคัดย่อ ให้การวิเคราะห์ทางคณิตศาสตร์ที่สมบูรณ์และบริสุทธิ์ของการกลายพันธุ์ของโปรแกรม พฤติกรรมของโปรแกรมซึ่งเป็นการปรับเปลี่ยนความสัมพันธ์อย่างต่อเนื่องระหว่างโครงสร้างทางคณิตศาสตร์เชิงนามธรรมต่างๆ ได้รับการอธิบายและพิสูจน์แล้ว!!

• ตรรกะและการพิสูจน์ - การแนะนำ CMU และแบบลีน : หลักสูตรนี้ออกแบบที่ CMU และยังทำหน้าที่เป็นสื่อเบื้องต้นสำหรับการพิสูจน์ทฤษฎีบทแบบลีน

หากคุณรู้สึกว่าต้องการข้อมูลเชิงลึกทางทฤษฎีเพิ่มเติม โปรดดูหมายเหตุด้านบน

บล็อก

• เริ่มต้นด้วยวิธีที่เป็นทางการ
• K Framework และความพยายามในการตรวจสอบอย่างเป็นทางการใน Blockchain
• การตรวจสอบ Pact อย่างเป็นทางการสำหรับสัญญาอัจฉริยะของ Blockchain : บล็อกสั้น ๆ ที่ยอดเยี่ยมที่อธิบายวิธีการ ของ Pact FV พร้อมการแนะนำเล็กน้อยเกี่ยวกับการตรวจสอบอย่างเป็นทางการตามหลักการแรก
• สู่ AI ที่แข็งแกร่งและตรวจสอบได้: การทดสอบข้อมูลจำเพาะ การฝึกอบรมที่แข็งแกร่ง และการตรวจสอบอย่างเป็นทางการ - DeepMind
• ความท้าทายในการตรวจสอบและทดสอบการเรียนรู้ของเครื่อง - Ian GoodFellow และ Nicolas Papernot

MOOC

• การตรวจสอบซอฟต์แวร์อย่างเป็นทางการ - edX
• การตรวจสอบแบบจำลองเชิงปริมาณ - Coursera
• Cyber ​​Physical Systems : หลักสูตรโดย UC Berkeley มุ่งเน้นไปที่การใช้วิธีการตรวจสอบสำหรับการสร้างแบบจำลอง Cyper Physical Systems (CPS)
• ภาษาโปรแกรม - Coursera

เครื่องมือ

ผู้ช่วยพิสูจน์

• coq: เครื่องพิสูจน์ทฤษฎีบทที่ได้รับความนิยมและใช้กันอย่างแพร่หลาย รองรับฟีเจอร์มากมายรวมถึงการแยก ML, การทำแพ็กเกจโปรเจ็กต์ (การสร้างโปรเจ็กต์และ Makefile) มีสื่อ how-to มากมายที่ใช้ coq ในการทำให้เป็นทางการ ใครๆ ก็อาจพบว่าทฤษฎีบท 100 ข้อใน Coq น่าสนใจมาก

• ยัน: Theorem Prover ที่ค่อนข้างใหม่โดย Microsoft Research มีบทช่วยสอนแบบโต้ตอบที่ดี เริ่มต้นได้ง่าย

• เครื่องตรวจสอบแบบจำลอง PRISM : เป็นเครื่องตรวจสอบแบบจำลองที่พัฒนาโดย University of Oxford

• Nuprl : เครื่องพิสูจน์ทฤษฎีบท โดย Cornell ภายใต้โครงการ Proof Refinement Logic

• Agda: ผู้ช่วยพิสูจน์อักษรที่ค่อนข้างเป็นผู้ใหญ่ มีคุณสมบัติคล้ายกับ Coq เรียนรู้ได้ง่ายหลังจากมีประสบการณ์ใน coq มาบ้างแล้ว

• อิสซาเบล: มันเป็นทฤษฎีบทอันเก่าแก่ มีการใช้งานคอร์ลอจิกที่ดีแต่ขาดคุณสมบัติอื่นๆ ที่เกี่ยวข้องกับ UX

• VCC : เครื่องมือตรวจสอบเชิงกลสำหรับโปรแกรม C ที่ทำงานพร้อมกันโดย Microsoft

• TLA+ : ภาษาระดับสูงสำหรับการสร้างแบบจำลองภาษาและระบบ (โดยเฉพาะที่เกิดขึ้นพร้อมกันและกระจาย)

ตัวแก้ปัญหา SAT/SMT/SMC

นักแก้ปัญหา SAT:

• มินิแซท.

ตัวทำละลาย SMT:

• Z3

• ซีวีซี4

• คณิตSAT5

• อินเตอร์โพล

• เจ้าหญิง

ผู้ให้บริการ SMC:

• สิ่งตีพิมพ์

ไฮบริดโซเวอร์

Proof Assitants มีการใช้งานลอจิกโปรแกรมที่แข็งแกร่งมาก บางครั้งอาจเป็นไปไม่ได้ในเชิงกลยุทธ์ที่จะดำเนินการพิสูจน์ที่ซับซ้อนโดยใช้เพียงสิ่งเหล่านั้นเท่านั้น ดังนั้น การวิจัยในปัจจุบันจึงรวมหลักการของการให้เหตุผลตามตรรกะที่แข็งแกร่งนี้เข้ากับตัวแก้ปัญหา SMT และ SMC ที่ทรงพลัง เพื่อความสะดวกในการพัฒนาการพิสูจน์ ตัวอย่างบางส่วนอยู่ที่นี่ด้านล่าง:

• ฟสตาร์(F*)

  • เป็นไปได้ที่จะแยกรหัส F* เป็น C โดยใช้ KreMLin

• SMTCoq

โครงการ

โครงการส่วนใหญ่มีการพัฒนาผู้พิสูจน์ทฤษฎีบทหรือตัวแก้ SAT/SMT/SMC/ ตามลำดับไม่มากก็น้อย ดังนั้นจึงสามารถค้นหาได้จากที่นั่น เหล่านี้คือโครงการอื่นๆ บางส่วนที่ได้รับการพัฒนาอย่างแข็งขัน

• DeepSpec เป็นโครงการหลักที่มุ่งเน้นการสร้างระบบซอฟต์แวร์ที่ได้รับการตรวจสอบแล้ว โครงการย่อยที่สำคัญต่อไปนี้มีการดำเนินการอย่างแข็งขันเมื่อ:

  • คอมพิวเตอร์
  • LLVM ที่ตรวจสอบแล้ว (VeLLVM)
  • ToolChain ซอฟต์แวร์ที่ได้รับการตรวจสอบแล้ว (VST)

• ikos เป็นคอมไพเลอร์ C ที่ปราศจากจุดบกพร่อง ที่เชื่อถือได้ โดยอิงตามทฤษฎีการตีความเชิงนามธรรม

• โครงการ Everest: เป็นโครงการวิจัยที่มีจุดมุ่งหมายเพื่อสร้างระบบนิเวศ HTTPS ที่ปลอดภัยและตรวจสอบได้

• CertiCrypt: เป็นโปรเจ็กต์ที่มุ่งเน้นการสร้างแบบจำลองการเข้ารหัสคีย์สาธารณะโดยใช้ตัวช่วยพิสูจน์ coq

• ไอริส: ไอริสเป็นเฟรมเวิร์กลอจิกการแยกพร้อมกันที่มีลำดับสูงกว่าที่นำไปใช้และตรวจสอบในผู้ช่วยพิสูจน์ Coq

• VeriDeep - การตรวจสอบความปลอดภัยของเครือข่าย Deep Neural

• VeHICal : โครงการมุ่งเน้นไปที่การพัฒนารากฐานของการออกแบบร่วมอินเทอร์เฟซและการควบคุมสำหรับระบบไซเบอร์กายภาพของมนุษย์ที่ได้รับการตรวจสอบแล้ว

• FastSMT - เครื่องมือเพื่อเพิ่มประสิทธิภาพของตัวแก้ปัญหา SMT โดยการเรียนรู้เพื่อเพิ่มประสิทธิภาพให้กับชุดข้อมูลสูตรของคุณ ได้รับการพัฒนาโดยห้องปฏิบัติการ SRI โดยมี ETH Zurich สร้างขึ้นบนตัวแก้ปัญหา Z3 SMT

• fm4cps - วิธีการอย่างเป็นทางการสำหรับระบบกายภาพไซเบอร์ ความพยายามร่วมกันโดย INRIA และ ECNU เซี่ยงไฮ้

ความท้าทายที่จะเกิดขึ้น

ความปลอดภัยที่เกี่ยวข้อง

• ความปลอดภัยของซอฟต์แวร์

  • การอ่าน
    • วิธีการอย่างเป็นทางการสำหรับการรักษาความปลอดภัย การประชุมเชิงปฏิบัติการ NSF
    • ความสัมพันธ์เชิงสัญลักษณ์ระหว่างวิธีการอย่างเป็นทางการและความปลอดภัย
    • เอกสารวิจัยโครงการ-Everest
    • วิธีการอย่างเป็นทางการในการรักษาความปลอดภัยของซอฟต์แวร์
    • วิธีการอย่างเป็นทางการสำหรับระบบคอมพิวเตอร์ที่ปลอดภัย
    • ความสมบูรณ์ทางการคำนวณของการเข้ารหัสอย่างเป็นทางการ
    • โครงสร้างการรักษาความปลอดภัยโดยใช้วิธีการอย่างเป็นทางการ
    • การตรวจสอบ Cryptographic Primitive
    • การรับรองอย่างเป็นทางการของการพิสูจน์การเข้ารหัสตามเกม
    • การรับรองอย่างเป็นทางการของการพิสูจน์การเข้ารหัสตามรหัส
  • วิดีโอ
    • ข้อมูลจำเพาะเชิงลึกสำหรับ Dropbox
    • DSL สำหรับการคำนวณหลายฝ่ายที่ปลอดภัยและได้รับการยืนยันใน F*
    • การใช้วิธีการอย่างเป็นทางการเพื่อการพัฒนาระบบที่มีความปลอดภัยสูง
    • การรักษาความปลอดภัยด้วยวิธีการรูปแบบและสถาปัตยกรรมที่ปลอดภัย (CERIAS - Purdue University)
    • เทคนิคที่ใช้ภาษาสำหรับการเข้ารหัสและความเป็นส่วนตัว

• ความเป็นส่วนตัวที่แตกต่างกัน

  • การอ่าน
    • การตรวจสอบความเป็นส่วนตัวที่แตกต่างกันอย่างเป็นทางการสำหรับระบบโต้ตอบ
    • วิธีการอย่างเป็นทางการเพื่อความเป็นส่วนตัว
    • LightDP - สู่การพิสูจน์ความเป็นส่วนตัวที่แตกต่างกันโดยอัตโนมัติ
    • EasyCrypt - ตรวจสอบความเป็นส่วนตัวส่วนต่างทางการคำนวณด้วยแอปพลิเคชันไปยัง Smart Meter
    • การพิสูจน์ความเป็นส่วนตัวที่แตกต่างใน Hoare Logic
    • การเขียนโปรแกรมแบบเบย์ส่วนตัวที่แตกต่างกัน
    • การมีเพศสัมพันธ์ที่น่าจะเป็นขั้นสูงเพื่อความเป็นส่วนตัวที่แตกต่างกัน
  • วิดีโอ
    • วิธีการอย่างเป็นทางการและการพิสูจน์คุณสมบัติความเป็นส่วนตัว - 1
    • วิธีการอย่างเป็นทางการและการพิสูจน์คุณสมบัติความเป็นส่วนตัว - 2
    • วิธีการอย่างเป็นทางการและการพิสูจน์คุณสมบัติความเป็นส่วนตัว - 3
    • การพิสูจน์ความเป็นส่วนตัวที่แตกต่างโดยใช้ประเภทเชิงสัมพันธ์

• แอปพลิเคชันใน Block Chain Security

  วิธีการอย่างเป็นทางการสำหรับบล็อกเชน : นี่เป็นเวิร์คช็อปครั้งแรกที่เน้นการใช้วิธีการที่เป็นทางการในเทคโนโลยีบล็อกเชน จะเป็นวันที่ 11 ตุลาคม 2562

  CertiK : เป็นสตาร์ทอัพที่เน้นการใช้วิธีการที่เป็นทางการเพื่อทำให้บล็อกเชนมีความปลอดภัยในการตรวจสอบยืนยัน

  • การอ่าน
    • การวิเคราะห์และการตรวจสอบอย่างเป็นทางการเพิ่มความปลอดภัยให้กับระบบที่ใช้บล็อคเชนอย่างไร - บทช่วยสอน @ MIT
    • สัญญาอันชาญฉลาดและโอกาสสำหรับวิธีการที่เป็นทางการ
    • K Framework และความพยายามในการตรวจสอบอย่างเป็นทางการใน Blockchain คอลเลกชันที่ยอดเยี่ยมของเนื้อหาอธิบายเกี่ยวกับ K framework และการประยุกต์ใช้ในการตรวจสอบระบบ Blockchain
    • การตรวจสอบ Pact อย่างเป็นทางการสำหรับสัญญาอัจฉริยะของ Blockchain : บล็อกสั้น ๆ ที่ยอดเยี่ยมที่อธิบายวิธีการ ของ Pact FV พร้อมการแนะนำเล็กน้อยเกี่ยวกับการตรวจสอบอย่างเป็นทางการตามหลักการแรก
    • Tempoporal Blockchains - การวิเคราะห์อย่างเป็นทางการ
    • การตรวจสอบความถูกต้องของสัญญาอัจฉริยะแบบกระจายอำนาจผ่านทฤษฎีเกมและวิธีการอย่างเป็นทางการ
  • วิดีโอ
    • การออกแบบ การนำไปใช้ และการตรวจสอบภาษา BlockChain อย่างเป็นทางการ
    • CertiK - แพลตฟอร์มการตรวจสอบสัญญาอัจฉริยะอย่างเป็นทางการ (รีวิว)
    • ความเรียบง่าย - ภาษาใหม่สำหรับบล็อกเชน

• ความท้าทายในการทำให้ AI ปลอดภัย

  FLoC 2018- การประชุมสุดยอด Machine Learning เป็นไปตามวิธีการที่เป็นทางการ

  Verified Machine Learning - Radboud University Nijmegen : หลักสูตรมหาวิทยาลัยเกี่ยวกับการใช้วิธีการยืนยันใน Machine Learning

  วิธีการอย่างเป็นทางการพบกับการเรียนรู้ของเครื่อง - RWTH Aachen University : การสัมมนาในปี 2018 เกี่ยวกับความก้าวหน้าในการเรียนรู้ของเครื่องที่ปลอดภัยที่ตรวจสอบได้โดยใช้วิธีการอย่างเป็นทางการ

  • การอ่าน

    • สู่ปัญญาประดิษฐ์ที่ได้รับการตรวจสอบแล้ว - S. Seshia
    • สู่ AI ที่แข็งแกร่งและตรวจสอบได้: การทดสอบข้อมูลจำเพาะ การฝึกอบรมที่แข็งแกร่ง และการตรวจสอบอย่างเป็นทางการ - DeepMind
    • การพัฒนาระบบการเรียนรู้ของเครื่อง BugFree ด้วยคณิตศาสตร์อย่างเป็นทางการ
    • การผสมผสานวิธีการอย่างเป็นทางการ การเรียนรู้ของเครื่อง และปฏิสัมพันธ์ระหว่างมนุษย์กับคอมพิวเตอร์
    • การเรียนรู้ของเครื่องในรูปแบบที่เป็นทางการ
    • การเรียนรู้ของเครื่องและวิธีการอย่างเป็นทางการ
    • อัลกอริธึมสำหรับการตรวจสอบเครือข่าย Deep Neural
    • การตรวจสอบความปลอดภัยของโครงข่าย Deep Neural
    • ความท้าทายในการตรวจสอบและทดสอบการเรียนรู้ของเครื่อง - Ian GoodFellow และ Nicolas Papernot
    • การตรวจสอบคุณสมบัติของโครงข่ายประสาทเทียมเชิงลึกแบบไบนารี
    • Reluplex: ตัวแก้ปัญหา SMT ที่มีประสิทธิภาพสำหรับการตรวจสอบเครือข่าย Deep Neural
    • การตรวจสอบเครือข่ายการส่งต่อฟีดเชิงเส้นแบบแยกส่วน
    • ความท้าทายในการตรวจสอบอัลกอริธึมการเรียนรู้แบบเสริมกำลัง
    • การประยุกต์วิธีการอย่างเป็นทางการในการเรียนรู้แบบเสริมกำลัง - Galois Inc.
    • สู่การพิสูจน์ความแข็งแกร่งของฝ่ายตรงข้ามของโครงข่ายประสาทเทียมระดับลึก

  • วิดีโอ

    • การตรวจสอบความปลอดภัยสำหรับ Deep Neural Networks -ICST 2018
    • การตรวจสอบความปลอดภัยสำหรับโครงข่าย Deep Neural - Marta Kwiatkowska - CAV 2017
    • การตรวจสอบความปลอดภัยสำหรับเครือข่าย Deep Neural -INRIA
    • กฎการตรวจสอบการเรียนรู้ของเครื่อง ตั้งแต่ข้อบกพร่องที่ขับเคลื่อนด้วยข้อมูลไปจนถึง AI ที่อธิบายได้
    • การตรวจสอบโปรแกรมการเรียนรู้ของเครื่อง
    • Reluplex: ตัวแก้ปัญหา SMT ที่มีประสิทธิภาพสำหรับการตรวจสอบเครือข่าย Deep Neural - วิดีโอการประชุม
    • การพัฒนาโมเดล Machine Learning ที่ปราศจากข้อผิดพลาดโดยใช้ Certigrad - Daniel Selsam

• สร้างระบบ CyberPhysical ที่ปลอดภัย

  VeHICal : โครงการมุ่งเน้นไปที่การพัฒนารากฐานของการออกแบบร่วมอินเทอร์เฟซและการควบคุมสำหรับระบบไซเบอร์กายภาพของมนุษย์ที่ได้รับการตรวจสอบแล้ว

  fm4cps - วิธีการอย่างเป็นทางการสำหรับระบบกายภาพไซเบอร์ ความพยายามร่วมกันโดย INRIA และ ECNU เซี่ยงไฮ้

  • การอ่าน
    • การออกแบบระบบไซเบอร์-กายภาพ: พื้นฐานอย่างเป็นทางการ วิธีการ และโซ่เครื่องมือแบบผสมผสาน
    • ขอบเขตใหม่ในวิธีการอย่างเป็นทางการ: การเรียนรู้ ระบบไซเบอร์กายภาพ การศึกษา และอื่นๆ
    • การตรวจสอบแบบจำลองทางสถิติสำหรับระบบไซเบอร์กายภาพ
    • การตรวจสอบอย่างเป็นทางการของระบบทางกายภาพทางไซเบอร์ในการขนส่ง
    • การตรวจสอบระบบไซเบอร์-กายภาพ
    • การตรวจสอบและการตรวจสอบความถูกต้องในระบบทางกายภาพทางไซเบอร์: ความท้าทายด้านการวิจัยและหนทางข้างหน้า
    • การตรวจจับความผิดปกติในระบบไซเบอร์-กายภาพ: แนวทางวิธีการอย่างเป็นทางการ
    • การตรวจสอบองค์ประกอบของระบบไซเบอร์กายภาพแบบปรับตัวได้เอง
  • วิดีโอ
    • กฎบัตรวิธีการอย่างเป็นทางการสำหรับระบบไซเบอร์กายภาพและอินเทอร์เน็ตในทุกสิ่งทางอุตสาหกรรม
    • การตรวจสอบอย่างเป็นทางการของระบบทางกายภาพทางไซเบอร์
    • การตรวจสอบระบบทางกายภาพทางไซเบอร์

เน้นการตีความเชิงนามธรรม

• การรับรองความทนทานที่รวดเร็วและมีประสิทธิภาพ : โครงการ DeepZ - สำหรับการรับรองความทนทานของโครงข่ายประสาทเทียมตามการตีความเชิงนามธรรม
• AI2 : การรับรองความปลอดภัยและความคงทนของโครงข่ายประสาทเทียมพร้อมการตีความเชิงนามธรรม
• ส่งเสริมการรับรองความทนทานของโครงข่ายประสาทเทียม : ใช้การตีความเชิงนามธรรมในวิธีการ

การวิจัยภาษาการเขียนโปรแกรมที่เกี่ยวข้อง

• การเขียนโปรแกรมความน่าจะเป็น

  • การอ่าน
    • ความรู้เบื้องต้นเกี่ยวกับการเขียนโปรแกรมความน่าจะเป็น
    • การตรวจสอบอย่างเป็นทางการของโปรแกรมความน่าจะเป็นลำดับที่สูงกว่า
    • การเขียนโปรแกรมลอจิกความน่าจะเป็นและเครือข่ายแบบเบย์
    • ฟังก์ชันความน่าจะเป็นและออราเคิลการเข้ารหัสในลอจิกลำดับที่สูงกว่า - Andreas Lochbihler
    • การตรวจสอบความสัมพันธ์ที่น่าจะเป็นของการใช้งานการเข้ารหัส
    • การพิสูจน์การมีเพศสัมพันธ์คือโปรแกรมผลิตภัณฑ์ความน่าจะเป็น
    • การมีเพศสัมพันธ์ที่น่าจะเป็นขั้นสูงเพื่อความเป็นส่วนตัวที่แตกต่างกัน
    • วิธีการอย่างเป็นทางการสำหรับการเขียนโปรแกรมความน่าจะเป็น
    • วิธีการอย่างเป็นทางการสำหรับโปรแกรมความน่าจะเป็น : สไลด์บรรยาย
    • การเขียนโปรแกรมความน่าจะเป็น - ความท้าทายในการตรวจสอบความถูกต้อง
    • FairSquare : การตรวจสอบความน่าจะเป็นของความเป็นธรรมของโปรแกรม
    • VPHL: ลอจิกความถูกต้องบางส่วนที่ได้รับการตรวจสอบแล้วสำหรับโปรแกรมความน่าจะเป็น
    • การรวมลอจิกและความน่าจะเป็น
  • วิดีโอ
    • การตรวจสอบอย่างเป็นทางการของโปรแกรมความน่าจะเป็นลำดับที่สูงกว่า - วิดีโอการประชุม POPL 2019
    • การเขียนโปรแกรมลอจิกความน่าจะเป็นและการประยุกต์ - ลุค เดอ เรดต์, เลอเวน

• การพัฒนาภาษาโปรแกรมควอนตัม

  • การอ่าน
    • Qwire : การตรวจสอบอย่างเป็นทางการของโปรแกรมควอนตัมใน Coq
    • ตรรกะสำหรับการตรวจสอบอย่างเป็นทางการของโปรแกรมควอนตัม
    • เทคนิคการเชื่อมต่อเพื่อการให้เหตุผลเกี่ยวกับโปรแกรมควอนตัม
    • การตรวจสอบอย่างเป็นทางการเทียบกับความไม่แน่นอนของควอนตัม
    • การตรวจสอบแบบจำลองโปรโตคอลควอนตัมแบบเรียกซ้ำ
  • วิดีโอ
    • คอมพิวเตอร์ควอนตัมที่มีความสามารถในภารกิจสำหรับการตรวจสอบและยืนยันซอฟต์แวร์ (VV) - มช
    • Dominique Unruh: การตรวจสอบอย่างเป็นทางการของการเข้ารหัสควอนตัม

• การปรับแต่งภาษาโดยใช้วิธีการอย่างเป็นทางการ

โดยเฉพาะอย่างยิ่งเกี่ยวข้องกับการปรับปรุงคุณสมบัติบางอย่าง (เช่น Parallelism & Concurrency) ของภาษาโปรแกรมที่มีอยู่ สามารถค้นหาสิ่งต่างๆ มากมายเกี่ยวกับเรื่องนี้ได้อย่างง่ายดาย เนื่องจากท้ายที่สุดแล้ว นี่คือเหตุผลที่สำคัญที่สุดเพียงอย่างเดียวในการศึกษาทฤษฎี PL การประชุมทั้งหมดที่ระบุไว้ในที่นี้ ACM SIGPLAN มีงานวิจัยส่วนใหญ่เกี่ยวกับการพัฒนาภาษาการเขียนโปรแกรม ลองเข้าไปดูสิ

อุตสาหกรรมและสตาร์ทอัพที่เกี่ยวข้อง

• เซอร์ติเค
• กาลัวส์ อิงค์
• จิตใจสังเคราะห์
• ห้องทดลองเร่ร่อน
• เทซอส
• เจนสตรีท
• ซิสเทเรล
• ทวีก
• เวอร์ริโฟลว์

ใบอนุญาต

ข้อเสนอแนะใด ๆ ยินดีต้อนรับ โปรดพิจารณาส่งคำขอดึงหากคุณรู้สึกว่า !!