practical fm
1.0.0
Si ve una empresa en la lista que ya no existe, o ya no usa métodos formales, envíe una solicitud de extracción con una explicación. Lo mismo ocurre si actualmente está trabajando o conoce a una empresa que usa métodos formales pero no está en la lista. Incluya el sitio web, GitHub (si corresponde), ubicaciones y sector. Si la empresa está contratando, incluya un enlace al anuncio.
| Nombre | Ubicación | Sector | Fuente |
|---|---|---|---|
| Amazonas | EE.UU | comercio electrónico, computación en la nube | TLA+ Cómo Amazon Web Services utiliza métodos formales, el uso de métodos formales en Amazon Web Services, CBMC Modelo Comprobando el código de arranque de AWS Data Centers, Dafny AWS Cicryption SDK |
| Aerobús | Francia | Astrée : "En 2003, Astrée demostró la ausencia de cualquier error de tiempo de ejecución en el software primario de control de vuelo de un modelo AirBus. Las 132,000 líneas de código C del sistema se analizaron completamente automáticamente en solo 80 minutos en una PC de 2.8GHz 32 bits utilizando 300MB de memoria (y en solo 50 minutos en un AMD Athlon 64 utilizando 580MB de la memoria). El desarrollo del software crítico de seguridad para varias series de aviones, incluida la A380 ", Coq (entrevista con Xavier Leroy), CAVEAT , un verificador C desarrollado por CEA y utilizado por Airbus., Frama-C (uso industrial de un proceso de ingeniería de software formal de software basado en métodos formales seguros y eficientes). | |
| Altrano | Francia, París | Colaboradores de SPARK Spark | |
| Manzana | Valle de Santa Clara, California, EE. UU. | Hardware y software | |
| Brazo | Austin, Texas y San José, California, EE. UU. | Hardware | Verificación de ACL2 de hardware aritmético, verificando la especificación oficial del brazo, TLA+ Linux Kernel |
| Adacore | Estados Unidos, Nueva York | ? | ? |
| Alacris | ? | Cadena de bloques | |
| Sistemas BAE | Coq Reddit | ||
| Sistemas de roca madre | Boston & Bay Area, EE. UU.; Berlín y Munich, Alemania | Seguridad de sistemas, cómputo confiable | Coq , C++ , Github |
| La empresa boeing | EE.UU | Aeroespacial, defensa | Coq (sin prueba), Ivory (fuente) |
| Bosch | Alemania | Automotor | Astrée |
| Tecnología de centauro | EE.UU | Hardware | ACL2 |
| Sistemas de dientes | Australia, Nueva Gales del Sur, Sydney | Sitio | |
| Data61 | Australia | Isabelle/HOL (el proyecto de verificación SEL4) | |
| Pañero | EE.UU | Defensa, espacio | Coq , Z3 |
| Ethereum | Suiza | Why3 Dev actualización: Métodos formales, Isabelle/HOL A Lem Formalización de EVM y algunas pruebas de Isabelle/Hol, Coq Verificación formal de contratos de Ethereum | |
| Seguridad en el bosque | Software | Tamarin wireguard | |
| aprendizaje de espark | Estados Unidos, IL, Chicago | Educación | TLA+ Métodos formales en la práctica: Uso de TLA+ en Espark Learning |
| Elástico | Global | Software de búsqueda y análisis | TLA+ Isabelle/HOL Elasticsearch-formal-Models Repository Conference Talk y puestos abiertos actuales |
| Agencia Espacial Europea | TLA+ (Desarrollo formal de un RTOS centrado en la red: 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+ )) | ||
| EE.UU | INFER moviéndose rápido con verificación de software Zoncolan Cómo Facebook usa el análisis estático para detectar y prevenir problemas de seguridad | ||
| Fusey | Dresden, Alemania (equipo difunto) | Seguridad | Anuncio de trabajo Coq : ingeniero de métodos formales y desarrollador científico en FireEye |
| A prueba de aletas | Rusia, SPB | Finanzas (blockchain) | Coq , Agda |
| Tierra formal | Global | Software | VERIFICACIÓN Coq DE LA TEZOS BLOCHSTAIN |
| Reivindicaciones formales | Barcelona, España | Ley | Software de fecha y hora formalizado de Coq |
| Galois | Portland, Oregon, EE. UU. | Consultoría/investigación | Coq (?) |
| genua gmbh | Alemania | CPAchecker otra ruta para la calidad del software? Verificación automatizada de software y OpenBSD y aplicación de verificación de software para OpenBSD Módulos de red | |
| CA, EE. UU. | Computación en la nube, software de computadora, AI | Coq (código simple de alto nivel para la aritmética criptográfica: con pruebas, sin compromisos (cromo)), modelado formal y análisis de la megastore de Google en el maude en tiempo real | |
| Gramatecha | Anotaciones de la biblioteca Frama-C C en ACSL para Frama-C: Informe de experiencia | ||
| Software de Green Hills | EE.UU | Aeroespacial | ACL2 Uso industrial de ACL2 |
| Instituto Kestrel | EE.UU | Investigación de Ciencias de la Computación | Principalmente ACL2, algunos Isabelle/Hol, un poco de PVS y COQ. Consulte el sitio web, particularmente páginas de proyectos y páginas de personas, para obtener detalles y publicaciones. |
| IBM | EE.UU | ? | SPIN/Promela Paul E. McKenney's Journal, ¿Qué es RCU, fundamentalmente? (Linux Kernel, RCU), Coq Q*Cert |
| IGE+xao | Europa | Diseño asistido por computadora | Informe de experiencia Coq : el contrabando un poco de COQ dentro de un contexto de desarrollo de CAD COQ se utiliza para verificar los siguientes: (i) Algoritmos específicos del dominio (aplicación de "parches" a documentos de diseño eléctrico) (ii) Algoritmos gráficos (A* búsqueda, diseño de árbol de longitud de longitud, B & B Tsp, ...) (iii) Estructuras de datos (sindical-FIND, Priority QueeUs, ... (Iv) (IV) (Iv) (Iv). Inferencia de tipo de idioma) (v) Proyectos de investigación pequeños |
| Intel | EE.UU | Hardware | Prover (quince años de verificación de propiedad formal en Intel), HOL Light (verificación formal de algoritmos de división IA-64), TLA+ (verificación formal pre-rtl: una experiencia Intel) |
| Sistemas informales | Toronto, Viena, Lausana, Berlín | Blockchain, sistemas distribuidos | TLA+ apalache, verificador de modelos simbólicos para TLA+, consenso BFT de Rust y protocolo de comunicación interblockchain en óxido con especificaciones TLA+, pruebas basadas en modelos con TLA+ y apalacheache y apalache |
| Infotecs | Rusia, Moscú | TLA+ , Coq , construcción y verificación formal de un algoritmo de exclusión mutua distribuida tolerante a fallas, пострetro umen | |
| ISP Ras | Moscú, Rusia | Sistemas operativos; hardware | Frama-C , Jessie , Why3 Astraver, Linux Kernel Library Functions Formalmente verificadas; SPIN/Promela , sitio Microtesk ; Event-B мделирование и верификация политик безопаículos Isabelle/HOL del núcleo Cap9 |
| Kernkonzept gmbh | Alemania | Sistemas operativos | L4Re (fuente) |
| Kaspersky | Moscú, Rusia | Seguridad/AV | Aleación, tla, Event-B (fuente), Ivory (fuente) |
| Machine Zone Inc. | Rusia | Software de juego móvil, informática en tiempo real, redes basadas en la nube | TLA+ Twitter |
| Microsoft | Redmond, EE. UU. | Desarrollo de software | TLA+ TLA+ Pruebas, pensamiento para programadores, especificaciones de TLA+ de alto nivel para los cinco niveles de consistencia ofrecidos por Azure Cosmos DB, Microsoft's Static Driver Verifier Completador estático de los controladores de dispositivos Contralación Clousot de la verificación con la interpretación abstracta, los métodos formales y las herramientas para sistemas distribuidos, métodos formales a escala en microsoft |
| Mongodb | Nueva York, EE. UU. | Desarrollo de software | TLA+ TLA+ Spec de una parte simplificada del sistema de replicación de MongoDB |
| NASA | EE.UU | Espacio | PVS Programa de investigación de métodos formales de PVS Langley. JPF Java Pathfinder, Robust Software Engineering Group, Laboratorio de propulsión de chorro Model Checking , aplicaciones inspiradoras de SPIN/Promela de Spin, PVS (fuente) |
| Laboratorios nómadas | París, Francia | cadena de bloques | Página Coq sobre verificación de software |
| Oráculo | Redwood Shores, CA, EE. UU. | Software empresarial, computación en la nube, hardware de computadora | ACL2 (teoremas de prueba sobre Java y el JVM con ACL2) |
| Software particular | TLA+ TLA+ Especificaciones para nservicebus | ||
| Pingcap | TLA+ TLA+ en TIDB | ||
| Tecnología prover | Europa | Ferrocarril | Model checking |
| Rusbitech (русбитех) | Rusia, Moscú | Сис regalo | Frama-C , Event-B (мделирование и верификациimo политик безопаículos |
| Rockwell Collins | Estados Unidos, Cedar Rapids, Iowa | Sistemas de alta garantía | Métodos formales en la industria aeroespacial: siga el dinero |
| Serokell | Tallinn, Estonia | Fintech, blockchain, IoT, aprendizaje automático, verificación formal | Agda |
| Sinopsis | ? | ? | Sitio |
| Systerel | Francia | Software, consultoría, servicio | S3 Un verificador de modelos para un lenguaje de sincrono, método B, Event-B/Rodin. Reclutamiento. |
| Guarda | EE. UU., Área de la Bahía de San Francisco | Hardware | Coq LinkedIn |
| Caja de estado | Amsterdam, Países Bajos | Cadena de bloques | Idris (Github) |
| Sukhoi | Rusia, Moscú | Aeroespacial y defensa | ANSYS SCADE Suite (fuente: un compilador formalmente verificado para brillo) |
| Tales | Frama-C (un enfoque de verificación formal ascendente para la certificación de criterios comunes: aplicación a la máquina virtual de Javacard) | ||
| Trustinsoft | Estados Unidos, CA, San Francisco | - | Sitio TrustInSoft Analyzer |
| Sistemas confiables | Australia, Sydney | Isabelle/HOL , sitio Coq | |
| Dos seis tecnologías | EE.UU | Investigación de defensa | Isabelle/HOL , Verificación de hardware (ejemplo), Coq (ejemplo) |
| Investigación de JetBrains | San Petersburgo, Rusia | - | Coq (fuente) |
| Ц ц | Moscú, Rusia | ? | SPIN/Promela |
| T-Platforms | Moscú, Rusia | - | Coq , SPIN/Promela , TLA+ , McErlang , mCRL2 Empleado CV CV |
| Sargento | Genève, Suiza | Software de control mCRL2 del experimento CMS en el gran colider de hadrones de CERN | |
| Yandex | Software | Algoritmo de replicación TLA+ Clickhouse, asignador de memoria sin bloqueo | |
| Zilliqa | Singapur | Cadena de bloques | Proyecto Coq Scilla-Coq |
| Ondas | Cadena de bloques | ???? |
