Developing correctly replicated databases using formal tools
- Submitting institution
-
The University of Birmingham
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 76032854
- Type
- E - Conference contribution
- DOI
-
10.1109/DSN.2014.45
- Title of conference / published proceedings
- 2014 44th Annual IEEE/IFIP international conference on dependable systems and networks (proceedings)
- First page
- 395
- Volume
- -
- Issue
- -
- ISSN
- 1530-0889
- Open access status
- Out of scope for open access requirements
- Month of publication
- June
- Year of publication
- 2014
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
4
- Research group(s)
-
-
- Citation count
- 9
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This paper was the first in a recent line of work on the formal (theorem prover-based) verification of implementations of distributed systems. As Tatlock (a world leading expert in formal verification) and colleagues noted, our paper introduces a language that "provides expressive primitives and combinators for implementing distributed
systems" (https://dl.acm.org/doi/abs/10.1145/2737924.2737958). This is significant because our paper described the first safety proof of an implementation of the seminal Paxos protocol, variants of which are widely used in industry by companies such as Google and Microsoft in some of their critical services.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -