practical fm
1.0.0
Se você vir uma empresa na lista que não existe mais ou não usa mais métodos formais, envie uma solicitação de tração com uma explicação. O mesmo acontece se você estiver trabalhando atualmente ou conhece uma empresa que usa métodos formais, mas não está na lista. Inclua o site, Github (se aplicável), locais e setor. Se a empresa estiver contratando, inclua um link para o anúncio.
| Nome | Localização | Setor | Fonte |
|---|---|---|---|
| Amazon | EUA | comércio eletrônico, computação em nuvem | TLA+ Como a Amazon Web Services usa métodos formais, uso de métodos formais no Amazon Web Services, CBMC Model Verificando o código de inicialização de data centers da AWS, Dafny AWS Encryption SDK |
| Airbus | França | Astrée : "In 2003, Astrée proved the absence of any runtime errors in the primary flight-control software of an Airbus model. The system's 132,000 lines of C code were analyzed completely automatically in only 80 minutes on a 2.8GHz 32-bit PC using 300MB of memory (and in only 50 minutes on an AMD Athlon 64 using 580MB of memory). Since then, Airbus France has been using Astrée in O desenvolvimento de software crítico de segurança para várias séries de planos, incluindo o A380. ", Coq (entrevista com Xavier Leroy), CAVEAT , um C-VERIFICADOR desenvolvido pela CEA e usado pela Airbus., Frama-C (uso industrial de um processo de engenharia de software formal e segura e eficiente em Avionics). | |
| Altran | França, Paris | SPARK colaboradores | |
| Maçã | Santa Clara Valley, Califórnia, EUA | Hardware e software | |
| Braço | Austin, Texas e San Jose, Califórnia, EUA | Hardware | ACL2 Verificação de hardware aritmético, verificando contra a especificação oficial do braço, kernel TLA+ Linux |
| Adacore | EUA, Nova York | ? | ? |
| Alacris | ? | Blockchain | |
| BAE Systems | Coq Reddit | ||
| Sistemas de rock | Boston & Bay Area, EUA; Berlim e Munique, Alemanha | Segurança de sistemas, computação confiável | Coq , C++ , github |
| A empresa da Boeing | EUA | Aeroespacial, Defesa | Coq (sem prova), Ivory (fonte) |
| Bosch | Alemanha | Automotivo | Astrée |
| Tecnologia Centaur | EUA | Hardware | ACL2 |
| Sistemas de engara | Austrália, Nova Gales do Sul, Sydney | Site | |
| Data61 | Austrália | Isabelle/HOL (o projeto de verificação Sel4) | |
| Draper | EUA | Defesa, espaço | Coq , Z3 |
| Ethereum | Suíça | Why3 Dev Update: Métodos formais, Isabelle/HOL a Lem Formalização de EVM e algumas provas de Isabelle/Hol, Verificação formal de Coq de contratos Ethereum | |
| ArdiSecurity | Software | Tamarin Wireguard | |
| Aprendizagem Espark | EUA, IL, Chicago | Educação | TLA+ Métodos formais na prática: Usando TLA+ no Espark Learning |
| Elástico | Global | Software de pesquisa e análise | TLA+ Isabelle/HOL ELASTICSECH-MODELS MODELOS Repositório Conferência de Conferência e Posições Abertas atuais |
| Agência Espacial Europeia | TLA+ (Desenvolvimento formal de um RTOS centrado em rede: 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+ ) | ||
| EUA | INFER em movimento rápido com verificação de software Zoncolan Como o Facebook usa análise estática para detectar e prevenir problemas de segurança | ||
| FireEye | Dresden, Alemanha (time extinto) | Segurança | Anúncio de trabalho Coq : engenheiro formal de métodos e desenvolvedor científico da FireEye |
| Barbatana | Rússia, SPB | Finanças (blockchain) | Coq , Agda |
| Terra formal | Global | Software | Verificação Coq da blockchain Tezos |
| Vindicações formais | Barcelona, Espanha | Lei | Software formalizado de DateTime Coq |
| Galois | Portland, Oregon, EUA | Consultoria/pesquisa | Coq (?) |
| Genua GmbH | Alemanha | CPAchecker Outro caminho para a qualidade do software? Verificação automatizada de software e OpenBSD e aplicação da verificação de software para os módulos de rede OpenBSD | |
| CA, EUA | Computação em nuvem, software de computador, IA | Coq (Código de alto nível simples para aritmética criptográfica-com provas, sem compromissos (cromo)), modelagem formal e análise da megaestore do Google em Maude em tempo real | |
| Grammatech | Anotações da biblioteca Frama-C C C no ACSL for Frama-C: Relatório de Experiência | ||
| Software Green Hills | EUA | Aeroespacial | ACL2 Uso industrial de ACL2 |
| Instituto Kestrel | EUA | Pesquisa em ciência da computação | Principalmente ACL2, alguns Isabelle/Hol, um pouco de Pvs e Coq. Consulte o site, principalmente páginas de projeto e páginas de pessoas, para obter detalhes e publicações. |
| IBM | EUA | ? | SPIN/Promela Paul E. McKenney's Journal, O que é RCU, fundamentalmente? (Linux Kernel, RCU), Coq Q*Cert |
| IgE+Xao | Europa | Design auxiliado por computador | Relatório de experiência Coq : O contrabando um pouco de coq dentro de um contexto de desenvolvimento de CAD Coq é usado para verificar o seguinte: (i) algoritmos específicos do domínio (aplicação de "patches" em documentos de design elétrico) (ii) algoritmos de grafos (PELVIMENTO) (PELRATURAÇÃO DE LIMURNA (LAYOUT DE PESQUISA DA LIMPEIRA, UNIDENTION-FILING, UNIDENTION-FIRIDADE (III) (stractures stractures, união-fuminagem, união-fuminagem, B&B Tsp, ...) (III) Structure Structure (inferência de tipo de idioma personalizado) (v) Projetos de pesquisa pequenos |
| Intel | EUA | Hardware | Prover (quinze anos de verificação formal da propriedade na Intel), HOL Light (verificação formal dos algoritmos da divisão IA-64), TLA+ (verificação formal pré-RTL: uma experiência Intel) |
| Sistemas informais | Toronto, Viena, Lausanne, Berlim | Blockchain, sistemas distribuídos | TLA+ Apalache, verificador de modelo simbólico para TLA+, consenso de BFT da TLA+ Rust e protocolo de comunicação interblockchain na ferrugem com especificações TLA+, testes baseados em modelo com TLA+ e Apalache |
| Infotecs | Rússia, Moscou | TLA+ , Coq , Construção e verificação formal de um algoritmo de exclusão mútua distribuído tolerante a falhas, пот sentido и и ииии litry ррре sentido. | |
| ISP Ras | Moscou, Rússia | Sistemas operacionais; hardware | Frama-C , Jessie , Why3 Astraver, Funções da Biblioteca do Kernel Linux formalmente verificadas; SPIN/Promela , site Microtesk ; Event-B модеел sentido и и и-b-BUS и и и и и и и-b и-bиццfiaя полин б в в в в-bииасосцц поцца ês Especificação formal de Isabelle/HOL do Kernel Cap9 |
| Kernkonzept GmbH | Alemanha | Sistemas operacionais | L4Re (fonte) |
| Kaspersky | Moscou, Rússia | Segurança/Av | Liga, TLA, Event-B (fonte), Ivory (fonte) |
| Machine Zone Inc. | Rússia | Software para jogos móveis, computação em tempo real, rede baseada em nuvem | TLA+ Twitter |
| Microsoft | Redmond, EUA | Desenvolvimento de software | TLA+ TLA+ Proofs, Thinking for Programmers, High-level TLA+ specifications for the five consistency levels offered by Azure Cosmos DB, Microsoft's Static Driver Verifier Thorough static analysis of device drivers Clousot Static contrace checking with Abstract Interpretation, Formal Methods and Tools for Distributed Systems, Formal Methods at Scale in Microsoft |
| MongoDB | Nova York, EUA | Desenvolvimento de software | TLA+ TLA+ Spec de uma parte simplificada do sistema de replicação do MongoDBB |
| NASA | EUA | Espaço | Programa de Pesquisa de Métodos Formais da NASA Langley PVS . JPF Java Pathfinder, Grupo Robusto de Engenharia de Software, Laboratório de Propulsão a Jato de Model Checking , Aplicações Inspiradoras de SPIN/Promela de Spin, PVS (Fonte) |
| Laboratórios nômades | Paris, França | Blockchain | Página Coq na verificação de software |
| Oráculo | Redwood Shores, CA, EUA | Software corporativo, computação em nuvem, hardware de computador | ACL2 (provando teoremas sobre Java e a JVM com ACL2) |
| Software particular | TLA+ TLA+ Especificações para NServiceBus | ||
| Pingcap | TLA+ tla+ em tidb | ||
| Tecnologia do Prover | Europa | Ferrovia | Model checking |
| Rusbitech (рссиfiaL) | Rússia, Moscou | Иfia | Frama-C , Event-B (Моделирование и верификация политик безопасности управления доступом в операционных системах) |
| Rockwell Collins | EUA, Cedar Rapids, Iowa | Sistemas de alta garantia | Métodos formais na indústria aeroespacial: siga o dinheiro |
| Serokell | Tallinn, Estônia | Fintech, blockchain, IoT, aprendizado de máquina, verificação formal | Agda |
| Sinopse | ? | ? | Site |
| Systel | França | Software, consultoria, serviço | S3 Um verificador de modelo para uma linguagem sincronizada, Método B, Event-B/Rodin. Recrutamento. |
| Sifive | EUA, área da baía de São Francisco | Hardware | Coq LinkedIn |
| StateBox | Amsterdã, Holanda | Blockchain | Idris (Github) |
| Sukhoi | Rússia, Moscou | Aeroespacial e Defesa | ANSYS SCADE Suite (fonte - um compilador formalmente verificado para o brilho) |
| Tales | Frama-C (uma abordagem de verificação formal de baixo para cima para certificação de critérios comuns: aplicação à máquina virtual Javacard) | ||
| Confiança | EUA, CA, São Francisco | - | Site TrustInSoft Analyzer |
| Sistemas confiáveis | Austrália, Sydney | Isabelle/HOL , site Coq | |
| Duas seis tecnologias | EUA | Pesquisa de defesa | Isabelle/HOL , verificação de hardware (exemplo), Coq (exemplo) |
| Pesquisa de Jetbrains | São Petersburgo, Rússia | - | Coq (fonte) |
| Ццт | Moscou, Rússia | ? | SPIN/Promela |
| T-plataforms | Moscou, Rússia | - | Coq , SPIN/Promela , TLA+ , McErlang , mCRL2 Funcionário CV |
| CERN | Genève, Suíça | Software de controle mCRL2 do experimento CMS no Large Hadron Collider do CERN | |
| Yandex | Software | Algoritmo de replicação TLA+ clickhouse, alocador de memória sem bloqueio | |
| Zilliqa | Cingapura | Blockchain | Projeto Coq Scilla-Coq |
| Ondas | Blockchain | ??? |
