practical fm
1.0.0
Si vous voyez une entreprise sur la liste qui n'existe plus ou n'utilise plus de méthodes formelles, veuillez envoyer une demande de traction avec une explication. Il en va de même si vous travaillez actuellement ou connaissez une entreprise qui utilise des méthodes formelles mais qui ne figure pas sur la liste. Veuillez inclure le site Web, GitHub (le cas échéant), les emplacements et le secteur. Si l'entreprise embauche, veuillez inclure un lien vers l'annonce.
| Nom | Emplacement | Secteur | Source |
|---|---|---|---|
| Amazone | USA | commerce électronique, cloud computing | TLA+ Comment Amazon Web Services utilise des méthodes formelles, l'utilisation de méthodes formelles chez Amazon Web Services, le modèle CBMC vérifiant le code de démarrage à partir des centres de données AWS, Dafny AWS Encryption SDK |
| Airbus | France | Astrée : "En 2003, Astrée a prouvé l'absence de toutes les erreurs d'exécution dans le logiciel de contrôle de vol primaire d'un modèle Airbus. Les 132 000 lignes de C du système ont été analysées complètement automatiquement en seulement 80 minutes sur un AMD ATHLON à 32 bits en utilisant 580mb Le développement de logiciels critiques pour la sécurité pour diverses séries d'avions, y compris l'A380. ", Coq (entretien avec Xavier Leroy), CAVEAT , un c-Verifier développé par CEA et utilisé par Airbus., Frama-C (utilisation industrielle d'un processus d'ingénierie de logiciels formel sûr et efficace basé sur des méthodes dans Avionics). | |
| Altran | France, Paris | Contributeurs Spark SPARK | |
| Pomme | Santa Clara Valley, Californie, États-Unis | Matériel et logiciel | |
| Bras | Austin, Texas et San Jose, Californie, États-Unis | Matériel | Vérification ACL2 du matériel arithmétique, vérifiant la spécification officielle du bras, le noyau TLA+ Linux |
| Adacore | États-Unis, New York | ? | ? |
| Alacris | ? | Blockchain | |
| Systèmes BAE | Coq Reddit | ||
| Systèmes de roche | Boston & Bay Area, États-Unis; Berlin et Munich, Allemagne | Sécurité des systèmes, calcul digne de confiance | Coq , C++ , github |
| La Boeing Company | USA | Aérospatial, défense | Coq (pas de preuve), Ivory (source) |
| Bosch | Allemagne | Automobile | Astraine |
| Technologie Centaure | USA | Matériel | ACL2 |
| COG Systèmes | Australie, Nouvelle-Galles du Sud, Sydney | Site | |
| Data61 | Australie | Isabelle/HOL (le projet de vérification SEL4) | |
| Drapier | USA | Défense, espace | Coq , Z3 |
| Ethereum | Suisse | MISE Why3 JOUR DE DEV: Méthodes formelles, Isabelle/HOL A Lem Formalisation de l'EVM et certaines preuves Isabelle / Hol, vérification formelle Coq des contrats Ethereum | |
| Ectésécurité | Logiciel | Tamarin Wireguard | |
| apprentissage en espèce | États-Unis, IL, Chicago | Éducation | TLA+ Méthodes formelles dans la pratique: utiliser TLA + chez ESPARK LECTOY |
| Élastique | Mondial | Logiciel de recherche et d'analyse | TLA+ Isabelle/HOL ELASTICSEARCH-FORMAL-MODELS REPOSETORY Conference Talk et Postes ouverts actuels |
| Agence spatiale européenne | TLA+ (développement formel d'un RTOS axé sur le réseau: 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+ ) | ||
| USA | INFER de déménagement rapidement avec la vérification du logiciel Zoncolan comment Facebook utilise une analyse statique pour détecter et prévenir les problèmes de sécurité | ||
| Foyer | Dresde, Allemagne (équipe disparue) | Sécurité | Annonce d'emploi Coq : Ingénieur de méthodes formelles et développeur scientifique chez FireEye |
| Nageoire à nageoires | Russie, SPB | Finance (blockchain) | Coq , Agda |
| Terre formelle | Mondial | Logiciel | Vérification Coq de la blockchain Tezos |
| Vindications formelles | Barcelone, Espagne | Loi | Coq FORMALISED DATETime Software |
| Galois | Portland, Oregon, États-Unis | Conseil / recherche | Coq (?) |
| Geuta gmbh | Allemagne | CPAchecker un autre chemin pour la qualité du logiciel? Vérification des logiciels automatisés et OpenBSD et application de la vérification du logiciel aux modules réseau OpenBSD | |
| CA, USA | Cloud Computing, logiciel informatique, AI | Coq (Code simple de haut niveau pour l'arithmétique cryptographique - avec des preuves, sans compromis (chrome)), la modélisation formelle et l'analyse du mégastore de Google dans Maude en temps réel | |
| Grammatech | Annotations de bibliothèque Frama-C C dans ACSL pour FraM-C: Rapport d'expérience | ||
| Logiciel Green Hills | USA | Aérospatial | ACL2 Utilisation industrielle d'ACL2 |
| Institut Kestrel | USA | Recherche en informatique | Surtout ACL2, certains Isabelle / Hol, un peu de PVS et de Coq. Voir le site Web, en particulier les pages de projet et les pages de personnes, pour plus de détails et de publications. |
| Ibm | USA | ? | SPIN/Promela Paul E. McKenney's Journal, Qu'est-ce que RCU, fondamentalement? (Linux Kernel, RCU), Coq Q * CERT |
| Ige + xao | Europe | Conception assistée par ordinateur | Rapport d'expérience Coq : Conversement d'un peu de COQ dans un contexte de développement CAD, Coq est utilisé pour vérifier ce qui suit: (i) Algorithmes spécifiques au domaine (application des "correctifs" sur les documents de conception électrique) (ii) Algorithmes de graphes (A * Recherche, Longueur-Présidence Présentation des arbres, B&B TSP, ...) (III Structures de questions (Union-Find, Priorités (Inférence du type de langue personnalisée) (v) PROJETS DE RECHERCHE |
| Intel | USA | Matériel | Prover (quinze ans de vérification formelle des biens dans Intel), HOL Light (vérification formelle des algorithmes de division IA-64), TLA+ (vérification formelle pré-RTL: une expérience Intel) |
| Systèmes informels | Toronto, Vienne, Lausanne, Berlin | Blockchain, systèmes distribués | TLA+ Apalache, vérificateur de modèle symbolique pour TLA +, Rust Tendermint BFT Consensus et InterblockChain Communication Protocol in Rust with TLA + Specs, Test basé sur le modèle avec TLA + et Apalache |
| Infotecs | Russie, Moscou | TLA+ , Coq , construction et vérification formelle d'un algorithme d'exclusion mutuel distribué tolérant aux défauts, построение В верификация отйчооойчйч m'entention | |
| ISP RAS | Moscou, Russie | Systèmes d'exploitation; matériel | Frama-C , Jessie , Why3 Astaver, Linux Kernel Library Fonctions Formalement vérifiées; SPIN/Promela , site Microtesk ; Event-B моделирование и Верифeveкация полититик безопасности управленbli. Spécification formelle Isabelle/HOL du noyau CAP9 |
| Kernkonzept gmbh | Allemagne | Systèmes d'exploitation | L4Re (source) |
| Kaspersky | Moscou, Russie | Sécurité / AV | ALLOY, TLA, Event-B (SOURCE), Ivory (SOURCE) |
| Machine Zone Inc. | Russie | Logiciel de jeu mobile, informatique en temps réel, réseau basé sur le cloud | TLA+ Twitter |
| Microsoft | Redmond, USA | Développement de logiciels | TLA+ TLA + Proomes, réflexion pour les programmeurs, spécifications TLA + de haut niveau pour les cinq niveaux de cohérence offerts par Azure Cosmos DB, Microsoft's Static Driver Verifier Analysis statique statique des pilotes de dispositifs Clousot Contracte Static Vérification de Microsoft |
| Mongodb | New York, États-Unis | Développement de logiciels | TLA+ TLA + SPEC d'une partie simplifiée du système de réplication MongoDB |
| NASA | USA | Espace | PVS Programme de recherche sur les méthodes formelles de la NASA Langley. JPF Java Pathfinder, Robust Software Engineering Group, Model Checking du Jet Propulsion Laboratory, SPIN/Promela Inspiring Applications of Spin, PVS (Source) |
| Laboratoires nomades | Paris, France | blockchain | Page Coq sur la vérification du logiciel |
| Oracle | Redwood Shores, CA, USA | Logiciel d'entreprise, cloud computing, matériel informatique | ACL2 (prouver des théorèmes sur Java et le JVM avec ACL2) |
| Logiciel particulier | TLA+ TLA + Spécifications pour NServiceBus | ||
| Pingcap | TLA+ tla + dans Tidb | ||
| Technologie de prover | Europe | Chemin de fer | Model checking |
| Rusbitech (рсбитех) | Russie, Moscou | Си | Frama-C , Event-B (моделированdent и Верифeveкция политиère безопасности управлеmuni |
| Rockwell Collins | États-Unis, Cedar Rapids, Iowa | Systèmes d'assurance élevée | Méthodes formelles dans l'industrie aérospatiale: suivez l'argent |
| Sérokell | Tallinn, Estonie | FinTech, blockchain, IoT, apprentissage automatique, vérification formelle | Agda |
| Synopsis | ? | ? | Site |
| Systerel | France | Logiciel, conseil, service | S3 Un vérificateur de modèle pour un langage synchrone, méthode B, événement-b / rodin. Recrutement. |
| Tamiser | États-Unis, région de la baie de San Francisco | Matériel | Coq LinkedIn |
| Boîte d'état | Amsterdam, Pays-Bas | Blockchain | Idris (github) |
| Sukhoi | Russie, Moscou | Aérospatial et défense | ANSYS SCADE Suite (Source - un compilateur officiellement vérifié pour Luster) |
| Thales | Frama-C (une approche de vérification formelle ascendante pour les critères communs certification: application à la machine virtuelle Javacard) | ||
| TrustInSoft | États-Unis, CA, San Francisco | - | Site TrustInSoft Analyzer |
| Systèmes dignes de confiance | Australie, Sydney | Isabelle/HOL , site Coq | |
| Deux six technologies | USA | Recherche de défense | Isabelle/HOL , vérification matérielle (exemple), Coq (exemple) |
| Recherche de Jet-Brains | Saint-Pétersbourg, Russie | - | Coq (source) |
| Ццц | Moscou, Russie | ? | SPIN/Promela методы и средства Верифeveкации протоколов когерентности па½ |
| Plate-forme T | Moscou, Russie | - | Coq , SPIN/Promela , TLA+ , McErlang , mCRL2 employé cv |
| Cern | Genève, Suisse | Logiciel de contrôle mCRL2 de l'expérience CMS au grand collisionneur de hadrons du CERN | |
| Yandex | Logiciel | Algorithme de réplication TLA+ Clickhouse, allocateur de mémoire sans verrouillage | |
| Zilliqa | Singapour | Blockchain | Projet Coq Scilla-Coq |
| Flots | Blockchain | ??? |
