practical fm
1.0.0
إذا رأيت شركة على القائمة غير موجودة بعد الآن ، أو لم تعد تستخدم طرقًا رسمية ، فيرجى إرسال طلب سحب مع شرح. ينطبق الشيء نفسه إذا كنت تعمل حاليًا في شركة تستخدم أساليب رسمية أو تعرفها ولكنها ليست مدرجة في القائمة. يرجى تضمين موقع الويب ، github (إن أمكن) ، المواقع ، والقطاع. إذا كانت الشركة توظيف ، فيرجى تضمين رابط للإعلان.
| اسم | موقع | قطاع | مصدر |
|---|---|---|---|
| أمازون | الولايات المتحدة الأمريكية | التجارة الإلكترونية ، الحوسبة السحابية | TLA+ كيف تستخدم Amazon Web Services أساليب رسمية ، واستخدام الأساليب الرسمية في Amazon Web Services ، و CBMC Description Code Code من مراكز بيانات AWS ، Dafny AWS Encryption SDK |
| إيرباص | فرنسا | Astrée : "في عام 2003 ، أثبت Astrée عدم وجود أي أخطاء في وقت التشغيل في برنامج التحكم في الطيران الأساسي لنموذج Airbus. تم تحليل سطر النظام 132،000 من رمز C بالكامل بالكامل في 80 دقيقة فقط على استخدام MAMEMAN تطوير البرامج الحرجة للسلامة لمختلف سلسلة الطائرات ، بما في ذلك A380. "، Coq ( Frama-C مع Xavier Leroy) ، CAVEAT ، و verifier C التي طورتها CEA واستخدامها من قبل Airbus. | |
| ألتران | فرنسا ، باريس | SPARK سبارك المساهمين | |
| تفاحة | سانتا كلارا فالي ، كاليفورنيا ، الولايات المتحدة الأمريكية | الأجهزة والبرامج | |
| ذراع | أوستن ، تكساس ، وسان خوسيه ، كاليفورنيا ، الولايات المتحدة الأمريكية | الأجهزة | التحقق من ACL2 من الأجهزة الحسابية ، والتحقق من مواصفات الذراع الرسمية ، TLA+ Linux kernel |
| adacore | الولايات المتحدة الأمريكية ، نيويورك | ؟ | ؟ |
| alacris | ؟ | blockchain | |
| أنظمة BAE | Coq reddit | ||
| أنظمة الأساس | منطقة بوسطن وخليج ، الولايات المتحدة الأمريكية ؛ برلين وميونيخ ، ألمانيا | أمن الأنظمة ، حساب جدير بالثقة | Coq ، C++ ، github |
| شركة بوينغ | الولايات المتحدة الأمريكية | الفضاء ، الدفاع | Coq (لا دليل) ، Ivory (المصدر) |
| بوش | ألمانيا | السيارات | Astrée |
| تقنية Centaur | الولايات المتحدة الأمريكية | الأجهزة | ACL2 |
| أنظمة COG | أستراليا ، نيو ساوث ويلز ، سيدني | موقع | |
| Data61 | أستراليا | Isabelle/HOL (مشروع التحقق من SEL4) | |
| دريبر | الولايات المتحدة الأمريكية | الدفاع ، الفضاء | Coq ، Z3 |
| ethereum | سويسرا | تحديث Why3 : الطرق الرسمية ، Isabelle/HOL A LEM لإضفاء الطابع الرسمي على EVM وبعض أدلة Isabelle/HOL ، Coq التحقق الرسمي لعقود Ethereum | |
| الأمن | برمجة | Tamarin Wireguard | |
| التعلم espark | الولايات المتحدة الأمريكية ، إلينوي ، شيكاغو | تعليم | TLA+ الطرق الرسمية في الممارسة: استخدام TLA+ في ESPARK Learning |
| مرنة | عالمي | برنامج البحث والتحليلات | TLA+ Isabelle/HOL ELASTICSERESS-FORSILS ROPOSTORY CONKEN |
| وكالة الفضاء الأوروبية | TLA+ (التطوير الرسمي لـ RTOs المتمحور حول الشبكة: The European Space Agency's Rosetta spacecraft, which flew to a comet, used a real-time operating system called Virtuoso to control some of its instruments. The next version of that operating system, called OpenComRTOS, was developed using TLA+ ) | ||
| فيسبوك | الولايات المتحدة الأمريكية | INFER التحرك بسرعة مع التحقق من البرامج Zoncolan كيف يستخدم Facebook تحليلًا ثابتًا للكشف عن مشكلات الأمن ومنع | |
| fireeye | درسدن ، ألمانيا (انهار الفريق) | حماية | إعلان الوظيفة Coq : مهندس أساليب رسمية ومطور علمي في FireEye |
| عازف | روسيا ، spb | التمويل (blockchain) | Coq ، Agda |
| أرض رسمية | عالمي | برمجة | Coq التحقق من tezos blockchain |
| الاهتمامات الرسمية | برشلونة ، إسبانيا | قانون | برنامج DateTime الرسمي Coq |
| غالوا | بورتلاند ، أوريغون ، الولايات المتحدة الأمريكية | الاستشارات/البحث | Coq (؟) |
| gena gmbh | ألمانيا | CPAchecker مسار آخر لجودة البرنامج؟ التحقق الآلي للبرمجيات و OpenBSD وتطبيق وحدات شبكة OpenBSD OpenBSD | |
| جوجل | كاليفورنيا ، الولايات المتحدة الأمريكية | الحوسبة السحابية ، برامج الكمبيوتر ، الذكاء الاصطناعي | Coq (رمز بسيط المستوى من أجل الحساب التشفير-مع البراهين ، دون تنازلات (Chromium)) ، النمذجة الرسمية وتحليل Megastore من Google في الوقت الفعلي Maude |
| Grammatech | تعليقات مكتبة Frama-C C في ACSL لـ Frama-C: تقرير التجربة | ||
| برنامج Green Hills | الولايات المتحدة الأمريكية | الفضاء | الاستخدام الصناعي ACL2 لـ ACL2 |
| معهد كيستريل | الولايات المتحدة الأمريكية | أبحاث علوم الكمبيوتر | في الغالب ACL2 ، بعض إيزابيل/هول ، القليل من PVS و COQ. راجع موقع الويب ، وخاصة صفحات المشروع وصفحات الأشخاص ، للحصول على التفاصيل والمنشورات. |
| IBM | الولايات المتحدة الأمريكية | ؟ | SPIN/Promela PAUL E. McKenney's Journal ، ما هي RCU ، بشكل أساسي؟ (Linux kernel ، RCU) ، Coq q*cert |
| Ige+Xao | أوروبا | تصميم بمساعدة الكمبيوتر | تقرير تجربة Coq : تم تهريب القليل من CoQ داخل سياق تطوير CAD يتم استخدام CoQ للتحقق من ما يلي: (1) خوارزميات خاصة بالمجال (تطبيق "تصحيحات" على وثائق التصميم الكهربائي) (II) خوارزميات الرسم البياني (IV) (IV). استدلال نوع اللغة) (5) مشاريع البحث الصغيرة |
| إنتل | الولايات المتحدة الأمريكية | الأجهزة | Prover (خمسة عشر عامًا من التحقق الرسمي للممتلكات في Intel) ، HOL Light (التحقق الرسمي لخوارزميات تقسيم IA-64) ، TLA+ (التحقق الرسمي قبل RTL: تجربة Intel) |
| أنظمة غير رسمية | تورونتو ، فيينا ، لوزان ، برلين | blockchain ، الأنظمة الموزعة | TLA+ Apalache ، مدقق النموذج الرمزي لـ TLA+ ، إجماع Rust Tendermint BFT وبروتوكول اتصال Interblockchain في الصدأ مع مواصفات TLA+ ، الاختبار القائم على النموذج مع TLA+ و Apalache |
| infotecs | روسيا ، موسكو | TLA+ ، Coq ، البناء والتحقق الرسمي لخوارزمية الاستبعاد المتبادل الموزع ذي الخداع ، построение и верифифифицияияифеледененсссمنى | |
| ISP RAS | موسكو ، روسيا | أنظمة التشغيل ؛ الأجهزة | Frama-C ، Jessie ، Why3 Astraver ، Linux kernel وظائف تم التحقق منها رسميًا ؛ SPIN/Promela ، موقع Microtesk ؛ Event-B оелирование и врификацمس политик безопаенبعض уравлеمس довс о в в оерыхионых сиииионых сииционых ممكن مواصفات Isabelle/HOL الرسمية لنواة CAP9 |
| Kernkonzept GmbH | ألمانيا | أنظمة التشغيل | L4Re (المصدر) |
| كاسبرسكي | موسكو ، روسيا | الأمن/av | السبائك ، TLA ، Event-B (مصدر) ، Ivory (المصدر) |
| الآلات Zone Inc. | روسيا | برنامج ألعاب الهاتف المحمول ، والحوسبة في الوقت الفعلي ، والشبكات القائمة على السحابة | TLA+ Twitter |
| Microsoft | ريدموند ، الولايات المتحدة الأمريكية | تطوير البرمجيات | أدلة TLA+ TLA+ ، التفكير للمبرمجين ، مواصفات TLA+ عالية المستوى لمستويات الاتساق الخمسة التي يقدمها Azure Cosmos DB ، Microsoft's Static Driver Verifier للأنظمة الثابتة الشاملة على نطاق الجهاز في Clousot . |
| mongodb | نيويورك ، الولايات المتحدة الأمريكية | تطوير البرمجيات | TLA+ TLA+ Spec من جزء مبسط من نظام النسخ المتماثل MongoDB |
| ناسا | الولايات المتحدة الأمريكية | فضاء | PVS NASA LANGLEY MOTIONAL MOTIONAL PROGRAM. JPF Java Pathfinder ، مجموعة هندسة البرمجيات القوية ، Model Checking المختبر Propulls ، تطبيقات SPIN/Promela الملهمة لـ Spin ، PVS (المصدر) |
| المختبرات البدوية | باريس ، فرنسا | blockchain | صفحة Coq على التحقق من البرامج |
| أوراكل | ريدوود شورز ، كاليفورنيا ، الولايات المتحدة الأمريكية | برنامج المؤسسة ، الحوسبة السحابية ، أجهزة الكمبيوتر | ACL2 (نظريات تثبت عن Java و JVM مع ACL2) |
| برنامج معين | TLA+ TLA+ مواصفات NServiceBus | ||
| pingcap | TLA+ TLA+ في الحزب | ||
| تقنية المثل | أوروبا | السكك الحديدية | Model checking |
| Rusbitech (рситех) | روسيا ، موسكو | сماد | Frama-C ، Event-B (моделирование и веификацمس политик безопасности уравлسبب |
| روكويل كولينز | الولايات المتحدة الأمريكية ، سيدار رابيدز ، أيوا | أنظمة ضمان عالية | طرق رسمية في صناعة الطيران: اتبع المال |
| سيروكيل | تالين ، إستونيا | fintech ، blockchain ، إنترنت الأشياء ، التعلم الآلي ، التحقق الرسمي | Agda |
| ملخص | ؟ | ؟ | موقع |
| Systerel | فرنسا | البرمجيات ، الاستشارات ، الخدمة | S3 A Model Checker للغة Synchrone ، طريقة B ، الحدث ب/رودن. التوظيف. |
| سيففي | الولايات المتحدة الأمريكية ، منطقة خليج سان فرانسيسكو | الأجهزة | Coq LinkedIn |
| StateBox | أمستردام ، هولندا | blockchain | Idris (جيثب) |
| Sukhoi | روسيا ، موسكو | الطيران والدفاع | ANSYS SCADE Suite (المصدر - مترجم تم التحقق منه رسميًا للبريق) |
| ثاليس | Frama-C (نهج التحقق الرسمي من أسفل إلى أعلى للحصول على شهادة المعايير الشائعة: تطبيق على الجهاز الظاهري Javacard) | ||
| Trustinsoft | الولايات المتحدة الأمريكية ، كاليفورنيا ، سان فرانسيسكو | - | موقع TrustInSoft Analyzer |
| أنظمة جديرة بالثقة | أستراليا ، سيدني | Isabelle/HOL ، موقع Coq | |
| اثنان ستة تقنيات | الولايات المتحدة الأمريكية | أبحاث الدفاع | Isabelle/HOL ، التحقق من الأجهزة (مثال) ، Coq (مثال) |
| أبحاث Jetbrains | سانت بطرسبرغ ، روسيا | - | Coq (المصدر) |
| ццт | موسكو ، روسيا | ؟ | SPIN/Promela еетоыы и средстсифифиابت |
| T- المنصات | موسكو ، روسيا | - | Coq ، SPIN/Promela ، TLA+ ، McErlang ، mCRL2 الموظف السيرة الذاتية |
| سيرن | جينيف ، سويسرا | برنامج التحكم mCRL2 لتجربة CMS في CERN's Large Hadron Collider | |
| ياندكس | برمجة | خوارزمية النسخ المتماثل TLA+ Clickhouse ، مخصص للذاكرة الخالية من القفل | |
| Zilliqa | سنغافورة | blockchain | Coq SCILLA-COQ |
| الأمواج | blockchain | ؟؟؟ |
