8000 GitHub - tdi/practical-fm: A gently curated list of companies using verification formal methods in industry
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

tdi/practical-fm

BranchesTags
 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

25 Commits
README.md
README.md
 
 

Repository files navigation

A List of companies that use formal verification methods in software engineering

If you see a company on the list that doesn't exist anymore, or does not use formal methods anymore, please send a pull request with an explanation. The same goes if you're currently working at, or know a company that uses formal methods but is not on the list. Please include the website, github (if applicable), locations, and sector. If the company is hiring please include a link to the ad.

Name Location Sector Source
Amazon USA eCommerce, Cloud computing TLA+ How Amazon Web Services Uses Formal Methods, Use of Formal Methods at Amazon Web Services
Airbus France Astr ́ee, Coq Interview with Xavier Leroy
Altran France, Paris SPARK SPARK contributors
Apple Santa Clara Valley, California, USA Hardware and Software
ARM USA, California, San Jose Hardware Verifying against the official ARM specification, TLA+ Linux Kernel
AdaCore USA, New York ? ?
BAE Systems Coq Reddit
The Boeing Company USA Aerospace, Defense Coq (no proof)
Centaur Technology USA Hardware ACL2
Cog Systems Australia, New South Wales, Sydney Site
Data61 Australia Isabelle/HOL (seL4)
Ethereum Switzerland Why3 Dev Update: Formal Methods, Isabelle/HOL A Lem formalization of EVM and some Isabelle/HOL proofs, Coq Formal Verification of Ethereum Contracts
eSpark Learning USA, IL, Chicago Education TLA+ Formal Methods in Practice: Using TLA+ at eSpark Learning
Elastic Global Search & analytics software TLA+ Isabelle/HOL elasticsearch-formal-models repository conference talk and current open positions
Facebook USA INFER Moving Fast with Software Verification
FireEye Dresden, Germany (team defunct) Security Coq Job announcement: formal methods engineer and scientific developer at FireEye
Galois Portland, Oregon, USA Consulting/Research Coq (?)
Grammatech Frama-C C Library annotations in ACSL for Frama-C: experience report
Green Hills Software USA Aerospace ACL2 Industrial Use of ACL2
IBM USA ? SPIN/Promela Paul E. McKenney's Journal, What is RCU, Fundamentally? (Linux Kernel, RCU)
Intel USA Hardware [Fifteen Years of Formal Property Verification in Intel]q(https://link.springer.com/chapter/10.1007%2F978-3-540-69850-0_8?LI=true)
InfoTecs Russia, Moscow TLA+, Coq, Construction and formal verification of a fault-tolerant distributed mutual exclusion algorithm, Построение и верификация отказоустойчивого алгоритма распределенной блокировки
ISP RAS Moscow, Russia Operating systems; hardware Frama-C, Jessie, Why3 Astraver; SPIN/Promela, Microtesk Site
Kernkonzept Germany Operating systems Site
Kaspersky Lab Moscow, Russia Security/AV Что представляет собой операционная система Kaspesky OS?
Machine Zone Inc. Russia Mobile gaming software, Real-time computing, Cloud-based networking TLA+ Twitter
Microsoft Redmond, USA Software development 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
MongoDB New York, USA Software development TLA+ TLA+ Spec of a simplified part of MongoDB replication system
NASA USA Space PVS NASA Langley Formal Methods Research Program. JPF Java Pathfinder. Robust Software Engineering Group.
PingCAP TLA+ TLA+ in TiDB
Rockwell Collins USA, Cedar Rapids, Iowa High Assurance Systems ?
Synopsis ? ? Site
SiFive USA, San Francisco Bay Area Hardware Coq LinkedIn
TrustInSoft USA, CA, San Francisco - TrustInSoft Analyzer Site
Trustworthy Systems Australia, Sydney Isabelle/HOL, Coq Site
JetBrains Saint Petersburg, Russia - Site
МЦСТ Moscow, Russia ? SPIN/Promela Методы и средства верификации протоколов когерентности памяти
T-Platforms Moscow, Russia - Coq, SPIN/Promela, TLA+, McErlang, mCRL2 Employee CV
CERN Genève, Switzerland mCRL2 Control Software of the CMS Experiment at CERN’s Large Hadron Collider
Ziliqa ? Blockchain Coq

See also

About

A gently curated list of companies using verification formal methods in industry

Resources

Readme
Activity

Stars

0 stars

Watchers

1 watching

Forks

0 forks
Report repository

Releases

No releases published

Packages

No packages published
0