practical fm
1.0.0
더 이상 존재하지 않거나 더 이상 공식적인 방법을 사용하지 않는 회사가 목록에 표시되면 설명과 함께 풀 요청을 보내주십시오. 현재 일하고 있거나 공식적인 방법을 사용하지만 목록에 있지 않은 회사를 알고있는 경우에도 마찬가지입니다. 웹 사이트, Github (해당되는 경우), 위치 및 부문을 포함하십시오. 회사가 고용중인 경우 광고 링크를 포함하십시오.
| 이름 | 위치 | 부문 | 원천 |
|---|---|---|---|
| 아마존 | 미국 | 전자 상거래, 클라우드 컴퓨팅 | TLA+ Amazon Web Services를 사용하여 공식적인 방법, Amazon Web Services에서 공식 방법 사용, CBMC 모델 AWS 데이터 센터에서 부팅 코드 확인, Dafny AWS 암호화 SDK |
| 에어 버스 | 프랑스 | Astrée : "2003 년 Astrée는 Airbus 모델의 기본 비행 제어 소프트웨어에 런타임 오류가 없음을 증명했습니다. 시스템의 132,000 라인의 C 코드는 300MB의 메모리를 사용하여 2.8GHz 32 비트 PC에서 80 분 안에 완전히 자동으로 분석되었습니다 (580mb의 메모리를 사용하여 Amd Athlon 64에서만 50 분 만에 Amberbs in Atror). CAVEAT Coq Frama-C | |
| 알트란 | 프랑스, 파리 | SPARK 스파크 기고자 | |
| 사과 | 산타 클라라 밸리, 캘리포니아, 미국 | 하드웨어 및 소프트웨어 | |
| 팔 | 오스틴, 텍사스 및 미국 캘리포니아 산호세 | 하드웨어 | ACL2 공식 팔 사양에 대해 확인, TLA+ Linux 커널에 대한 ARITHMETIC 하드웨어 검증 |
| Adacore | 미국, 뉴욕 | ? | ? |
| 알라 크리스 | ? | 블록 체인 | |
| BAE 시스템 | Coq Reddit | ||
| 기반암 시스템 | 보스턴 & 베이 지역, 미국; 베를린 & 뮌헨, 독일 | 시스템 보안, 신뢰할 수있는 컴퓨팅 | Coq , C++ , Github |
| 보잉 회사 | 미국 | 항공 우주, 방어 | Coq (증명 없음), Ivory (출처) |
| 보쉬 | 독일 | 자동차 | 아스트레 |
| Centaur 기술 | 미국 | 하드웨어 | ACL2 |
| COG 시스템 | 호주, 뉴 사우스 웨일즈, 시드니 | 대지 | |
| 데이터 61 | 호주 | Isabelle/HOL (SEL4 확인 프로젝트) | |
| 포목상 | 미국 | 방어, 우주 | Coq , Z3 |
| 이더 리움 | 스위스 | Why3 Dev 업데이트 : 공식 방법, Isabelle/HOL A EVM 및 일부 Isabelle/Hol 증명의 LEM 공식화, Coq Ethereum Contracts의 공식적인 검증 | |
| 가장자리 보안 | 소프트웨어 | Tamarin 와이어 가드 | |
| Espark 학습 | 미국, 일리노이 주 시카고 | 교육 | 실제로 TLA+ 공식 방법 : Espark Learning에서 TLA+ 사용 |
| 탄력 있는 | 글로벌 | 검색 및 분석 소프트웨어 | TLA+ Isabelle/HOL Elasticsearch-Formal-Models 리포지토리 컨퍼런스 토크 및 현재 오픈 포지션 |
| 유럽 우주국 | 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은 정적 분석을 사용하여 보안 문제를 감지하고 방지하는 방법 | |
| 불 | 독일 드레스덴 (팀 소멸) | 보안 | Coq 직업 발표 : Fireeye의 공식 방법 엔지니어 및 과학 개발자 |
| 지느러미 | 러시아, spb | 금융 (블록 체인) | Coq , Agda |
| 공식적인 땅 | 글로벌 | 소프트웨어 | Tezos 블록 체인의 Coq 검증 |
| 공식적인 증언 | 바르셀로나, 스페인 | 법 | Coq DateTime 소프트웨어를 공식화했습니다 |
| 갈로이 | 미국 오리건 주 포틀랜드 | 컨설팅/연구 | Coq (?) |
| GERUA GMBH | 독일 | CPAchecker 소프트웨어 품질의 또 다른 경로? 자동화 된 소프트웨어 검증 및 OpenBSD 및 소프트웨어 verification의 적용 OpenBSD 네트워크 모듈 | |
| 미국 CA | 클라우드 컴퓨팅, 컴퓨터 소프트웨어, AI | Coq (암호화 산술에 대한 간단한 고급 코드-증명, 타협없이 (크롬)), 실시간 Maude에서 Google Megastore의 공식 모델링 및 분석 | |
| 문법 | Frama-C C FRAMA-C를위한 ACSL의 Frama-C C 라이브러리 주석 : 경험 보고서 | ||
| 그린 힐스 소프트웨어 | 미국 | 항공 우주 | ACL2 의 ACL2 산업 사용 |
| Kestrel Institute | 미국 | 컴퓨터 과학 연구 | 대부분 ACL2, 일부 Isabelle/Hol, PVS 및 COQ. 자세한 내용 및 출판물은 웹 사이트, 특히 프로젝트 페이지 및 사람 페이지를 참조하십시오. |
| IBM | 미국 | ? | SPIN/Promela Paul E. McKenney의 저널, 근본적으로 RCU는 무엇입니까? (Linux 커널, RCU), Coq Q*Cert |
| Ige+Xao | 유럽 | 컴퓨터 보조 디자인 | Coq 경험 보고서 : CAD 개발 컨텍스트 내부에서 약간의 COQ 밀수 COQ는 다음을 검증하는 데 사용됩니다. (i) 도메인 별 알고리즘 (전기 설계 문서에 대한 "패치"적용) (ii) 그래프 알고리즘 (A* 검색, 길이 예측 트리 레이아웃, B & B TSP, ...) (III) (Union, PRORTION, PROGRENT PROGRONT) 언어 단용 추론) (v) 소규모 연구 프로젝트 |
| 인텔 | 미국 | 하드웨어 | Prover (Intel에서 15 년의 공식적인 속성 검증), HOL Light (IA-64 디비전 알고리즘의 공식 검증), TLA+ (프리 RTL 공식 검증 : 인텔 경험) |
| 비공식 시스템 | 토론토, 비엔나, 로잔, 베를린 | 블록 체인, 분산 시스템 | TLA+ APALACHE, TLA+, Rust Tendermint BFT Consensus 및 TLA+ 사양을 사용한 Rust의 Tendermint BFT Consensus 및 InterBlockchain 통신 프로토콜, TLA+ 및 Apalache를 사용한 모델 기반 테스트 |
| 인포테스 | 러시아, 모스크바 | TLA+ , Coq , fault-tolerant 분산 상호 배제 알고리즘의 구성 및 공식 검증, построение и верифи 변천 | |
| ISP RAS | 모스크바, 러시아 | 운영 체제; 하드웨어 | Frama-C , Jessie , Why3 Astraver, Linux 커널 라이브러리 기능은 공식적으로 확인되었습니다. SPIN/Promela , Microtesk 사이트; Event-B моделирование и верифа칭 политик безопасти управления доступом В операцион이 систе,, 이벤트 B 사양의 일부; CAP9 커널의 Isabelle/HOL 공식 사양 |
| Kernkonzept Gmbh | 독일 | 운영 체제 | L4Re (소스) |
| 카스퍼 스키 | 모스크바, 러시아 | 보안/AV | 합금, TLA, Event-B (소스), Ivory (소스) |
| Machine Zone Inc. | 러시아 제국 | 모바일 게임 소프트웨어, 실시간 컴퓨팅, 클라우드 기반 네트워킹 | TLA+ 트위터 |
| 마이크로 소프트 | 미국 레드몬드, 미국 | 소프트웨어 개발 | TLA+ TLA+ 증명, 프로그래머에 대한 사고, Azure Cosmos DB가 제공하는 5 가지 일관성 수준에 대한 고급 TLA+ 사양, Microsoft's Static Driver Verifier 장치 드라이버의 철저한 정적 분석 Clousot 정적 반대 추상적 해석, 공식 방법 및 분산 시스템에 대한 도구, Microsoft의 공식적인 방법으로 정식 메소드의 정적 정적 검사를 철저히 정적으로 분석합니다. |
| Mongodb | 미국 뉴욕 | 소프트웨어 개발 | MongoDB 복제 시스템의 단순화 된 부분의 TLA+ TLA+ 사양 |
| NASA | 미국 | 공간 | PVS NASA Langley 공식 방법 연구 프로그램. JPF Java Pathfinder, 강력한 소프트웨어 엔지니어링 그룹, Model Checking 제트 추진 실험실, SPIN/Promela 영감 스핀, PVS (소스) |
| 유목 실험실 | 파리, 프랑스 | 블록 체인 | 소프트웨어 검증의 Coq 페이지 |
| 신탁 | 미국 캘리포니아 주 레드 우드 쇼어 | 엔터프라이즈 소프트웨어, 클라우드 컴퓨팅, 컴퓨터 하드웨어 | ACL2 (Java 및 ACL2로 JVM에 대한 이론을 증명) |
| 특정 소프트웨어 | nservicebus에 대한 TLA+ tla+ 사양 | ||
| Pingcap | TIDB의 TLA+ TLA+ | ||
| 잠언 기술 | 유럽 | 철도 | Model checking |
| rusbitech (русбитех) | 러시아, 모스크바 | системное по | Frama-C , Event-B (моделирование и и верификация политик безопасности 랜스 |
| 로크웰 콜린스 | 미국, 시더 래 피즈, 아이오와 | 높은 보증 시스템 | 항공 우주 산업의 공식적인 방법 : 돈을 따르십시오 |
| 세로 켈 | 탈린, 에스토니아 | 핀 테크, 블록 체인, IoT, 기계 학습, 공식 검증 | Agda |
| 개요 | ? | ? | 대지 |
| Systerel | 프랑스 | 소프트웨어, 컨설팅, 서비스 | S3 Synchrone 언어, B 메소드, Event-B/Rodin에 대한 모델 검사기. 모병. |
| Sifive | 미국, 샌프란시스코 베이 지역 | 하드웨어 | Coq LinkedIn |
| 스테이트 박스 | 암스테르담, 네덜란드 | 블록 체인 | Idris (Github) |
| Sukhoi | 러시아, 모스크바 | 항공 우주 및 방어 | ANSYS SCADE Suite (소스 - 공식적으로 검증 된 컴파일러) |
| 탈레스 | Frama-C (일반적인 기준 인증을위한 상향식 공식 검증 접근법 : Javacard 가상 머신에 응용 프로그램) | ||
| Trustinsoft | 미국, 캘리포니아, 샌프란시스코 | - | TrustInSoft Analyzer 사이트 |
| 신뢰할 수있는 시스템 | 호주, 시드니 | Isabelle/HOL , Coq 사이트 | |
| 2 개의 6 가지 기술 | 미국 | 방어 연구 | Isabelle/HOL , 하드웨어 검증 (예), Coq (예) |
| JetBrains 연구 | 상트 페테르부르크, 러시아 | - | Coq (소스) |
| м주 께 | 모스크바, 러시아 | ? | SPIN/Promela методы и средства верификации протоколов 관어 관어 |
| t- 플랫폼 | 모스크바, 러시아 | - | Coq , SPIN/Promela , TLA+ , McErlang , mCRL2 직원 CV |
| CERN | Genève, 스위스 | CERN의 대형 Hadron Collider에서 CMS 실험의 mCRL2 제어 소프트웨어 | |
| 얀덱스 | 소프트웨어 | TLA+ 클릭 하우스 복제 알고리즘, 잠금 메모리 할당 | |
| Zilliqa | 싱가포르 | 블록 체인 | Coq Scilla-Coq 프로젝트 |
| 파도 | 블록 체인 | ? |
