الصفحة الرئيسية>المتعلقة بالبرمجة>شفرة المصدر الأخرى
تنزيل

نظرية لغة البرمجة والأساليب الرسمية - الموارد

الصورة مجاملة: مجموعة فورسايت

الأساليب الرسمية هي تقنيات رياضية تستخدم للتصميم والتحقق ومواصفات مشاكل البرامج والأجهزة. هذه في الأساس مجموعة فرعية من أبحاث نظرية لغة البرمجة التي يتم استخدامها لدراسة مشاكل علوم الكمبيوتر المعقدة.

يتضمن التحليل بالطرق الرسمية بشكل أساسي الخطوات التالية:

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

يتم تطوير البرهان الرسمي وفحص النموذج في المقام الأول باستخدام مثبتات النظرية التفاعلية التي يطلق عليها غالبًا اسم مساعدي الإثبات. التجريد هو خلق علاقات سليمة من الناحية الهيكلية بين أجزاء النماذج.

إليكم محاولتي لتنظيم قائمة بمواد القراءة ومقاطع الفيديو والأدوات المفيدة مصحوبة ببعض التحديات القادمة في هذا المجال.

ملحوظة :

  1. لقد حاولت أن أجعل المحتوى أكثر تركيزًا على البحث الحالي والتطبيق الصناعي. يجب على الأشخاص الذين يبحثون عن مجموعة أكاديمية بحتة الرجوع إلى الأساليب الرسمية في التعليم - جيريمي أفيجاد.

  2. من المتوقع أن يكون لدى القارئ بعض المعرفة الأساسية بنظرية النوع . يمكن العثور على رؤية أكاديمية أكثر هنا learn-tt.

محتويات

  • الكتب والمحاضرات
  • مدونات
  • MOOCs
  • أدوات
  • المشاريع
  • التحديات القادمة
    • المتعلقة بالأمن
      • أمن البرمجيات
      • الخصوصية التفاضلية
      • تطبيقات في أمن سلسلة الكتل
      • التحديات في جعل الذكاء الاصطناعي آمنًا
      • إنشاء أنظمة سيبرانية فيزيائية آمنة
    • يركز التفسير الملخص
    • أبحاث لغة البرمجة ذات الصلة
      • البرمجة الاحتمالية
      • تطوير لغة البرمجة الكمومية
      • صقل اللغة باستخدام الأساليب الرسمية
  • الصناعات ذات الصلة والشركات الناشئة

الكتب والمحاضرات

  • أسس البرمجيات : أنصح بشدة بهذا باعتباره مادة أولية للتعمق في هذا المجال. الكتاب مفيد جدًا في بناء المفاهيم الأساسية ويعد بمثابة مقدمة سليمة جدًا لهذا المجال. يتم توفير المفاهيم الموضحة بشكل جميل مع أمثلة للممارسة في جميع أنحاء مما يجعل النظرية التفاعلية تثبت متعة التعلم.

  • FRAP - Adam Chlipala : كتاب يساعدك على فهم وفهم الصحة الشكلية للبرامج. تساعد الأمثلة المستوحاة من لغة الأمر ( C ) لهياكل البيانات والخوارزميات بشكل كبير على البدء في التفكير في التحقق الرسمي منها.

  • البرمجة المعتمدة مع الأنواع التابعة - Adam Chlipala : أحد أفضل theoretical books لتعلم إثبات النظرية باستخدام coq.

  • التحقق الرسمي - جاك فليريوت : هذه دورة تتضمن إثبات النظرية باستخدام بعض الأدوات الأكثر تطورًا مثل أدوات حل SAT وSMT.

  • التفسير المجرد - باتريك كوزوت أفضل المواد المتوفرة حول نظرية التفسير المجرد. أنه يعطي تحليل رياضي كامل ونقي لطفرات البرنامج. تم شرح وإثبات سلوك البرنامج كعلاقة تعديل مستمر بين مختلف الهياكل الرياضية المجردة!!.

  • المنطق والإثبات - CMU ومقدمة Lean : تم تصميم هذه الدورة في CMU وهي أيضًا بمثابة مادة تمهيدية لإثبات النظرية في Lean

إذا كنت تشعر أنك بحاجة إلى مزيد من الأفكار النظرية، يرجى الرجوع إلى الملاحظة أعلاه.

مدونات

  • البدء بالطرق الرسمية
  • إطار K وجهود التحقق الرسمي في Blockchain
  • التحقق الرسمي من Pact للعقود الذكية Blockchain: مدونة قصيرة رائعة تشرح منهجية Pact FV مع مقدمة صغيرة للتحقق الرسمي من خلال المبادئ الأولى.
  • نحو ذكاء اصطناعي قوي ومتحقق منه: اختبار المواصفات، والتدريب القوي، والتحقق الرسمي - DeepMind
  • التحدي المتمثل في التحقق من التعلم الآلي واختباره - إيان جودفيلو ونيكولاس بابيرنوت

MOOCs

  • التحقق الرسمي من البرنامج - edX
  • التحقق من النماذج الكمية - كورسيرا
  • الأنظمة الفيزيائية السيبرانية : دورة تقدمها جامعة كاليفورنيا في بيركلي، تركز على استخدام طرق التحقق لنمذجة الأنظمة الفيزيائية السيبرانية (CPS).
  • لغات البرمجة - كورسيرا

أدوات

مساعدو الإثبات

  • coq: مُبرهن النظرية الأكثر شيوعًا والأكثر استخدامًا. وهو يدعم الكثير من الميزات بما في ذلك استخراج ML وتغليف المشروع (إنشاء المشروع وMakefile). هناك الكثير من المواد how-to المتاحة التي تستخدم coq ​​لإضفاء الطابع الرسمي. قد يجد أي شخص هذه النظريات الـ 100 المثيرة للاهتمام في Coq.

  • العجاف: إثبات نظرية جديد إلى حد ما من قبل أبحاث مايكروسوفت . يحتوي على برنامج تعليمي تفاعلي لطيف، ومن السهل البدء به.

  • مدقق نموذج PRISM: هو مدقق نموذج تم تطويره بواسطة جامعة أكسفورد.

  • Nuprl: مُبرهن النظرية من كورنيل ضمن مشروع منطق تحسين الإثبات.

  • أغدا: مساعد إثبات ناضج جدًا. لديه ميزات مشابهة لـ Coq. من السهل التعلم بعد بعض الخبرة في coq.

  • إيزابيل: إنها نظرية قديمة. يتمتع بتطبيق جيد للمنطق الأساسي ولكنه يفتقر إلى الميزات الأخرى المتعلقة بتجربة المستخدم.

  • VCC: أداة التحقق الميكانيكية لبرامج C المتزامنة بواسطة Microsoft.

  • TLA+: لغة عالية المستوى للغات وأنظمة النمذجة (خاصة المتزامنة والموزعة).

حلول SAT/SMT/SMC

حلول SAT :

  • ميني سات.

حلول SMT:

  • Z3

  • CVC4

  • ماث سات5

  • SMTالإنتربول

  • أميرة

حلول SMC:

  • النشر

حلول الهجين

يمتلك مساعدو الإثبات تطبيقات قوية جدًا لمنطق البرنامج. في بعض الأحيان قد لا يكون من الممكن من الناحية التكتيكية تنفيذ البراهين المعقدة باستخدامها فقط. لذلك يجمع البحث الحالي بين مبدأ الاستدلال المنطقي القوي مع أدوات حل SMT وSMC القوية لتسهيل تطوير الدليل. بعض الأمثلة هنا أدناه:

  • فستار(F*)

    • من الممكن استخراج كود F* إلى C باستخدام KreMLin.

  • SMTCoq

المشاريع

معظم المشاريع عبارة عن تطوير إلى حد ما لمثبتات النظرية المعنية أو أدوات حل SAT/SMT/SMC/ وبالتالي يمكن البحث عنها هناك. هذه بعض المشاريع الأخرى التي تم تطويرها بنشاط.

  • DeepSpec هو مشروع شامل يركز على بناء أنظمة برمجية تم التحقق منها. يتم العمل بنشاط على المشاريع الفرعية الرئيسية التالية:

    • كومبيرت
    • تم التحقق من LLVM (VeLLVM)
    • سلسلة أدوات البرامج التي تم التحقق منها (VST)

  • ikos هو مترجم C موثوق به وخالي من الأخطاء ويعتمد على نظرية التفسير المجرد.

  • مشروع إيفرست: هو مشروع بحثي يهدف إلى إنشاء نظام HTTPS آمن وموثق.

  • CertiCrypt: هو مشروع يركز على نمذجة تشفير المفتاح العام باستخدام مساعد إثبات الجودة.

  • Iris: Iris عبارة عن إطار منطقي للفصل المتزامن عالي الترتيب تم تنفيذه والتحقق منه في مساعد الإثبات Coq.

  • VeriDeep - التحقق من سلامة الشبكات العصبية العميقة

  • VeHICal : يركز المشروع على تطوير أسس التصميم المشترك الذي تم التحقق منه للواجهات والتحكم في الأنظمة المادية السيبرانية البشرية.

  • FastSMT - أداة لزيادة حل SMT الخاص بك عن طريق تعلم تحسين أدائه لمجموعة البيانات الخاصة بك من الصيغ. تم تطويره بواسطة مختبر SRI، ETH Zurich، وهو مبني على Z3 SMT Solver.

  • fm4cps - الأساليب الرسمية للأنظمة الفيزيائية السيبرانية، الجهود المشتركة من قبل INRIA وECNU شنغهاي.

التحديات القادمة

المتعلقة بالأمن

  • أمن البرمجيات

    • قراءات
      • الأساليب الرسمية للأمن، ورشة عمل NSF
      • العلاقة الرمزية بين الأساليب الرسمية والأمن
      • أوراق بحثية لمشروع إيفرست
      • الأساليب الرسمية في أمن البرمجيات
      • الطرق الرسمية لأنظمة الكمبيوتر الآمنة والمأمونة
      • السلامة الحسابية للتشفير الرسمي
      • الهياكل الأمنية باستخدام الأساليب الرسمية
      • التحقق من التشفير البدائي
      • شهادة رسمية لإثباتات التشفير المستندة إلى اللعبة
      • شهادة رسمية لإثباتات التشفير المبنية على الكود
    • فيديوهات
      • مواصفات عميقة لدروببوإكس
      • DSL للحسابات الآمنة متعددة الأطراف التي تم التحقق منها في F*
      • استخدام الأساليب الرسمية لتطوير الأنظمة عالية الأمان
      • الأمن من خلال الأساليب الرسمية والبنية الآمنة (CERIAS - جامعة بوردو)
      • التقنيات القائمة على اللغة للتشفير والخصوصية

  • الخصوصية التفاضلية

    • قراءات
      • التحقق الرسمي من الخصوصية التفاضلية للأنظمة التفاعلية
      • الطرق الرسمية للخصوصية
      • LightDP - نحو أتمتة إثباتات الخصوصية التفاضلية
      • EasyCrypt - الخصوصية الحسابية التفاضلية التي تم التحقق منها مع تطبيقات العداد الذكي
      • إثبات الخصوصية التفاضلية في منطق هور
      • البرمجة البايزية الخاصة التفاضلية
      • الاقتران الاحتمالي المتقدم للخصوصية التفاضلية
    • فيديوهات
      • الطرق الرسمية وإثباتات خصائص الخصوصية - 1
      • الطرق الرسمية وإثباتات خصائص الخصوصية - 2
      • الطرق الرسمية وإثباتات خصائص الخصوصية - 3
      • إثبات الخصوصية التفاضلية باستخدام الأنواع العلائقية

  • تطبيقات في أمن سلسلة الكتل

    الطرق الرسمية لسلاسل الكتل : هذه هي أول ورشة عمل على الإطلاق تركز على استخدام الأساليب الرسمية في تكنولوجيا سلسلة الكتل. سيكون يوم 11 أكتوبر 2019 .

    CertiK : هي شركة ناشئة تركز على استخدام الأساليب الرسمية لجعل سلاسل الكتل آمنة بشكل يمكن التحقق منه.

    • قراءات
      • كيف يضيف التحليل الرسمي والتحقق الأمان إلى الأنظمة القائمة على Blockchain - البرنامج التعليمي في معهد ماساتشوستس للتكنولوجيا
      • العقود الذكية وفرص الأساليب الرسمية
      • إطار K وجهود التحقق الرسمي في Blockchain مجموعة رائعة من المواد التوضيحية حول إطار K وتطبيقه في التحقق من أنظمة Blockchain.
      • التحقق الرسمي من Pact للعقود الذكية Blockchain: مدونة قصيرة رائعة تشرح منهجية Pact FV مع مقدمة صغيرة للتحقق الرسمي من خلال المبادئ الأولى.
      • Blockchains الزمانية - تحليل رسمي
      • التحقق من صحة العقود الذكية اللامركزية من خلال نظرية اللعبة والأساليب الرسمية
    • فيديوهات
      • التصميم الرسمي والتنفيذ والتحقق من لغات BlockChain
      • CertiK - منصة التحقق الرسمية للعقود الذكية (مراجعة)
      • البساطة - لغة جديدة لسلاسل الكتل

  • التحديات في جعل الذكاء الاصطناعي آمنًا

    FLoC 2018- قمة التعلم الآلي تلبي الأساليب الرسمية

    التعلم الآلي المعتمد - جامعة رادبود نيميغن : دورة جامعية حول استخدام طرق التحقق في التعلم الآلي.

    تجتمع الأساليب الرسمية مع التعلم الآلي - جامعة RWTH Aachen : ندوة 2018 حول التطورات في التعلم الآلي الآمن الذي يمكن التحقق منه باستخدام الأساليب الرسمية.

    • قراءات

      • نحو ذكاء اصطناعي تم التحقق منه - س. سيشيا
      • نحو ذكاء اصطناعي قوي ومتحقق منه: اختبار المواصفات، والتدريب القوي، والتحقق الرسمي - DeepMind
      • تطوير أنظمة التعلم الآلي الخالية من الأخطاء باستخدام الرياضيات الرسمية
      • المزج بين الأساليب الرسمية والتعلم الآلي والتفاعل بين الإنسان والحاسوب
      • التعلم الآلي بالطرق الرسمية
      • التعلم الآلي والأساليب الرسمية
      • خوارزميات للتحقق من الشبكات العصبية العميقة
      • التحقق من سلامة الشبكات العصبية العميقة
      • التحدي المتمثل في التحقق من التعلم الآلي واختباره - إيان جودفيلو ونيكولاس بابيرنوت
      • التحقق من خصائص الشبكات العصبية العميقة الثنائية
      • Reluplex: حل SMT فعال للتحقق من الشبكات العصبية العميقة
      • التحقق من شبكات التغذية الخطية غير المنتظمة
      • التحديات في التحقق من خوارزميات التعلم المعزز
      • تطبيق الأساليب الرسمية في التعلم المعزز - Galois Inc.
      • نحو إثبات المتانة العدائية للشبكات العصبية العميقة

    • فيديوهات

      • التحقق من السلامة للشبكات العصبية العميقة -ICST 2018
      • التحقق من سلامة الشبكات العصبية العميقة - مارتا كوياتكوسكا - CAV 2017
      • التحقق من السلامة للشبكات العصبية العميقة -INRIA
      • قواعد التحقق من التعلم الآلي، بدءًا من الأخطاء المستندة إلى البيانات وحتى الذكاء الاصطناعي القابل للتفسير
      • التحقق من برامج التعلم الآلي
      • Reluplex: حل SMT فعال للتحقق من الشبكات العصبية العميقة - فيديو المؤتمر
      • تطوير نماذج التعلم الآلي الخالية من الأخطاء باستخدام Certigrad - دانيال سلسام

  • إنشاء أنظمة فيزيائية إلكترونية آمنة

    VeHICal : يركز المشروع على تطوير أسس التصميم المشترك الذي تم التحقق منه للواجهات والتحكم في الأنظمة المادية السيبرانية البشرية.

    fm4cps - الأساليب الرسمية للأنظمة الفيزيائية السيبرانية، الجهود المشتركة من قبل INRIA وECNU شنغهاي.

    • قراءات
      • تصميم الأنظمة الفيزيائية السيبرانية: الأسس الرسمية والأساليب وسلاسل الأدوات المتكاملة
      • حدود جديدة في الأساليب الرسمية: التعلم، والأنظمة الفيزيائية السيبرانية، والتعليم، وما بعده
      • فحص النماذج الإحصائية للأنظمة الفيزيائية السيبرانية
      • التحقق الرسمي من أنظمة النقل الفيزيائية السيبرانية
      • التحقق من الأنظمة الفيزيائية السيبرانية
      • التحقق والتحقق من الصحة في الأنظمة الفيزيائية السيبرانية: تحديات البحث والطريق إلى الأمام
      • اكتشاف الشذوذ في الأنظمة الفيزيائية السيبرانية: نهج الأساليب الرسمية
      • التحقق التركيبي للأنظمة الفيزيائية السيبرانية ذاتية التكيف
    • فيديوهات
      • ميثاق الأساليب الرسمي للأنظمة الفيزيائية السيبرانية وإنترنت الأشياء الصناعي
      • التحقق الرسمي من الأنظمة الفيزيائية السيبرانية
      • مراقبة الأنظمة الفيزيائية السيبرانية

يركز التفسير الملخص

  • شهادة المتانة السريعة والفعالة: مشروع DeepZ - للتصديق على قوة الشبكة العصبية بناءً على التفسير المجرد.
  • AI2: شهادة السلامة والمتانة للشبكات العصبية مع تفسير مجرد
  • تعزيز شهادة متانة الشبكات العصبية: يستخدم التفسير المجرد في منهجيته.

أبحاث لغة البرمجة ذات الصلة

  • البرمجة الاحتمالية

    • قراءات
      • مقدمة في البرمجة الاحتمالية
      • التحقق الرسمي من البرامج الاحتمالية ذات الترتيب العالي
      • البرمجة المنطقية الاحتمالية والشبكات الافتراضية
      • الدوال الاحتمالية وأوراكل التشفير في المنطق الأعلى - أندرياس لوشبيهلر
      • التحقق العلائقي الاحتمالي لتطبيقات التشفير
      • تعتبر إثباتات الاقتران بمثابة برامج منتجات احتمالية
      • الاقتران الاحتمالي المتقدم للخصوصية التفاضلية
      • الطرق الرسمية للبرمجة الاحتمالية
      • الطرق الرسمية للبرامج الاحتمالية: شرائح المحاضرة
      • البرمجة الاحتمالية - تحدي التحقق الحقيقي
      • FairSquare: التحقق الاحتمالي من عدالة البرنامج
      • VPHL: منطق الصحة الجزئية المعتمد للبرامج الاحتمالية
      • توحيد المنطق والاحتمال
    • فيديوهات
      • التحقق الرسمي من البرامج الاحتمالية ذات الترتيب العالي - فيديو مؤتمر POPL 2019
      • البرمجة المنطقية الاحتمالية وتطبيقاتها - لوك دي رايدت، لوفين

  • تطوير لغة البرمجة الكمومية

    • قراءات
      • Qwire: التحقق الرسمي من البرامج الكمومية في Coq
      • منطق للتحقق الرسمي من البرامج الكمومية
      • تقنيات الاقتران للاستدلال حول البرامج الكمومية
      • التحقق الرسمي مقابل عدم اليقين الكمي
      • نموذج التحقق من بروتوكولات الكم العودية
    • فيديوهات
      • الحوسبة الكمومية القادرة على تنفيذ المهام للتحقق من البرامج والتحقق من صحتها (VV) - CMU
      • دومينيك أونروه: التحقق الرسمي من التشفير الكمي

  • صقل اللغات باستخدام الأساليب الرسمية

يتعامل هذا بشكل خاص مع تحسين خصائص معينة (مثل التوازي والتزامن) للغات البرمجة الحالية. يمكن البحث بسهولة عن الكثير فيما يتعلق بهذا لأنه بعد كل هذا هو السبب الوحيد الأكثر أهمية لدراسة نظرية PL. تحتوي جميع المؤتمرات المدرجة هنا ACM SIGPLAN على غالبية الأوراق البحثية حول تطوير لغة البرمجة، قم بمراجعتها.

الصناعات ذات الصلة والشركات الناشئة

  • سيرتيك
  • شركة جالوا
  • العقول الاصطناعية
  • مختبرات البدو
  • تيزوس
  • جين ستريت
  • سيستريل
  • تويج
  • فيريفلوو

رخصة

أي اقتراحات هي موضع ترحيب. يرجى النظر في تقديم طلب سحب إذا كنت ترغب في ذلك !!

يوسع
معلومات إضافية
تطبيقات ذات صلة
نوصي لك
أخبار ذات صلة الكل