A diversified and correct-by-construction broadcast service

Rahli, Vincent; Schiper, Nicolas; Renesse, Robbert Van; Bickford, Mark; Constable, Robert L.

doi:10.1109/ICNP.2012.6459943

Request a copy

Paper published in a book (Scientific congresses, symposiums and conference proceedings)

A diversified and correct-by-construction broadcast service

Rahli, Vincent; Schiper, Nicolas; Renesse, Robbert Van et al.

2012 • In ICNP 2012

Peer reviewed

Permalink
https://hdl.handle.net/10993/22666

DOI
10.1109/ICNP.2012.6459943

Files (1)Send to Details Statistics Bibliography Similar publications

Files

Full Text

WRIPE_2012_Paper.pdf

Author preprint (217.78 kB)

Request a copy

All documents in ORBilu are protected by a user license.

Send to

RIS BibTex APA Chicago Permalink X Linkedin

Details

Disciplines :

Computer science

Author, co-author :

Rahli, Vincent ; Cornell University > Computer Science Department

Schiper, Nicolas; Cornell University > Computer Science Department

Renesse, Robbert Van; Cornell University > Computer Science Department

Bickford, Mark; Cornell University > Computer Science Department

Constable, Robert L.; Cornell University > Computer Science Department

External co-authors :

yes

Language :

English

Title :

A diversified and correct-by-construction broadcast service

Publication date :

2012

Event name :

WRiPE 2012

Event date :

from 30-10-2012 to 02-11-2012

Main work title :

ICNP 2012

Peer reviewed :

Peer reviewed

Additional URL :

http://doi.ieeecomputersociety.org/10.1109/ICNP.2012.6459943

Commentary :

1--6

Available on ORBilu :

since 30 November 2015

Statistics

Number of views

33 (1 by Unilu)

Number of downloads

0 (0 by Unilu)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

WoS citations^™

Bibliography

The Coq Proof Assistant. http://coq.inria.fr/.
S. F. Allen, M. Bickford, R. L. Constable, R. Eaton, C. Kreitz, L. Lorigo, and E. Moran. Innovations in computational type theory using Nuprl. J. Applied Logic, 4(4):428-469, 2006. (Pubitemid 44647980)
J. Baker, C. Bond, J. Corbett, J. J. Furman, A. Khorlin, J. Larson, J.-M. Leon, Y. Li, A. Lloyd, and V. Yushprakh. Megastore: Providing scalable, highly available storage for interactive services. In CIDR'11, pages 223-234, 2011.
Y. Bertot and P. Casteran. Interactive Theorem Proving and Program Development. Springer Verlag, 2004.
M. Bickford. Component specification using event classes. In Component-Based Software Engineering, 12th Int'l Symp., volume 5582 of LNCS, pages 140-155. Springer, 2009.
M. Bickford and R. L. Constable. Formal foundations of computer security. In NATO Science for Peace and Security Series, D: Information and Communication Security, volume 14, pages 29-52. 2008.
M. Bickford, R. L. Constable, J. Y. Halpern, and S. Petride. Knowledgebased synthesis of distributed systems using event structures. Logical Methods in Computer Science, 7(2), 2011.
M. Bickford, C. Kreitz, and R. van Renesse. Formally verifying hybrid protocols with the NUPRL logical programming environment. Technical Report TR2001-1839, Cornell University, Ithaca, New York, 2001.
M. Bickford, C. Kreitz, R. van Renesse, and X. Liu. Proving hybrid protocols correct. In R. Boulton and P. Jackson, editors, Proceedings of 14th Int'l Conf. on Theorem Proving in Higher Order Logics (TPHOLs'01), volume 2152 of Lecture Notes in Computer Science, pages 105-120. Springer-Verlag, 2001.
G. S. Blair, L. Blair, V. Issarny, P. Tuma, and A. Zarras. The role of software architecture in constraining adaptation in component-based middleware platforms. In Middleware'00, pages 164-184, Secaucus, NJ, USA, 2000.
M. Burrows. The Chubby Lock Service for loosely-coupled distributed systems. In SOSP'06, Seattle, WA, 2006.
Wen-Ke C., M.A. Hiltunen, and R.D. Schlichting. Constructing adaptive software in distributed systems. In 21st Int'l Conf. on Distributed Computing Systems., pages 635-643, 2001.
B. Charron-Bost and A. Schiper. The Heard-Of model: computing in distributed systems with benign failures. Distributed Computing, 22(1):49-71, 2009.
L. Chen and A. Avizienis. N-version programming: A fault-tolerance approach to reliability of software operation. In FTCS'77, Los Alamitos, CA, 1977. IEEE Computer Society Press.
R. Constable, M. Bickford, and R. van Renesse. Investigating correct-by-construction attack-tolerant systems. Technical report, Department of Computer Science, Cornell University, 2010.
R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith. Implementing mathematics with the Nuprl proof development system. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1986.
C. Dwork, N. Lynch, and L. Stockmeyer. Consensus in the presence of partial synchrony. J. ACM, 35(2):288-323, 1988.
M. J. Fischer, N. A. Lynch, and M. S. Patterson. Impossibility of distributed consensus with one faulty process. J. ACM, 32(2):374-382, 1985.
M. J. C. Gordon, R. Milner, and C. P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation., volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.
J. O. Hallstrom, W. M. Leal, and A. Arora. Scalable evolution of highly available systems. Transactions of the Institute for Electronics, Information and Communication Engineers, pages 2154-2164, 2003.
R. Hayton, A. Herbert, and D. Donaldson. Flexinet-a flexible component oriented middleware system. In Proceedings of the 8th ACM SIGOPS European workshop on Support for composing distributed applications, pages 17-24, New York, NY, USA, 1998. ACM.
M. Isard. Autopilot: Automatic data center management. Operating Systems Review, 41(2):60-67, 2007.
S. Jajodia, A. K. Ghosh, V. Swarup, C. Wang, and X. S. Wang, editors. Moving Target Defense - Creating Asymmetric Uncertainty for Cyber Threats, volume 54 of Advances in Information Security. Springer, 2011.
J.C. Knight and N.G. Leveson. An experimental evaluation of the assumption of independence in multiversion programming. 12(1), 1986.
L. Lamport. Time, clocks, and the ordering of events in a distributed system. CACM, 21(7):558-565, July 1978. (Pubitemid 8615486)
L. Lamport. The part-time parliament. Trans. on Computer Systems, 16(2):133-169, 1998. (Pubitemid 128482394)
L. Lamport. Fast Paxos. Distributed Computing, 19(2):79-103, 2006. (Pubitemid 44673722)
L. Lamport. Byzantizing paxos by refinement. In David Peleg, editor, DISC, volume 6950 of LNCS, pages 211-224. Springer, 2011.
L. Lamport. Mechanically checked safety proof of a byzantine paxos algorithm, 2011.
X. Leroy. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In POPL'06, pages 42-54. ACM, 2006.
D. Pavlovic, P. Pepper, and D. R. Smith. Formal derivation of concurrent garbage collectors. In Claude Bolduc, Jules Desharnais, and Béchir Ktari, editors, MPC, volume 6120 of LNCS, pages 353-376. Springer, 2010.
D. Pavlovic and D. R. Smith. Software development by refinement. In Formal Methods at the Crossroads. From Panacea to Foundational Support, 10th Anniversary Colloquium of UNU/IIST, volume 2757 of LNCS, pages 267-286. Springer, 2002.
V. Rahli. Interfacing with proof assistants for domain specific programming using EventML. Presented to UITP 2012.
O. Rutti and A. Schiper. A predicate-based approach to dynamic protocol update in group communication. In IPDPS'08, pages 1-12, 2008.
F.B. Schneider. Implementing fault-tolerant services using the state machine approach: A tutorial. ACM Computing Surveys, 22(4):299-319, December 1990.
N. Swamy, J. Chen, C. Fournet, P.-Y. Strub, K. Bhargavan, and J. Yang. Secure distributed programming with value-dependent types. In 16th ACM SIGPLAN Int'l Conf. on Functional Programming, pages 266-278. ACM, 2011.
T. Tsuchiya and A. Schiper. Using bounded model checking to verify consensus algorithms. In DISC, pages 466-480, 2008.
R. van Renesse, Kenneth P. Birman, Mark Hayden, Alexey Vaysburd, and David Karr. Building adaptive systems using Ensemble. Software - Practice and Experience, 1998.
S. Weil, S.A. Brandt, E.L. Miller, D.D.E. Long, and C. Maltzahn. Ceph: A scalable, high-performance distributed file system. In OSDI'06, 2006.