Ecosyste.ms: Issues

An open API service for providing issue and pull request metadata for open source projects.

GitHub / uwplse/verdi issues and pull requests

#147 - simplify proofs

Pull Request - State: closed - Opened by gares 6 months ago - 1 comment

#146 - update publication URLs

Pull Request - State: closed - Opened by palmskog 12 months ago

#145 - Verdi paper links broken

Issue - State: closed - Opened by thesammiller 12 months ago

#144 - simplified conclude_using

Pull Request - State: closed - Opened by palmskog about 1 year ago

#143 - reorganize files under standard theories directory

Pull Request - State: closed - Opened by palmskog about 1 year ago

#142 - consistently use From-Require

Pull Request - State: closed - Opened by palmskog about 1 year ago

#141 - purge NPeano in favor of PeanoNat

Pull Request - State: closed - Opened by palmskog about 1 year ago

#140 - Fix deprecations

Pull Request - State: closed - Opened by palmskog about 1 year ago

#139 - Adapt w.r.t. coq/coq#17564.

Pull Request - State: closed - Opened by ppedrot over 1 year ago - 1 comment

#138 - What commit works for verdi with coq 8.12?

Issue - State: closed - Opened by brando90 almost 2 years ago - 2 comments

#137 - What version of coq-verdi does one need for coq 8.10

Issue - State: closed - Opened by brando90 almost 2 years ago

#136 - 8.17 drop configure

Pull Request - State: closed - Opened by palmskog almost 2 years ago

#135 - fix deprecations on 8.16 and later

Pull Request - State: closed - Opened by palmskog almost 2 years ago

#134 - add meta.yml, generate boilerplate

Pull Request - State: closed - Opened by palmskog about 2 years ago

#133 - Adapt w.r.t. coq/coq#16004.

Pull Request - State: closed - Opened by ppedrot over 2 years ago

#132 - Adapt w.r.t coq/coq#16004

Pull Request - State: closed - Opened by Alizter over 2 years ago

#131 - GhostSimulations:Be more robust to generated names

Pull Request - State: closed - Opened by JasonGross about 3 years ago - 1 comment

#129 - Adapt to coq/coq#13837 ("apply with" does not rename arguments)

Pull Request - State: closed - Opened by SkySkimmer about 3 years ago

#128 - Remove the only call to the Regular Subst Tactic option.

Pull Request - State: closed - Opened by ppedrot over 3 years ago - 1 comment

#127 - Replace use of omega with lia for Coq 8.14 #13741

Pull Request - State: closed - Opened by jfehrle over 3 years ago - 1 comment

#126 - Adapt w.r.t. coq/coq#12512.

Pull Request - State: closed - Opened by ppedrot over 4 years ago

#125 - Proposal: connect Verdi with verified crash-safe filesystem

Issue - State: open - Opened by palmskog about 5 years ago

#124 - Proposal: verify Verdi shim functions down to machine code

Issue - State: open - Opened by palmskog about 5 years ago

#122 - Modelling multithreaded applications

Issue - State: closed - Opened by k32 almost 6 years ago - 2 comments

#121 - port to Coq master

Pull Request - State: closed - Opened by palmskog almost 6 years ago

#120 - avoid using soon-to-be-deprecated automatic instance refinement

Pull Request - State: closed - Opened by palmskog almost 6 years ago

#119 - Use Docker to run Travis tests

Pull Request - State: closed - Opened by mernst almost 7 years ago

#118 - compatibility with both 8.6.1 and 8.7.0

Pull Request - State: closed - Opened by palmskog about 7 years ago

#117 - Disk log transformer and serialized message transformer

Pull Request - State: closed - Opened by palmskog about 7 years ago

#116 - Replace unmaintained finite map code with FMap from stdlib

Pull Request - State: closed - Opened by palmskog about 7 years ago

#115 - do all Travis build tasks via OPAM

Pull Request - State: closed - Opened by palmskog over 7 years ago

#114 - Generalize ghost sims

Pull Request - State: closed - Opened by palmskog over 7 years ago

#113 - Work around anomaly that only shows up in Coq trunk

Pull Request - State: closed - Opened by hackedy over 7 years ago

#112 - Support Coq 8.6

Pull Request - State: closed - Opened by A1kmm over 7 years ago - 1 comment

#111 - Use update function in reboot step of failure semantics

Pull Request - State: closed - Opened by palmskog over 7 years ago - 1 comment

#110 - SeqNum transformer using association list

Pull Request - State: closed - Opened by palmskog over 7 years ago

#109 - added labeled semantics for step_ordered_dynamic

Pull Request - State: closed - Opened by palmskog almost 8 years ago

#108 - use filterMap in partial map simulations

Pull Request - State: closed - Opened by palmskog almost 8 years ago

#107 - more straightforward names for liveness-related concepts

Pull Request - State: closed - Opened by palmskog almost 8 years ago - 1 comment

#106 - updated documentation

Pull Request - State: closed - Opened by palmskog almost 8 years ago

#105 - Friendlier syntax use in module declarations

Pull Request - State: closed - Opened by palmskog almost 8 years ago

#104 - use opam-dev repo in travis

Pull Request - State: closed - Opened by palmskog almost 8 years ago

#103 - small update to canonical OPAM metadata

Pull Request - State: closed - Opened by palmskog almost 8 years ago

#102 - Reenable downstream

Pull Request - State: closed - Opened by palmskog almost 8 years ago

#101 - Final changes to make Verdi OPAM ready

Pull Request - State: closed - Opened by palmskog almost 8 years ago

#100 - Uniform use of Verdi namespace

Pull Request - State: closed - Opened by palmskog almost 8 years ago

#99 - Remove string-related obsoleteness warnings

Pull Request - State: closed - Opened by palmskog almost 8 years ago - 1 comment

#98 - display second fractions in timestamps

Pull Request - State: closed - Opened by palmskog almost 8 years ago

#97 - make sure all order shim printfs are followed by flushing newlines

Pull Request - State: closed - Opened by palmskog almost 8 years ago

#96 - ISO 8601 timestamps, rework of printed messages in ordered shim

Pull Request - State: closed - Opened by palmskog almost 8 years ago

#95 - remove extraneous module val declaration in ordered shim

Pull Request - State: closed - Opened by palmskog almost 8 years ago

#94 - use same wrapper of select in both shims, placed in Util

Pull Request - State: closed - Opened by palmskog almost 8 years ago

#93 - Fair shims

Pull Request - State: closed - Opened by palmskog almost 8 years ago - 1 comment

#92 - Put reusable stuff from Chord extraction in Util

Pull Request - State: closed - Opened by hackedy almost 8 years ago

#91 - Dynamic ordered shim

Pull Request - State: closed - Opened by palmskog about 8 years ago

#90 - update disco repo

Pull Request - State: closed - Opened by palmskog about 8 years ago

#89 - Refactor unordered shim to omit request_id

Pull Request - State: closed - Opened by palmskog about 8 years ago

#88 - leave client id generation to ordered shim arrangements

Pull Request - State: closed - Opened by palmskog about 8 years ago

#87 - Reorganize unordered shim

Pull Request - State: closed - Opened by palmskog about 8 years ago

#86 - Expand OCaml util

Pull Request - State: closed - Opened by palmskog about 8 years ago

#85 - refactored ordered shim to enable client communication

Pull Request - State: closed - Opened by palmskog about 8 years ago

#84 - use specific Coq and ssreflect versions for Travis

Pull Request - State: closed - Opened by palmskog about 8 years ago

#83 - Coq and ssreflect from OPAM in Travis

Pull Request - State: closed - Opened by palmskog about 8 years ago

#82 - Add more Proof using annotations

Pull Request - State: closed - Opened by palmskog about 8 years ago

#81 - Documentation

Issue - State: closed - Opened by langston-barrett about 8 years ago - 2 comments

#80 - remove references to VarD in unordered shim to avoid possible confusion

Pull Request - State: closed - Opened by palmskog about 8 years ago

#80 - remove references to VarD in unordered shim to avoid possible confusion

Pull Request - State: closed - Opened by palmskog about 8 years ago

#79 - added ordered dynamic semantics without failures

Pull Request - State: closed - Opened by palmskog about 8 years ago

#78 - rename extraction-related module for easier compilation

Pull Request - State: closed - Opened by palmskog about 8 years ago

#77 - move ordered shim and main to dir with all OCaml extraction files

Pull Request - State: closed - Opened by palmskog about 8 years ago

#76 - Ordered shim with dynamic and failure modes

Pull Request - State: closed - Opened by wilcoxjay about 8 years ago

#75 - updated README.md on liveness and systems

Pull Request - State: closed - Opened by palmskog about 8 years ago

#74 - lifted weak_until_always lemma to InfSeqExt level

Pull Request - State: closed - Opened by palmskog about 8 years ago - 1 comment

#73 - Live Lockserv

Pull Request - State: closed - Opened by dwoos about 8 years ago - 1 comment

#72 - put type classes in Prop sort when possible

Pull Request - State: closed - Opened by palmskog about 8 years ago

#71 - added partial map execution simulations

Pull Request - State: closed - Opened by palmskog about 8 years ago

#70 - total mappings and simulations for executions

Pull Request - State: closed - Opened by palmskog about 8 years ago

#69 - add labeled async semantics

Pull Request - State: closed - Opened by palmskog about 8 years ago

#68 - added labeled params and execution-related definitions

Pull Request - State: closed - Opened by palmskog about 8 years ago

#67 - single node params and simulations

Pull Request - State: closed - Opened by palmskog about 8 years ago

#66 - added partial map simulations and plain ordered network semantics

Pull Request - State: closed - Opened by palmskog about 8 years ago

#65 - add total map VSTs for all ordered semantics

Pull Request - State: closed - Opened by palmskog about 8 years ago

#64 - Module types and modules for name overlays

Pull Request - State: closed - Opened by palmskog about 8 years ago

#63 - Add network semantics

Pull Request - State: closed - Opened by palmskog about 8 years ago

#62 - support for selecting StructTact branches to build against in travis

Pull Request - State: closed - Opened by palmskog about 8 years ago

#61 - enable quick compilation for lemmas and theorems

Pull Request - State: closed - Opened by palmskog about 8 years ago

#60 - refactored simulation type classes and proofs

Pull Request - State: closed - Opened by palmskog about 8 years ago

#59 - extract all_fin to 0..n-1 instead of 1..n, to match fin_to_nat

Pull Request - State: closed - Opened by palmskog about 8 years ago

#58 - updated to latest coqproject.sh

Pull Request - State: closed - Opened by palmskog about 8 years ago

#57 - add reference to Verdi Raft in README.md

Pull Request - State: closed - Opened by palmskog about 8 years ago

#56 - Move Raft verification into separate repository

Pull Request - State: closed - Opened by wilcoxjay about 8 years ago

#55 - pulled out and improved extraction-related definitions from VarDRaft

Pull Request - State: closed - Opened by palmskog about 8 years ago

#54 - more informative naming of step relations

Pull Request - State: closed - Opened by palmskog about 8 years ago

#53 - first attempt at style documentation

Pull Request - State: closed - Opened by palmskog about 8 years ago - 1 comment

#52 - Proofalytics

Pull Request - State: closed - Opened by ztatlock over 8 years ago

#51 - extracted out all update tactics into StructTact

Pull Request - State: closed - Opened by palmskog over 8 years ago

#50 - StructTact's generalized update in Raft

Pull Request - State: closed - Opened by palmskog over 8 years ago

#49 - Compatibility with StructTact that exports stand-alone update

Pull Request - State: closed - Opened by palmskog over 8 years ago