Vive la Difference: Paxos vs. Viewstamped Replication vs. Zab
by Robbert van Renesse, Nicolas Schiper, and Fred B. Schneider
IEEE Transactions on Dependable and Secure Computing. 2014
Towards a Formally Verified Proof Assistant
by Abhishek Anand and Vincent Rahli
The 5th Conference on Interactive Theorem Proving (ITP). Vienna, Austria. July 2014
Developing Correctly Replicated Databases Using Formal Tools
by Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, and Robert L. Constable
The 44th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). Atlanta, Georgia. June 2014
Inductive Construction in Nuprl Type Theory Using Bar Induction
by Mark Bickford and Robert Constable
Presented at TYPES 2014: Types for Proofs and Programs. Paris, France. May 2014
A Type Theory with Partial Equivalence Relations as Types
by Abhishek Anand, Mark Bickford, Robert Constable and Vincent Rahli
Presented at TYPES 2014: Types for Proofs and Programs. Paris, France. May 2014
Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types
by Vincent Rahli, Mark Bickford, and Abhishek Anand
4th Conference on Interactive Theorem Proving (ITP). Rennes, France. July 2013
Byzantine Chain Replication
by Robbert van Renesse, Chi Ho, and Nicolas Schiper
16th International Conference On Principles Of DIstributed Systems (OPODIS). Rome, Italy. December 2012
A Diversified and Correct-by-Construction Broadcast Service
by Vincent Rahli, Nicolas Schiper, Robbert Van Renesse, Mark Bickford and Robert L. Constable
Presented at the 2nd International Workshop on Rigorous Protocol Engineering (WRiPE). Austin, TX. October 2012
ShadowDB: A Replicated Database on a Synthesized Consensus Core
by Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable
Eighth Workshop on Hot Topics in System Dependability. 2012.
Interfacing with Proof Assistants for Domain Specific Programming Using EventML
Vincent Rahli
Presented at User Interfaces for Theorem Provers July 2012 (UITP12)
On Building Constructive Formal Theories of Computation Noting the Roles of Turing, Church, and Brouwer
Robert Constable
LICS 2012 June 2012 Invited. Article and lecture.
Proof Assistants and the Dynamic Nature of Formal Theories
Robert Constable
IJCAR Joint Workshops Invited June 2012. Article and lecture.
Type Theoretic Semantics for First-Order Logic
Robert Constable
The Constructive in Logic and Applications Conference Invited May 2012. Lecture.
Slide presentation on CRASH Methodology from PI meeting, May 2012
Mark Bickford
Slide presentation on Logic of Events, Jan. 2012
Mark Bickford
EventML Tutorial & Consensus Protocol March 2012
Mark Bickford, Robert L. Constable, Richard Eaton,
David Guaspari, and Vincent Rahli
EventML Manual & Introduction to Classic ML, 2011
by Christoph Kreitz and Vincent Rahli
Investigating Correct-by-Construction
Attack-Tolerant Systems, 2010
by Robert Constable, Mark Bickford, Robbert van Renesse
Attack-tolerant distributed systems change their protocols on-the-fly in response to apparent attacks from the environment; they substitute functionally equivalent versions possibly more resistant to detected threats. Alternative protocols can be packaged together as a single adaptive protocol or variants from a formal protocol library can be sent to threatened groups of processes. We are experimenting with libraries of attack-tolerant protocols that are correct-by-construction and testing them in environments that simulate specified threats, including constructive versions of the famous FLP imaginary adversary against fault-tolerant consensus. We expect that all variants of tolerant protocols are automatically generated and accompanied by machine checked proofs that the generated code satisfies formal properties.
Poster Slides for Correct by Construction Attack Tolerant Systems.
Kickoff Talk Slides from November 2010