commit eeae6835c234adc53a85eb92eb9493049fac2897 from: alvinary <49176889+alvinary@users.noreply.github.com> via: Sergey Bronnikov date: Wed Jul 03 19:56:33 2024 UTC Add Dafny to the list of Amazon tools commit - 5e081b197a4bc622e66b2e1fda8250faaf35d4e3 commit + eeae6835c234adc53a85eb92eb9493049fac2897 blob - 238acc11d0f96c4e3f3a03fcef37140332f5f98a blob + 43e4d8b01a50a53cc91581150d0a8ceec9724860 --- README.md +++ README.md @@ -6,7 +6,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) +[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), ```Dafny``` [AWS Encryption SDK](https://github.com/aws/aws-encryption-sdk-dafny) [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 |