IronFleet: proving practical distributed systems correct

By Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath T. V. Setty, Brian Zill. Symposium on Operating Systems Principles, 2015

434 citations recorded by the source corpus.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Cosette: An Automated Prover for SQL (2017, methodology): “As such, they have been used recently to prove the correctness of many software systems [22, 19].”
Learning Shape Analysis (2017, background): “A number of recent projects have shown that it is possible to verify implementations of systems with complex functional specifications (e.g. CompCert [27], miTLS [6], seL4 [24], and IronFleet [19]).”
Datacenter RPCs can be General and Fast (2018, background): “SMR is di cult to design and implement correctly [30]: the protocol must have a speci cation and a proof (e.”
Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling (2019, background): “It has been a longstanding, active area of artificial intelligence research that has demonstrated utility in the design of operating systems [1, 2], distributed systems [3, 4], compilers [5, 6], microprocessor design [7], and in general mathematics [8].”
Komodo: Using verification to disentangle secure-enclave hardware from software (2017, methodology): “Past work on verifying systems software [38, 39] extended Dafny with features for information hiding and modular reasoning such as opaque functions.”