practical fm
1.0.0
Jika Anda melihat perusahaan dalam daftar yang tidak ada lagi, atau tidak menggunakan metode formal lagi, silakan kirim permintaan tarik dengan penjelasan. Hal yang sama berlaku jika Anda sedang bekerja di, atau mengetahui perusahaan yang menggunakan metode formal tetapi tidak ada dalam daftar. Harap sertakan situs web, GitHub (jika ada), lokasi, dan sektor. Jika perusahaan merekrut, harap sertakan tautan ke iklan.
| Nama | Lokasi | Sektor | Sumber |
|---|---|---|---|
| Amazon | Amerika Serikat | e -commerce, cloud computing | TLA+ Bagaimana Layanan Web Amazon Menggunakan Metode Formal, Penggunaan Metode Formal Di Layanan Web Amazon, Model CBMC Memeriksa kode boot dari AWS Data Center, Dafny AWS Encryption SDK |
| Airbus | Perancis | Astrée : "Pada tahun 2003, Astrée membuktikan tidak adanya kesalahan runtime dalam perangkat lunak pengendalian penerbangan utama dari model Airbus. Sistem 132.000 baris kode C dianalisis sepenuhnya secara otomatis dalam 80 menit pada AMD 64 yang menggunakan AirB. Dalam pengembangan perangkat lunak kritis-keselamatan untuk berbagai seri pesawat, termasuk A380. ", Coq (wawancara dengan Xavier Leroy), CAVEAT , c-verifier yang dikembangkan oleh CEA dan digunakan oleh Airbus., Frama-C (penggunaan industri dari proses rekayasa perangkat lunak berbasis metode formal yang aman dan efisien dalam avionik). | |
| Altran | Prancis, Paris | Kontributor Spark SPARK | |
| Apel | Santa Clara Valley, California, AS | Perangkat keras dan perangkat lunak | |
| Lengan | Austin, Texas, & San Jose, California, AS | Perangkat keras | ACL2 Verifikasi perangkat keras aritmatika, memverifikasi terhadap spesifikasi lengan resmi, kernel TLA+ Linux |
| Adacore | AS, New York | ? | ? |
| Alacris | ? | Blockchain | |
| Sistem BAE | Coq Reddit | ||
| Sistem Bedrock | Boston & Bay Area, AS; Berlin & Munich, Jerman | Keamanan Sistem, Hitung yang Dapat Dipercaya | Coq , C++ , GitHub |
| The Boeing Company | Amerika Serikat | Aerospace, pertahanan | Coq (tidak ada bukti), Ivory (sumber) |
| Bosch | Jerman | Otomotif | Astrée |
| Teknologi Centaur | Amerika Serikat | Perangkat keras | ACL2 |
| Sistem COG | Australia, New South Wales, Sydney | Lokasi | |
| Data61 | Australia | Isabelle/HOL (proyek verifikasi Sel4) | |
| Pedagang kain | Amerika Serikat | Pertahanan, Ruang | Coq , Z3 |
| Ethereum | Swiss | Why3 Dev Update: Metode Formal, Isabelle/HOL Formalisasi LEM EVM dan beberapa bukti Isabelle/Hol, Verifikasi Formal Coq Kontrak Ethereum | |
| EDGESECURITY | Perangkat lunak | Tamarin Wireguard | |
| Pembelajaran Espark | AS, IL, Chicago | Pendidikan | TLA+ Metode Formal Dalam Praktek: Menggunakan TLA+ di Espark Learning |
| Elastis | Global | Perangkat Lunak Cari & Analytics | TLA+ Isabelle/HOL Elasticsearch-Formal-Model Repositori Conference Talk dan Posisi Terbuka Saat Ini |
| Badan Antariksa Eropa | TLA+ (Pengembangan Formal RTOS yang berpusat pada jaringan: 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+ ) | ||
| Amerika Serikat | INFER bergerak cepat dengan verifikasi perangkat lunak Zoncolan bagaimana facebook menggunakan analisis statis untuk mendeteksi dan mencegah masalah keamanan | ||
| FireEye | Dresden, Jerman (tim mati) | Keamanan | Pengumuman Pekerjaan Coq : Insinyur Metode Formal dan Pengembang Ilmiah di FireEye |
| Kedap halus | Rusia, spb | Keuangan (blockchain) | Coq , Agda |
| Tanah formal | Global | Perangkat lunak | Verifikasi Coq dari Blockchain Tezos |
| Pembenaran Formal | Barcelona, Spanyol | Hukum | Coq Perangkat lunak datetime formal |
| Galois | Portland, Oregon, AS | Konsultasi/Penelitian | Coq (?) |
| ALUAA GMBH | Jerman | CPAchecker jalur lain untuk kualitas perangkat lunak? Verifikasi Perangkat Lunak Otomatis dan OpenBSD dan Aplikasi Verifikasi Perangkat Lunak untuk Modul Jaringan OpenBSD | |
| CA, AS | Cloud Computing, Computer Software, AI | Coq (kode tingkat tinggi sederhana untuk aritmatika kriptografi-dengan bukti, tanpa kompromi (kromium)), pemodelan formal dan analisis megastor Google di Maude waktu nyata | |
| Grammatech | Anotasi Perpustakaan Frama-C C di ACSL untuk Frama-C: Laporan Pengalaman | ||
| Perangkat lunak Green Hills | Amerika Serikat | Aerospace | ACL2 Penggunaan Industri ACL2 |
| Institut Kestrel | Amerika Serikat | Penelitian Ilmu Komputer | Sebagian besar acl2, beberapa Isabelle/hol, sedikit PV dan COQ. Lihat situs web, terutama halaman proyek dan halaman orang, untuk detail dan publikasi. |
| IBM | Amerika Serikat | ? | Jurnal SPIN/Promela Paul E. McKenney, Apa itu RCU, pada dasarnya? (Kernel Linux, RCU), Coq Q*Cert |
| IgE+xao | Eropa | Desain Bantuan Komputer | Laporan Pengalaman Coq : menyelundupkan sedikit COQ di dalam konteks pengembangan CAD COQ digunakan untuk memverifikasi hal-hal berikut: (i) algoritma khusus domain (penerapan "tambalan" ke dokumen desain listrik) (ii) algoritma grafik (Pencarian, tata letak pepohonan priory, tata letak b & b tsp, ...) (iii) Struktur Data, tata letak que, B & B TSP, ...) (iii) (iii) Data, Inferensi Jenis Bahasa) (v) Proyek Penelitian Kecil |
| Intel | Amerika Serikat | Perangkat keras | Prover (lima belas tahun verifikasi properti formal di Intel), HOL Light (verifikasi formal algoritma divisi IA-64), TLA+ (Verifikasi Formal Pra-RTL: Pengalaman Intel) |
| Sistem informal | Toronto, Wina, Lausanne, Berlin | Blockchain, sistem terdistribusi | TLA+ Apalache, Pemeriksa Model Simbolik untuk TLA+, Konsensus BFT Rust Tendermint dan Protokol Komunikasi InterblockChain dalam karat dengan spesifikasi TLA+, pengujian berbasis model dengan TLA+ dan Apalache |
| Infotec | Rusia, Moskow | TLA+ , Coq , konstruksi dan verifikasi formal dari algoritma eksklusi bersama yang didistribusikan dengan kesalahan, построение и верификация отазосто secara аориб pemeriksaan осо оilan осазойчtoran | |
| ISP Ras | Moskow, Rusia | Sistem operasi; perangkat keras | Frama-C , Jessie , Why3 Astraver, Linux Kernel Library berfungsi secara formal diverifikasi; Situs SPIN/Promela , Microtesk ; Event-B моделированиilik и Верификация политик бопасност masuk упввancing д д д д д д д д dasar; Isabelle/HOL spesifikasi formal kernel CAP9 |
| Kernkonzept GmbH | Jerman | Sistem Operasi | L4Re (sumber) |
| Kaspersky | Moskow, Rusia | Keamanan/av | Paduan, TLA, Event-B (Sumber), Ivory (Sumber) |
| Mesin Zone Inc. | Rusia | Perangkat lunak game seluler, komputasi real-time, jaringan berbasis cloud | TLA+ Twitter |
| Microsoft | Redmond, AS | Pengembangan Perangkat Lunak | TLA+ TLA+ Bukti, Berpikir untuk Pemrogram, Spesifikasi TLA+ tingkat tinggi untuk lima tingkat konsistensi yang ditawarkan oleh Azure Cosmos DB, Microsoft's Static Driver Verifier Analisis Statis Telata Penggerak Perangkat, Metode Formal Clousot dalam skala Microsoft, Metode Formal, Metode Formal untuk Sistem Terdistribusi, Metode Formal pada Microsoft dalam Microsoft dalam Microsoft Microsoft |
| Mongodb | New York, AS | Pengembangan Perangkat Lunak | TLA+ TLA+ Spec dari bagian yang disederhanakan dari sistem replikasi MongoDB |
| NASA | Amerika Serikat | Ruang angkasa | Program Penelitian Metode Formal PVS NASA Langley. JPF Java Pathfinder, Grup Rekayasa Perangkat Lunak yang Kuat, Model Checking Jet Propulsion Laboratory, SPIN/Promela menginspirasi aplikasi spin, PVS (sumber) |
| Laboratorium Nomaden | Paris, Prancis | blockchain | Halaman Coq tentang Verifikasi Perangkat Lunak |
| Peramal | Redwood Shores, CA, USA | Perangkat lunak perusahaan, komputasi awan, perangkat keras komputer | ACL2 (Teorema Membuktikan Tentang Java dan JVM dengan ACL2) |
| Perangkat lunak tertentu | TLA+ TLA+ Spesifikasi untuk NServicebus | ||
| Pingcap | TLA+ tla+ di tidb | ||
| Teknologi pepatah | Eropa | Kereta api | Model checking |
| Rusbitech (рсбитех) | Rusia, Moskow | Системное по | Frama-C , Event-B (моделированиilik и Верификация политик бопасности управления доосту) в оиосте 201) в дист A дциост 201 д д p о dasar |
| Rockwell Collins | AS, Cedar Rapids, Iowa | Sistem Jaminan Tinggi | Metode formal dalam industri kedirgantaraan: Ikuti uang |
| Serokell | Tallinn, Estonia | Fintech, blockchain, IoT, pembelajaran mesin, verifikasi formal | Agda |
| Ringkasan | ? | ? | Lokasi |
| Systerel | Perancis | Perangkat Lunak, Konsultasi, Layanan | S3 Pemeriksa Model untuk Bahasa Synchrone, Metode B, Event-B/Rodin. Merekrut. |
| Sifive | USA, Area Teluk San Francisco | Perangkat keras | Coq LinkedIn |
| StateBox | Amsterdam, Belanda | Blockchain | Idris (GitHub) |
| Sukhoi | Rusia, Moskow | Aerospace dan pertahanan | ANSYS SCADE Suite (sumber - kompiler yang diverifikasi secara formal untuk kilau) |
| Thales | Frama-C (pendekatan verifikasi formal bottom-up untuk sertifikasi kriteria umum: Aplikasi untuk Javacard Virtual Machine) | ||
| Trustinsoft | AS, CA, San Francisco | - | Situs TrustInSoft Analyzer |
| Sistem yang dapat dipercaya | Australia, Sydney | Situs Isabelle/HOL , Coq | |
| Dua enam teknologi | Amerika Serikat | Penelitian Pertahanan | Isabelle/HOL , verifikasi perangkat keras (contoh), Coq (contoh) |
| Penelitian JetBrains | Saint Petersburg, Rusia | - | Coq (Sumber) |
| Цц | Moskow, Rusia | ? | SPIN/Promela методы и седства верификации протоколов когереancingтности памяти balik |
| T-platform | Moskow, Rusia | - | Coq , SPIN/Promela , TLA+ , McErlang , mCRL2 Karyawan CV |
| CERN | Genève, Swiss | Perangkat lunak kontrol mCRL2 dari percobaan CMS di Cern's Large Hadron Collider | |
| Yandex | Perangkat lunak | TLA+ Algoritma Replikasi Klik, Allocator Memori Bebas Kunci | |
| Zilliqa | Singapura | Blockchain | Proyek Coq Scilla-Coq |
| Ombak | Blockchain | ??? |
