Skip to content

Actions: shaobo-he/dafny_examples

Actions

All workflows

Actions

Loading...
Loading

Showing runs from all workflows
32 workflow runs
32 workflow runs

Filter by Workflow

⌥ + click/return to exclude

Filter by Event

⌥ + click/return to exclude

Filter by Status

⌥ + click/return to exclude

Filter by Branch

⌥ + click/return to exclude

Filter by Actor

⌥ + click/return to exclude
Resolve Dafny audit findings check proofs #86: Commit 5d73fd0 pushed by shaobo-he
2m 16s develop
develop
2m 16s
Add Dafny runtime tests to CI check proofs #85: Commit 5f1f946 pushed by shaobo-he
2m 35s develop
develop
2m 35s
Tighten remaining Dafny proof claims check proofs #84: Commit 0fa3a55 pushed by shaobo-he
1m 59s develop
develop
1m 59s
Clarify remaining Dafny specs check proofs #83: Commit 828ecb2 pushed by shaobo-he
1m 56s develop
develop
1m 56s
Strengthen Dafny proof specifications check proofs #82: Commit d224af8 pushed by shaobo-he
1m 35s develop
develop
1m 35s
prove DFSProp: the constructed DFS tree has no cross edges (1192 last… check proofs #81: Commit ebe1bdd pushed by shaobo-he
1m 57s develop
develop
1m 57s
add verified DFS constructing a spanning pre-order tree (1192 last mi… check proofs #80: Commit 7dcc3b9 pushed by shaobo-he
1m 41s develop
develop
1m 41s
prove the deeper theorem: Tarjan's low[v] > disc[u] bridge criterion check proofs #79: Commit 3f8368d pushed by shaobo-he
1m 16s develop
develop
1m 16s
add leetcode 1192 critical connections -- exact bridge-set correctness check proofs #78: Commit 1c10510 pushed by shaobo-he
1m 27s develop
develop
1m 27s
add leetcode 0004 median of two sorted arrays -- exact O(log) correct… check proofs #77: Commit ed34fc6 pushed by shaobo-he
1m 33s develop
develop
1m 33s
leetcode 0407: prove TRUE 2-D trapped-water correctness (the hard part) check proofs #76: Commit 4b4c5b4 pushed by shaobo-he
50s develop
develop
50s
add leetcode 0042 trapping rain water (1-D) -- EXACT correctness check proofs #75: Commit 2f396c9 pushed by shaobo-he
1m 21s develop
develop
1m 21s
add leetcode 0407 trapping rain water II (min-heap flood) check proofs #74: Commit 51a8ceb pushed by shaobo-he
1m 21s develop
develop
1m 21s
0026: witness both membership directions to kill the brittle VC check proofs #73: Commit 0a6ac8e pushed by shaobo-he
1m 25s develop
develop
1m 25s
0026: replace {:vcs_split_on_every_assert} with a pinned trigger check proofs #72: Commit 6b507aa pushed by shaobo-he
1m 42s develop
develop
1m 42s
audit: prove reverse membership for 0026 remove duplicates check proofs #71: Commit bd2b4a6 pushed by shaobo-he
1m 30s develop
develop
1m 30s
audit: prove multi-transaction optimality for 0122 stocks II check proofs #70: Commit 76266ca pushed by shaobo-he
1m 43s develop
develop
1m 43s
audit: eliminate soundness gaps and fix BST invariant check proofs #69: Commit 445c13c pushed by shaobo-he
1m 25s develop
develop
1m 25s
add leetcode 0312 burst balloons (bottom-up interval DP) check proofs #68: Commit 915a1d8 pushed by shaobo-he
1m 26s develop
develop
1m 26s
docs: bump leetcode count to 24 (LRU cache, calculator III) check proofs #67: Commit 5fec221 pushed by shaobo-he
1m 35s develop
develop
1m 35s
docs: refresh README layout (Graph, leetcode count) check proofs #66: Commit a2537f1 pushed by shaobo-he
1m 9s develop
develop
1m 9s
add graph topological sort via Kahn's BFS check proofs #65: Commit be6d096 pushed by shaobo-he
1m 9s develop
develop
1m 9s
add leetcode 0123 stocks iii check proofs #64: Commit 1af413f pushed by shaobo-he
1m 8s develop
develop
1m 8s
add leetcode 0023 merge k sorted lists check proofs #63: Commit 8a58464 pushed by shaobo-he
58s develop
develop
58s
add leetcode 0340 longest substring k distinct check proofs #62: Commit d34e4a8 pushed by shaobo-he
1m 2s develop
develop
1m 2s