practical fm
1.0.0
Если вы видите компанию в списке, которая больше не существует, или больше не использует формальные методы, отправьте запрос на привлечение с объяснением. То же самое касается, если вы сейчас работаете или знаете компанию, которая использует формальные методы, но не в списке. Пожалуйста, включите веб -сайт, Github (если применимо), местоположения и сектор. Если компания нанимает, включите ссылку на объявление.
| Имя | Расположение | Сектор | Источник |
|---|---|---|---|
| Амазонка | США | Электронная коммерция, облачные вычисления | TLA+ Как Amazon Web Services использует формальные методы, использование формальных методов в Amazon Web Services, CBMC Проверка загрузочного кода из центров обработки данных AWS, Dafny AWS Encryption SDK |
| Airbus | Франция | Astrée : «В 2003 году Astrée доказала отсутствие каких-либо ошибок времени выполнения в первичном программном обеспечении полета модели Airbus. 132 000 строк C кода C были полностью проанализированы только за 80 минут на 32-гг 32-битном ПК с использованием AMD Athlon 64, используя 580mb of Memory, с тех пор, используя Amd Athlon 64. Разработка критического программного обеспечения для безопасности для различных серий плоскостей, включая A380 »., Coq (интервью с Ксавьером Лерой), CAVEAT , C-проверки, разработанный CEA и используемый Airbus., Frama-C (промышленное использование безопасного и эффективного формального процесса разработки программного обеспечения на основе методов в авионике). | |
| Альтран | Франция, Париж | SPARK Spark Apportors | |
| Яблоко | Вэлли Санта -Клара, Калифорния, США | Аппаратное и программное обеспечение | |
| Рука | Остин, Техас и Сан -Хосе, Калифорния, США | Аппаратное обеспечение | Проверка арифметического оборудования ACL2 , проверка на официальную спецификацию рук, ядро TLA+ Linux |
| Адакор | США, Нью -Йорк | ? | ? |
| Алакрис | ? | Блокчейн | |
| BAE Systems | Coq Reddit | ||
| Системы коренных пород | Boston & Bay Area, США; Берлин и Мюнхен, Германия | Системная безопасность, достойный вычисление | Coq , C++ , GitHub |
| Boeing Company | США | Аэрокосмическая, защита | Coq (без доказательств), Ivory (источник) |
| Бош | Германия | Автомобиль | Astrée |
| Технология Кентавра | США | Аппаратное обеспечение | ACL2 |
| Cog Systems | Австралия, Новый Южный Уэльс, Сидней | Сайт | |
| Data61 | Австралия | Isabelle/HOL (проект проверки SEL4) | |
| Дрэпер | США | Защита, пространство | Coq , Z3 |
| Ethereum | Швейцария | Why3 Обновление Dev: формальные методы, формализация EVM EVM Isabelle/HOL A и некоторых доказательств Isabelle/HOL, формальная проверка Coq Ethereum Contrics | |
| Щинка безопасности | Программное обеспечение | Tamarin Wireguard | |
| Espark Learning | США, Иллинойс, Чикаго | Образование | TLA+ Формальные методы на практике: Использование TLA+ At Espark Learning |
| Эластичный | Глобальный | Программное обеспечение для поиска и аналитики | TLA+ Isabelle/HOL Elasticsearch-Formal-Models Conference Conference Conference и текущие открытые позиции |
| Европейское космическое агентство | TLA+ (Формальное развитие сетевого ориентированного RTO: 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 | Финансы (блокчейн) | Coq , Agda |
| Формальная земля | Глобальный | Программное обеспечение | Coq проверка блокчейна Tezos |
| Формальные оправдания | Барселона, Испания | Закон | Coq Formalized DateTime Software |
| Галуа | Портленд, Орегон, США | Консультация/исследования | Coq (?) |
| Genua Gmbh | Германия | CPAchecker еще один путь для качества программного обеспечения? Автоматизированная проверка программного обеспечения и OpenBSD и применение программного обеспечения Verificationto OpenBSD сетевые модули | |
| CA, США | Облачные вычисления, компьютерное программное обеспечение, искусственное искусство | Coq (простой высокоуровневый код для криптографической арифметики-с доказательствами, без компромиссов (хромиум)), формальное моделирование и анализ Megastore Google в Моде в режиме реального времени | |
| Грамматх | Аннотации библиотеки Frama-C C в ACSL для FRAMA-C: Experience Report | ||
| Программное обеспечение Green Hills | США | Аэрокосмическая | ACL2 промышленное использование ACL2 |
| Институт Kestrel | США | Исследование компьютерных наук | В основном ACL2, некоторые Изабель/HOL, немного PVS и COQ. Смотрите веб -сайт, особенно страницы проектов и страницы людей, для деталей и публикаций. |
| IBM | США | ? | SPIN/Promela Пол Э. МакКенни Журнал, что такое RCU, принципиально? (Linux kernel, rcu), Coq q*cert |
| Ige+Xao | Европа | Компьютерный дизайн | Отчет об опыте Coq : контрабанда немного COQ в контексте разработки CAD Coq Coq используется для проверки следующего: (i) алгоритмы специфичных для домена (применение «патчей» к электрическим дизайнерским документам) (ii) Алгоритмы графиков (A* Поиск, склады по обеспечению длины, приоритет (B & B TSP, ... III). Вывод типа языка) (v) Небольшие исследовательские проекты |
| Intel | США | Аппаратное обеспечение | Prover (пятнадцать лет проверки формальной собственности в Intel), HOL Light (формальная проверка алгоритмов деления IA-64), TLA+ (Pre-RTL Формальная проверка: опыт Intel) |
| Неформальные системы | Торонто, Вена, Лозанна, Берлин | Блокчейн, распределенные системы | TLA+ APALACHE, символическая проверка модели для TLA+, Rust Tenermint BFT Consensus и протокол связи между блубкхайн |
| Infotecs | Россия, Москва | TLA+ , Coq , строительство и формальная проверка распределенного алгоритма взаимного исключения, то есть | |
| ISP RAS | Москва, Россия | Операционные системы; аппаратное обеспечение | Frama-C , Jessie , Why3 Astraver, библиотека ядра Linux формально проверено; SPIN/Promela , Microtesk Site; Event-B и Верикаика в политии Формальная спецификация Isabelle/HOL ядра CAP9 |
| Kernkonzept Gmbh | Германия | Операционные системы | L4Re (источник) |
| Касперский | Москва, Россия | Безопасность/AV | Сплав, TLA, Event-B (источник), Ivory (источник) |
| Machine Zone Inc. | Россия | Программное обеспечение для мобильных игр, компьютерные компьютеры в реальном времени, облачные сети | TLA+ Twitter |
| Microsoft | Редмонд, США | Разработка программного обеспечения | TLA+ TLA+ доказательства, мышление для программистов, высокие уровни TLA+ спецификации для пяти уровней согласованности, предлагаемых Azure Cosmos DB, тщательный статический анализ драйверов устройств, статические напроки, с помощью формальных методов и инструментов для распределенных систем, формальные методы в Clousot Microsoft's Static Driver Verifier с помощью абстрактной интерпретации, формальных методов и инструментов для распределенных систем, формальных методов в масштабах в Microsoft. |
| Mongodb | Нью -Йорк, США | Разработка программного обеспечения | TLA+ TLA+ SPEC упрощенной части системы репликации MongoDB |
| НАСА | США | Космос | PVS NASA LANGLEY FORAL MEDITION Программа исследования. JPF Java Pathfinder, надежная группа разработчиков программного обеспечения, Лаборатория Model Checking реактивного движения, вдохновляющие приложения Spin, PVS (источник) SPIN/Promela , PVS (Source) |
| Кочевые лаборатории | Париж, Франция | блокчейн | Страница Coq по проверке программного обеспечения |
| Оракул | Редвуд Шорс, Калифорния, США | Корпоративное программное обеспечение, облачные вычисления, компьютерное оборудование | ACL2 (доказывание теорем о Java и JVM с ACL2) |
| Конкретное программное обеспечение | TLA+ TLA+ спецификации для nservicebus | ||
| Пингкап | TLA+ tla+ в tidb | ||
| Проверка технологии | Европа | Железная дорога | Model checking |
| Rusbitech (rusbioteх) | Россия, Москва | Системно | Frama-C , Event-B (Моделировани и Верикахия в поэлике |
| Роквелл Коллинз | США, Сидар -Рапидс, Айова | Системы высокой уверенности | Формальные методы в аэрокосмической промышленности: следуйте деньгам |
| Серокелл | Таллинн, Эстония | Fintech, блокчейн, IoT, машинное обучение, формальная проверка | Agda |
| Синопсис | ? | ? | Сайт |
| Систерия | Франция | Программное обеспечение, консалтинг, сервис | S3 Проверка моделя для синхронного языка, метод B, Event-B/Rodin. Рекрутинг. |
| Просмотр | США, район залива Сан -Франциско | Аппаратное обеспечение | Coq LinkedIn |
| Statebox | Амстердам, Нидерланды | Блокчейн | Idris (GitHub) |
| Sukhoi | Россия, Москва | Аэрокосмическая и защита | ANSYS SCADE Suite (источник - формально проверенный компилятор для блеска) |
| Фалес | Frama-C (подход к формальной проверке снизу вверх для общих критериев Сертификация: применение на виртуальную машину JavaCard) | ||
| Trustinsoft | США, Калифорния, Сан -Франциско | - | Сайт TrustInSoft Analyzer |
| Заслуживающие доверия системы | Австралия, Сидней | Isabelle/HOL , Coq сайт | |
| Две шесть технологий | США | Оборонные исследования | Isabelle/HOL , Аппаратная проверка (пример), Coq (пример) |
| Jetbrains Research | Сент -Петербург, Россия | - | Coq (источник) |
| Мгт | Москва, Россия | ? | SPIN/Promela -korentnotnosti |
| Т-платформы | Москва, Россия | - | Coq , SPIN/Promela , TLA+ , McErlang , mCRL2 сотрудников CV |
| CERN | Дженер, Швейцария | Программное обеспечение для управления mCRL2 эксперимента CMS в крупном адронном коллайдере CERN | |
| Яндекс | Программное обеспечение | Алгоритм репликации TLA+ Clickhouse, распределение памяти без блокировки | |
| Zilliqa | Сингапур | Блокчейн | Coq Scilla-Coq Project |
| Волны | Блокчейн | ??? |
