practical fm
1.0.0
Wenn Sie ein Unternehmen auf der Liste sehen, das nicht mehr vorhanden ist oder keine formellen Methoden mehr verwendet, senden Sie bitte eine Pull -Anfrage mit einer Erklärung. Gleiches gilt für Sie, wenn Sie derzeit an der Liste arbeiten oder ein Unternehmen kennen, das formelle Methoden verwendet, aber nicht auf der Liste steht. Bitte geben Sie die Website, GitHub (falls zutreffend), Standorte und Sektor an. Wenn das Unternehmen anstellt, fügen Sie bitte einen Link zur Anzeige hinzu.
| Name | Standort | Sektor | Quelle |
|---|---|---|---|
| Amazonas | USA | E -Commerce, Cloud Computing | TLA+ Wie Amazon Web Services formelle Methoden, Verwendung formaler Methoden bei Amazon Web Services und CBMC -Modellprüfungs -Boot -Code von AWS Data Centers, Dafny AWS -Verschlüsselung SDK verwendet |
| Airbus | Frankreich | Astrée : "Im Jahr 2003 bewies Astée das Fehlen von Laufzeitfehlern in der primären Flugkontrollsoftware eines Airbus-Modells. Die 132.000 Zeilen des C-Codes des Systems wurden in nur 80 Minuten in nur 80 Minuten auf einem 2,8-GHz-32-Bit-PC mit 300 MB Memory vollständig automatisch analysiert. Bei der Entwicklung CAVEAT Sicherheits-Kritischen Software für verschiedene Ebenenreihen, Coq des Frama-C . | |
| Altran | Frankreich, Paris | SPARK Spark -Mitwirkende | |
| Apfel | Santa Clara Valley, Kalifornien, USA | Hardware und Software | |
| Arm | Austin, Texas, & San Jose, Kalifornien, USA | Hardware | ACL2 -Überprüfung der arithmetischen Hardware und Überprüfung der offiziellen ARM -Spezifikation, TLA+ Linux -Kernel |
| Adacore | USA, New York | ? | ? |
| Alacris | ? | Blockchain | |
| BAE -Systeme | Coq Reddit | ||
| Grundgesteinssysteme | Boston & Bay Area, USA; Berlin & München, Deutschland | Systemsicherheit, vertrauenswürdiger Berechnung | Coq , C++ , GitHub |
| Die Boeing Company | USA | Luft- und Raumfahrt, Verteidigung | Coq (kein Beweis), Ivory (Quelle) |
| Bosch | Deutschland | Automobil | Astée |
| Centaur -Technologie | USA | Hardware | ACL2 |
| Zahnradsysteme | Australien, New South Wales, Sydney | Website | |
| Daten61 | Australien | Isabelle/HOL (das SEL4 -Verifizierungsprojekt) | |
| Draper | USA | Verteidigung, Raum | Coq , Z3 |
| Ethereum | Schweiz | Why3 -Dev -Update: Formale Methoden, Isabelle/HOL a lem Formalisierung von EVM und einigen Isabelle/HOL -Proofs, Coq -Formale Überprüfung der Ethereum -Verträge | |
| REDGECURITY | Software | Tamarin WireGuard | |
| Espark Lernen | USA, IL, Chicago | Ausbildung | TLA+ formale Methoden in der Praxis: Verwendung von TLA+ bei Espark Learning |
| Elastisch | Global | Such- und Analyse -Software | TLA+ Isabelle/HOL Elasticsearch-Formal-Modelle Repository Conference Talk und aktuelle offene Positionen |
| Europäische Weltraumagentur | TLA+ (formelle Entwicklung eines netzwerkzentrierten RTOs: 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 Sie mit Software -Überprüfung Zoncolan , wie Facebook statische Analysen verwendet, um Sicherheitsprobleme zu erkennen und zu verhindern | ||
| Fireeye | Dresden, Deutschland (Team Definct) | Sicherheit | Coq -Jobankündigung: formelle Methodeningenieur und wissenschaftlicher Entwickler bei Fireyeye |
| Feindlich | Russland, SPB | Finanzen (Blockchain) | Coq , Agda |
| Formelles Land | Global | Software | Coq -Überprüfung der Tezos -Blockchain |
| Formelle Rechtfertigung | Barcelona, Spanien | Gesetz | Coq Formalisierte DateTime -Software |
| Galois | Portland, Oregon, USA | Beratung/Forschung | Coq (?) |
| Genua Gmbh | Deutschland | CPAchecker Ein weiterer Weg für die Softwarequalität? Automatisierte Softwareverifizierung und OpenBSD sowie Anwendung von Software -Verifizierung von OpenBSD -Netzwerkmodulen | |
| CA, USA | Cloud Computing, Computersoftware, KI | Coq (einfacher hoher Code für kryptografische Arithmetik | |
| Grammatech | Frama-C C-Bibliothek Anmerkungen in ACSL für Frama-C: Erfahrungbericht | ||
| Software Green Hills | USA | Luft- und Raumfahrt | ACL2 Industrielle Verwendung von ACL2 |
| Kestrel Institute | USA | Informatikforschung | Meistens ACL2, einige Isabelle/Hol, ein wenig PVS und Coq. Weitere Informationen und Veröffentlichungen finden Sie auf der Website, insbesondere der Projektseiten und der Personenseiten. |
| IBM | USA | ? | SPIN/Promela Paul E. McKenney's Journal, was ist RCU grundsätzlich? (Linux Kernel, RCU), Coq Q*cert |
| Ige+xao | Europa | Computergestütztes Design | Coq -Erlebnisbericht: Das Schmuggel ein wenig CoQ innerhalb eines CAD-Entwicklungskontexts COQ wird verwendet, um Folgendes zu verifizieren: (i) domänenspezifische Algorithmen (Anwendung von "Patches" auf elektrische Designdokumente) (ii) Graph-Algorithmen (A* -Such, Länge-Präsen-Baum-Layout, B & B TSP, ...) (III) -Datenstrukturen (Gewerkschafts-Find-Findfind, Prioritäts-Progres, progressive Strukturen, Prioritäts-Messen, Prioritäts-Messen, progressive, progressive Strukturen (Gewerkschafts-Finddaten, Prioritäts-Messen, progressiven progressiven progressive strukturell-, progressive progreshy-struktur-struktur- (findfinddaten-, priorital-ques-struktur- (Benutzerdefinierte Sprachtyp Inferenz) (v) Kleine Forschungsprojekte |
| Intel | USA | Hardware | Prover (fünfzehn Jahre formale Eigentumsüberprüfung in Intel), HOL Light (formale Überprüfung der IA-64-Divisionalgorithmen), TLA+ (Vor-RTL-formelle Überprüfung: Eine Intel-Erfahrung) |
| Informelle Systeme | Toronto, Wien, Lausanne, Berlin | Blockchain, verteilte Systeme | TLA+ Apalache, symbolische Modellprüfung für TLA+, Rust Tendermint BFT -Konsens und Kommunikationsprotokoll für InterblockChain in Rost mit TLA+ -Paten, modellbasierten Tests mit TLA+ und Apalache |
| Infotecs | Russland, Moskau | TLA+ , Coq , Konstruktion und formale Überprüfung eines verteilten gegenseitigen Ausgrenzungsalgorithmus für verteilte Verteilte, построение и в рикация от & ззззз & тbehark | |
| Isp Ras | Moskau, Russland | Betriebssysteme; Hardware | Frama-C , Jessie , Why3 Astaver, Linux-Kernel-Bibliotheksfunktionen formell verifiziert; SPIN/Promela , Microtesk Site; Event-B моделирование и и верикация политик беззасности уравления доступо о оераных сersöns ди & д д & м м д & м м м д х х х х х х х х х х х х х х х х х х х х х х х х х х х х х х х х х х х х х х х х х х,, Isabelle/HOL formale Spezifikation des Cap9 -Kernels |
| Kernkonzept GmbH | Deutschland | Betriebssysteme | L4Re (Quelle) |
| Kaspersky | Moskau, Russland | Sicherheit/av | Legierung, TLA, Event-B (Quelle), Ivory (Quelle) |
| Maschinenzone Inc. | Russland | Mobile Gaming-Software, Echtzeit-Computing, Cloud-basierte Netzwerke | TLA+ Twitter |
| Microsoft | Redmond, USA | Softwareentwicklung | TLA+ TLA+ Proofs, Denken für Programmierer, hochgradige TLA+ -Pezifikationen für die fünf Konsistenzniveaus, die von Azure Cosmos DB angeboten werden, Microsoft's Static Driver Verifier gründlicher statischer Analyse von Geräte Treiber Clousot statische Verhütung mit abtrakten Interpretationen, formal |
| MongoDb | New York, USA | Softwareentwicklung | TLA+ TLA+ Spezifikation eines vereinfachten Teils des MongoDB -Replikationssystems |
| NASA | USA | Raum | PVS NASA LANGLEY FORTRAG METHODEN FORSCHUNGSPROGRAMM. JPF Java Pathfinder, robuste Software -Engineering -Gruppe, Model Checking Jet Propulsion Laboratory, SPIN/Promela Inspirierende Anwendungen von Spin, PVS (Quelle) |
| Nomadische Labors | Paris, Frankreich | Blockchain | Coq -Seite zur Softwareüberprüfung |
| Orakel | Redwood Shores, CA, USA | Enterprise -Software, Cloud Computing, Computerhardware | ACL2 (Beweise für Java und die JVM mit ACL2) |
| Bestimmte Software | TLA+ TLA+ Spezifikationen für Nservicebus | ||
| Pingcap | TLA+ TLA+ in TIDB | ||
| Prover -Technologie | Europa | Eisenbahn | Model checking |
| Rusbitech (русбитех) | Russland, Moskau | С morgen по по | Frama-C , Event-B (моделированmaß |
| Rockwell Collins | USA, Cedar Rapids, Iowa | Hohe Versicherungssysteme | Formale Methoden in der Luft- und Raumfahrtindustrie: Befolgen Sie das Geld |
| Serokell | Tallinn, Estland | Fintech, Blockchain, IoT, maschinelles Lernen, formale Überprüfung | Agda |
| Zusammenfassung | ? | ? | Website |
| Systerel | Frankreich | Software, Beratung, Dienst | S3 Eine Modellprüfung für eine Synchronesprache, B-Methode, Ereignis-B/Rodin. Rekrutierung. |
| Sieben | USA, San Francisco Bay Area | Hardware | Coq LinkedIn |
| Ratebox | Amsterdam, Niederlande | Blockchain | Idris (Github) |
| Sukhoi | Russland, Moskau | Luft- und Raumfahrt und Verteidigung | ANSYS SCADE Suite (Quelle - Ein formell verifizierter Compiler für Glanz) |
| Thales | Frama-C (Ein Bottom-up-Ansatz für formale Verifizierung für gemeinsame Kriterien: Anwendung auf Javacard Virtual Machine) | ||
| Trustinsoft | USA, CA, San Francisco | - - | TrustInSoft Analyzer Site |
| Vertrauenswürdige Systeme | Australien, Sydney | Isabelle/HOL , Coq -Site | |
| Zwei sechs Technologien | USA | Verteidigungsforschung | Isabelle/HOL , Hardwareverifizierung (Beispiel), Coq (Beispiel) |
| Jetbrains Forschung | Saint Petersburg, Russland | - - | Coq (Quelle) |
| Цццт | Moskau, Russland | ? | SPIN/Promela методы и с седства верик und ции протоколов когерентнantwort |
| T-Plattformen | Moskau, Russland | - - | Coq , SPIN/Promela , TLA+ , McErlang , mCRL2 -Mitarbeiter CV |
| Cern | Genève, Schweiz | mCRL2 -Steuerungssoftware des CMS -Experiments bei Cerns großem Hadron Collider | |
| Yandex | Software | TLA+ Klick-Haus-Replikationsalgorithmus, sperrenfreier Speicher Allocator | |
| Zilliqa | Singapur | Blockchain | Coq Scilla-Coq-Projekt |
| Wellen | Blockchain | ??? |
