practical fm
1.0.0
หากคุณเห็น บริษัท ในรายการที่ไม่มีอยู่อีกต่อไปหรือไม่ใช้วิธีการที่เป็นทางการอีกต่อไปโปรดส่งคำขอดึงพร้อมคำอธิบาย เช่นเดียวกันถ้าคุณกำลังทำงานอยู่หรือรู้จัก บริษัท ที่ใช้วิธีการอย่างเป็นทางการ แต่ไม่ได้อยู่ในรายการ โปรดรวมเว็บไซต์ GitHub (ถ้ามี) สถานที่และภาค หาก บริษัท กำลังจ้างโปรดระบุลิงก์ไปยังโฆษณา
| ชื่อ | ที่ตั้ง | ภาค | แหล่งที่มา |
|---|---|---|---|
| อเมซอน | สหรัฐอเมริกา | อีคอมเมิร์ซคลาวด์คอมพิวติ้ง | TLA+ วิธีการที่ Amazon Web Services ใช้วิธีการอย่างเป็นทางการการใช้วิธีการอย่างเป็นทางการที่ Amazon Web Services, CBMC Model ตรวจสอบรหัสบูตจากศูนย์ข้อมูล AWS, Dafny AWS Encryption SDK |
| แอร์บัส | ฝรั่งเศส | Astrée : "ในปี 2003 Astréeพิสูจน์ให้เห็นว่าไม่มีข้อผิดพลาดรันไทม์ใด ๆ ในซอฟต์แวร์ควบคุมการบินขั้นต้นของรุ่นแอร์บัสระบบ C 132,000 บรรทัดของรหัส C ได้รับการวิเคราะห์โดยอัตโนมัติในเวลาเพียง 80 นาทีบนพีซี 32-bit โดยใช้ Athlon 64 การพัฒนาซอฟต์แวร์ความปลอดภัยที่สำคัญสำหรับชุดเครื่องบินต่าง ๆ รวมถึง A380 ", Coq (สัมภาษณ์กับ Xavier Leroy), CAVEAT , C-verifier ที่พัฒนาโดย CEA และใช้โดย Airbus, Frama-C | |
| คนอื่น ๆ | ฝรั่งเศสปารีส | ผู้มีส่วนร่วม Spark SPARK | |
| แอปเปิล | Santa Clara Valley, California, USA | ฮาร์ดแวร์และซอฟต์แวร์ | |
| แขน | Austin, Texas, & San Jose, California, USA | ฮาร์ดแวร์ | การตรวจสอบ ACL2 ของฮาร์ดแวร์เลขคณิตตรวจสอบข้อกำหนดของแขนอย่างเป็นทางการ, เคอร์เนล TLA+ Linux |
| อดัคอร์ | สหรัฐอเมริกานิวยอร์ก | - | - |
| อลาคริส | - | blockchain | |
| ระบบ BAE | Coq reddit | ||
| ระบบข้อเท็จจริง | พื้นที่บอสตัน & เบย์สหรัฐอเมริกา; เบอร์ลิน & มิวนิคประเทศเยอรมนี | ความปลอดภัยของระบบการคำนวณที่น่าเชื่อถือ | Coq , C++ , GitHub |
| บริษัท โบอิ้ง | สหรัฐอเมริกา | การบินและอวกาศการป้องกัน | Coq (ไม่มีหลักฐาน), Ivory (แหล่งที่มา) |
| บอสช์ | ประเทศเยอรมนี | เกี่ยวกับยานยนต์ | ดอน |
| เทคโนโลยีเซนทอร์ | สหรัฐอเมริกา | ฮาร์ดแวร์ | ACL2 |
| ระบบ COG | ออสเตรเลียนิวเซาธ์เวลส์ซิดนีย์ | เว็บไซต์ | |
| data61 | ออสเตรเลีย | Isabelle/HOL (โครงการตรวจสอบ SEL4) | |
| ผ้าม่าน | สหรัฐอเมริกา | การป้องกันพื้นที่ | Coq , Z3 |
| Ethereum | สวิตเซอร์แลนด์ | Why3 dev update: วิธีการอย่างเป็นทางการ, Isabelle/HOL a lem เป็นทางการของ EVM และการพิสูจน์ Isabelle/hol บาง Coq การตรวจสอบอย่างเป็นทางการของสัญญา Ethereum | |
| ความปลอดภัย | ซอฟต์แวร์ | Tamarin Wireguard | |
| การเรียนรู้ espark | USA, IL, Chicago | การศึกษา | วิธีการ TLA+ อย่างเป็นทางการในทางปฏิบัติ: การใช้ TLA+ ที่การเรียนรู้ espark |
| ยืดหยุ่น | ทั่วโลก | ซอฟต์แวร์ค้นหาและวิเคราะห์ | TLA+ Isabelle/HOL ELASTICSEARCH-FORMAL-MODELS CONFONITION TALK TALK และตำแหน่งเปิดปัจจุบัน |
| สำนักงานอวกาศยุโรป | 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 |
| Galois | พอร์ตแลนด์โอเรกอนสหรัฐอเมริกา | การให้คำปรึกษา/การวิจัย | Coq (?) |
| GMBH GMBH | ประเทศเยอรมนี | CPAchecker อีกเส้นทางหนึ่งสำหรับคุณภาพซอฟต์แวร์? การตรวจสอบซอฟต์แวร์อัตโนมัติและ OpenBSD และแอปพลิเคชันการตรวจสอบซอฟต์แวร์เพื่อโมดูลเครือข่าย OpenBSD | |
| CA, USA | คลาวด์คอมพิวติ้งซอฟต์แวร์คอมพิวเตอร์ AI | Coq (รหัสระดับสูงอย่างง่ายสำหรับเลขคณิตการเข้ารหัส-ด้วยการพิสูจน์โดยไม่มีการประนีประนอม (โครเมียม)) การสร้างแบบจำลองอย่างเป็นทางการและการวิเคราะห์ megastore ของ Google ในม้อดแบบเรียลไทม์ | |
| Grammatech | คำอธิบายประกอบห้องสมุด Frama-C c ใน ACSL สำหรับ FRAMA-C: รายงานประสบการณ์ | ||
| ซอฟต์แวร์กรีนฮิลส์ | สหรัฐอเมริกา | การบินและอวกาศ | ACL2 การใช้ ACL2 |
| Kestrel Institute | สหรัฐอเมริกา | การวิจัยวิทยาศาสตร์คอมพิวเตอร์ | ส่วนใหญ่ ACL2, Isabelle/Hol, PV และ COQ เล็กน้อย ดูเว็บไซต์โดยเฉพาะหน้าโครงการและหน้าผู้คนสำหรับรายละเอียดและสิ่งพิมพ์ |
| IBM | สหรัฐอเมริกา | - | วารสาร SPIN/Promela Paul E. McKenney, RCU คืออะไรพื้นฐาน? (Linux Kernel, RCU), Coq Q*CERT |
| ige+xao | ยุโรป | การออกแบบที่ได้รับความช่วยเหลือจากคอมพิวเตอร์ | รายงานประสบการณ์ Coq : การลักลอบขน COQ เล็กน้อยภายในบริบทการพัฒนา CAD COQ ใช้เพื่อตรวจสอบสิ่งต่อไปนี้: (i) อัลกอริทึมเฉพาะโดเมน (การประยุกต์ใช้ "แพทช์" กับเอกสารการออกแบบไฟฟ้า) (ii) การจัดทำกราฟ (iii) (การอนุมานประเภทภาษาที่กำหนดเอง) (v) โครงการวิจัยขนาดเล็ก |
| Intel | สหรัฐอเมริกา | ฮาร์ดแวร์ | Prover (สิบห้าปีของการตรวจสอบทรัพย์สินอย่างเป็นทางการใน Intel), HOL Light (การตรวจสอบอย่างเป็นทางการของอัลกอริทึมการแบ่ง IA-64), TLA+ (การตรวจสอบอย่างเป็นทางการก่อน RTL: ประสบการณ์ Intel) |
| ระบบนอกระบบ | โตรอนโต, เวียนนา, โลซาน, เบอร์ลิน | blockchain ระบบกระจาย | TLA+ Apalache, ตัวตรวจสอบโมเดลสัญลักษณ์สำหรับ TLA+, Rust Tendermint ฉันทามติ BFT และโปรโตคอลการสื่อสาร interblockchain ในการเกิดสนิมด้วยสเป็ค TLA+, การทดสอบแบบจำลองด้วย TLA+ และ Apalache |
| อินโฟเทค | รัสเซียมอสโก | TLA+ , Coq , การก่อสร้างและการตรวจสอบอย่างเป็นทางการของอัลกอริทึมการยกเว้นการกระจายความผิดพลาด, построениииверифкацияотазоуивогои:าล | |
| ISP RAS | มอสโกรัสเซีย | ระบบปฏิบัติการ ฮาร์ดแวร์ | Frama-C , Jessie , Why3 Astraver, Linux Kernel Library ฟังก์ชั่นการตรวจสอบอย่างเป็นทางการ; SPIN/Promela , Microtesk Site; Event-B моделированиеиверикацияолитикопопасностиравлениสาธารณะ Isabelle/HOL Specification อย่างเป็นทางการของเคอร์เนล cap9 |
| Kernkonzept GmbH | ประเทศเยอรมนี | ระบบปฏิบัติการ | L4Re (แหล่งที่มา) |
| Kaspersky | มอสโกรัสเซีย | ความปลอดภัย/av | โลหะผสม, TLA, Event-B (แหล่งที่มา), Ivory (แหล่งที่มา) |
| Machine Zone Inc. | รัสเซีย | ซอฟต์แวร์เกมมือถือการคำนวณแบบเรียลไทม์เครือข่ายบนคลาวด์ | TLA+ twitter |
| Microsoft | Redmond, USA | การพัฒนาซอฟต์แวร์ | TLA+ TLA+ พิสูจน์การคิดสำหรับโปรแกรมเมอร์, ข้อกำหนด TLA+ ระดับสูงสำหรับห้าระดับความสอดคล้องที่นำเสนอโดย Azure Cosmos DB, Microsoft's Static Driver Verifier อย่างละเอียดการวิเคราะห์แบบคงที่ของไดรเวอร์อุปกรณ์ Clousot cloust contrace ด้วยการตีความบทคัดย่อ |
| MongoDB | นิวยอร์กสหรัฐอเมริกา | การพัฒนาซอฟต์แวร์ | TLA+ TLA+ ข้อมูลจำเพาะของส่วนที่เรียบง่ายของระบบการจำลองแบบ MongoDB |
| นาซ่า | สหรัฐอเมริกา | ช่องว่าง | PVS NASA Langley วิธีการอย่างเป็นทางการโครงการวิจัย JPF Java Pathfinder, กลุ่มวิศวกรรมซอฟต์แวร์ที่แข็งแกร่ง, Model Checking ห้องปฏิบัติการ Jet Propulsion, SPIN/Promela ที่สร้างแรงบันดาลใจในการหมุน, PVS (แหล่งที่มา) |
| ห้องปฏิบัติการเร่ร่อน | ปารีสฝรั่งเศส | blockchain | หน้า Coq ในการตรวจสอบซอฟต์แวร์ |
| คำพยากรณ์ | Redwood Shores, CA, USA | ซอฟต์แวร์ระดับองค์กร, คลาวด์คอมพิวติ้ง, ฮาร์ดแวร์คอมพิวเตอร์ | ACL2 (พิสูจน์ทฤษฎีบทเกี่ยวกับ Java และ JVM กับ ACL2) |
| ซอฟต์แวร์เฉพาะ | TLA+ tla+ ข้อมูลจำเพาะสำหรับ nservicebus | ||
| pingcap | TLA+ tla+ ใน tidb | ||
| เทคโนโลยีสุภาษิต | ยุโรป | ทางรถไฟ | Model checking |
| Rusbitech (руитех) | รัสเซียมอสโก | системноео | Frama-C , Event-B (моделированиеиверикацияолитикезопасностиравлениสาธารณะ |
| Rockwell Collins | USA, Cedar Rapids, Iowa | ระบบประกันภัยสูง | วิธีการอย่างเป็นทางการในอุตสาหกรรมการบินและอวกาศ: ติดตามเงิน |
| Serokell | ทาลลินน์เอสโตเนีย | Fintech, blockchain, IoT, การเรียนรู้ของเครื่อง, การตรวจสอบอย่างเป็นทางการ | Agda |
| เรื่องย่อ | - | - | เว็บไซต์ |
| Systerel | ฝรั่งเศส | ซอฟต์แวร์การให้คำปรึกษาบริการ | S3 ตัวตรวจสอบแบบจำลองสำหรับภาษาซิงโครน, วิธี B, Event-B/Rodin การสรรหา |
| มีมาก่อน | สหรัฐอเมริกาบริเวณอ่าวซานฟรานซิสโก | ฮาร์ดแวร์ | Coq linkedIn |
| สเตทบ็อกซ์ | อัมสเตอร์ดัมเนเธอร์แลนด์ | blockchain | Idris (GitHub) |
| ซูกฮอย | รัสเซียมอสโก | การบินและอวกาศและการป้องกัน | ANSYS SCADE Suite (แหล่งที่มา - คอมไพเลอร์ที่ผ่านการตรวจสอบอย่างเป็นทางการสำหรับ Luster) |
| Thales | Frama-C (วิธีการตรวจสอบอย่างเป็นทางการจากล่างขึ้นบนสำหรับการรับรองเกณฑ์ทั่วไป: แอปพลิเคชันกับ Javacard Virtual Machine) | ||
| TrustInsoft | สหรัฐอเมริกา, แคลิฟอร์เนีย, ซานฟรานซิสโก | - | ไซต์ TrustInSoft Analyzer |
| ระบบที่น่าเชื่อถือ | ออสเตรเลียซิดนีย์ | Isabelle/HOL , ไซต์ Coq | |
| สองเทคโนโลยีหก | สหรัฐอเมริกา | การวิจัยกลาโหม | Isabelle/HOL , การตรวจสอบฮาร์ดแวร์ (ตัวอย่าง), Coq (ตัวอย่าง) |
| การวิจัย Jetbrains | เซนต์ปีเตอร์สเบิร์กรัสเซีย | - | Coq (แหล่งที่มา) |
| мцст | มอสโกรัสเซีย | - | SPIN/Promela метоыисредстваверикацииротоколовкогерентнтностиамสาธารณะ |
| T-platforms | มอสโกรัสเซีย | - | Coq , SPIN/Promela , TLA+ , McErlang , CV Employee mCRL2 |
| เซิร์น | Genève, สวิตเซอร์แลนด์ | ซอฟต์แวร์ควบคุม mCRL2 ของการทดลอง CMS ที่ Cern Hadron Collider ของ CERN | |
| Yandex | ซอฟต์แวร์ | อัลกอริทึมการจำลองแบบ TLA+ Clickhouse, การจัดสรรหน่วยความจำฟรีล็อค | |
| zilliqa | สิงคโปร์ | blockchain | โครงการ Coq Scilla-Coq |
| คลื่น | blockchain | - |
