commit 2c5d02a163216364610dc6cb30c23ec0eb17ce94 from: Sergey Bronnikov via: GitHub date: Mon Oct 30 10:21:47 2023 UTC README: Add Thales, update Airbus commit - 71c65582d277160a6367c7c817baf4093d375460 commit + 2c5d02a163216364610dc6cb30c23ec0eb17ce94 blob - e864cda3a3ec5e85ef725d8981f44d5fce583edb blob + ede6dbdb45ef872982576b762fa66324281c0dcf --- README.md +++ README.md @@ -7,7 +7,7 @@ If the company is hiring please include a link to the | Name | Location | Sector | Source | | :--- | :------- | :----- | :----- | [Amazon](https://www.amazon.com/) | USA | eCommerce, Cloud computing | ```TLA+``` [How Amazon Web Services Uses Formal Methods](https://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/abstract), [Use of Formal Methods at Amazon Web Services](http://lamport.azurewebsites.net/tla/amazon.html), ```CBMC``` [Model Checking Boot Code from AWS Data Centers](http://www.kroening.com/papers/cav2018-aws.pdf) -[Airbus](http://www.airbus.com/) | France | | ```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 the development of safety-critical software for vari­ous plane series, including the A380.", ```Coq``` ([Interview with Xavier Leroy](https://www.cs.cmu.edu/~popl-interviews/leroy.html)), `CAVEAT`, a C-verifier developed by CEA and [used by Airbus](https://www.researchgate.net/publication/3965267). +[Airbus](http://www.airbus.com/) | France | | ```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 the development of safety-critical software for vari­ous plane series, including the A380.", ```Coq``` ([Interview with Xavier Leroy](https://www.cs.cmu.edu/~popl-interviews/leroy.html)), `CAVEAT`, a C-verifier developed by CEA and [used by Airbus](https://www.researchgate.net/publication/3965267)., `Frama-C` ([Industrial use of a safe and efficient formal method based software engineering process in avionics](https://www.erts2020.org/inc/telechargerPdf.php?pdf=ERTS2020_paper_54.pdf)). [Altran](https://www.altran.com/us/en/) | France, Paris | | ```SPARK``` [SPARK contributors](http://www.spark-2014.org/contributors) [Apple](https://www.apple.com/) | Santa Clara Valley, California, USA | Hardware and Software | [Arm](https://www.arm.com/company) | Austin, Texas, & San Jose, California, USA | Hardware | ```ACL2``` [Verification of Arithmetic Hardware](https://ieeexplore.ieee.org/document/9974354), [Verifying against the official ARM specification](https://alastairreid.github.io/using-armarm/), ```TLA+``` [Linux Kernel](https://git.kernel.org/pub/scm/linux/kernel/git/cmarinas/kernel-tla.git/about/) @@ -60,6 +60,7 @@ PingCAP | | | ```TLA+``` [TLA+ in TiDB](https://github [SiFive](https://www.sifive.com) | USA, San Francisco Bay Area | Hardware | ```Coq``` [LinkedIn](https://www.linkedin.com/jobs/view/coq-proof-assistant-based-formal-verification-at-sifive-800018056/) [Statebox](https://statebox.org/) | Amsterdam, Netherlands | Blockchain | ```Idris``` ([github](https://github.com/statebox)) [Sukhoi](https://www.sukhoi.org/) | Russia, Moscow | Aerospace and defense | [```ANSYS SCADE Suite```](https://www.ansys.com/products/embedded-software/ansys-scade-suite) (source - [A Formally Verified Compiler for Lustre](http://www.tbrk.org/papers/pldi17-slides.pdf)) +[Thales](https://www.thalesgroup.com/en) | | | `Frama-C` ([A Bottom-Up Formal Verification Approach for Common Criteria Certification: Application to JavaCard Virtual Machine](https://nikolai-kosmatov.eu/publications/djoudi_hkkomff_erts_2022.pdf)) | [TrustInSoft](https://trust-in-soft.com/) | USA, CA, San Francisco | - | ```TrustInSoft Analyzer``` [Site](https://trust-in-soft.com/polarssl-verification-kit/) [Trustworthy Systems](https://ts.data61.csiro.au/) | Australia, Sydney | | ```Isabelle/HOL```, ```Coq``` [Site](https://ts.data61.csiro.au/projects/TS/l4.verified/) [Two Six Technologies](https://twosixtech.com/) | USA | Defense research | ```Isabelle/HOL```, Hardware verification ([example](https://github.com/twosixlabs/ReWire)), ```Coq``` ([example](https://github.com/twosixlabs/coq-operads))