Skip to content

Commit f4fee8d

Browse files
committed
Add some MongoDB formal verification materials
1 parent 869cd8a commit f4fee8d

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

README.md

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -559,13 +559,14 @@ See also [formal methods](#formal-methods) section.
559559
uses [formal verification](#formal-methods) with TLA+ to check correctness of their replication protocol. Describes
560560
how replication bugs could have been found with help of formal model.
561561
* [eXtreme Modelling in Practice](https://arxiv.org/abs/2006.00915) — two attempts at MongoDB to check that code
562-
conforms to its formal model.
562+
conforms to its formal model. Accompanying video [eXtreme Modelling in Practice](https://youtu.be/IIGzXX72weQ)
563563
* [Formal Verification of a Distributed Dynamic Reconfiguration Protocol](https://youtu.be/VwCBlmS7XEA) — talk on
564564
formally verifying MongoDB Raft-based replication reconfiguration protocol with TLAPS.
565565
Paper [preprint](https://arxiv.org/abs/2109.11987).
566566
* [Change Point Detection in Software Performance Testing](https://arxiv.org/abs/2003.00584) — paper on how MongoDB team
567567
automatically detects performance degradations in the presence of noise in continuous integration runs. The paper was
568568
presented at [ICPE 2020](https://youtu.be/rSBgcMFPkHU)
569+
* [Conformance Checking at MongoDB: Testing That Our Code Matches Our TLA+ Specs](https://www.mongodb.com/company/blog/engineering/conformance-checking-at-mongodb-testing-our-code-matches-our-tla-specs)
569570

570571
See also [formal methods](#formal-methods) section.
571572

0 commit comments

Comments
 (0)