Skip to content
Snippets Groups Projects
Select Git revision
  • better-liveness
  • causality_example
  • master default protected
  • reliable_communication
  • rpc_galaad
  • statelib
  • stlib
7 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.024Oct2320191027Sep211913126129Aug2724181716231Jul15429Jun272625232221201918171514131098765432131May25232221201918174May3Apr18Feb17Dec20Nov1722Oct817Sep4231Aug18317Jul1610[crdt] add G-Counter examplestlibstlib[crdt] add causality-related premise in a user-to-prove lemmaTEMP: à réorganisermastermaster[crdt] remove unneeded TODO[crdt] add TODO for instantiation[crdt] fix proofsSimplification of proofs and TODOspartial cleaning imports and contextsMoving the lock acquisition in apply_threadEnd of the allocation proofsEnd of the proof of initEnd of setupInstantiation and setup for the user (1 admit remains)Resources allocationEnd of the STS-related proofs (needs reorganization)new proto + cleaner proofs (merge_update and init to finish).Adding (e < e') wrt evid → (e <_t e') to the notion of local validitysimplification of user specs + partial proof of broadcast + proof of send to all[apply_thread]: end of the proofPartial proof of [apply_thread]Erratum: [update] is proven (not [apply_thread] yet)[apply_thread] proven (few remaining lemmas on [fresh_events]).specs + proofs of get_state, apply_thread (remaining admits) and send2allpreparing proofsuser model: reorganizationresources: reorganization of the proofsResources: first definition and proofsSTS definitionmodel definitionDefinition of time + generic Compute_Maximals instanceTermination with countable non-determinism (#13)fix renamingsimplify and cleanup the ping_pong exampleFinalised refactoringWIP refactoringAdded receivefresh constructrename ping_pong filesMore cleanup of echo exampleIndentation nitAdded an instructive echo example