commit 5e081b197a4bc622e66b2e1fda8250faaf35d4e3 from: Daniel Abrahamsson via: Sergey Bronnikov date: Sat Mar 23 18:35:49 2024 UTC Add Prover Technology commit - d941858f9c1a1be16de495047a9150a1d3da215f commit + 5e081b197a4bc622e66b2e1fda8250faaf35d4e3 blob - cba5461424ba4778a4f9be3b938b0a0f885675fc blob + 238acc11d0f96c4e3f3a03fcef37140332f5f98a --- README.md +++ README.md @@ -53,6 +53,7 @@ NASA | USA | Space | ```PVS``` [NASA Langley Formal Me [Oracle](https://www.oracle.com/) | Redwood Shores, CA, USA | Enterprise software, Cloud computing, Computer hardware | `ACL2` ([Proving Theorems about Java and the JVM with ACL2](https://www.cs.utexas.edu/users/moore/publications/marktoberdorf-02/index.html)) [Particular Software](https://particular.net/) | | | ```TLA+``` [TLA+ Specifications for NServiceBus](https://github.com/tmasternak/NServiceBus.ModelChecking) PingCAP | | | ```TLA+``` [TLA+ in TiDB](https://github.com/pingcap/tla-plus) +[Prover Technology](https://www.prover.com/) | Europe | Railway | `Model checking` [Rusbitech](https://rusbitech.ru/) (РусБиТех) | Russia, Moscow | Системное ПО | `Frama-C`, `Event-B` ([Моделирование и верификация политик безопасности управления доступом в операционных системах](https://www.ispras.ru/publications/2018/security_policy_modeling_and_verification/)) | [Rockwell Collins](https://www.rockwellcollins.com/) | USA, Cedar Rapids, Iowa | High Assurance Systems | [Formal Methods in the Aerospace Industry: Follow the Money](http://www.jaist.ac.jp/icfem2012/Cofer-ICFEM2012.pdf) [Serokell](https://serokell.io/#tech) | Tallinn, Estonia | Fintech, blockchain, IoT, machine learning, formal verification | `Agda`