Skip to content

Actions: seL4/l4v

Actions

Proofs

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
proof-deploy.yml
280 workflow runs
280 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

rt ainvs+riscv refine: remove duplicate of ko_at_kheap_upd_id Proofs #1308: Commit 8e8a348 pushed by michaelmcinerney
3h 14m 51s rt
rt
3h 14m 51s
rt refine+crefine: prove updateKernelObject_unbundle Proofs #1307: Commit 0cb85b4 pushed by michaelmcinerney
2h 54m 22s rt
rt
2h 54m 22s
rt lib+refine+crefine: update after cherry-picking Proofs #1306: Commit a11d2c5 pushed by michaelmcinerney
3h 46m 24s rt
rt
3h 46m 24s
lib: add rcorres definition, lemmas, and automation Proofs #1305: Commit 64effed pushed by michaelmcinerney
3h 59m 34s master
master
3h 59m 34s
lib+spec+proof: generalise list_queue_relation Proofs #1304: Commit 8ad42e3 pushed by michaelmcinerney
2h 7m 26s master
master
2h 7m 26s
ainvs: minor cleanup of ArchAcc_AI Proofs #1303: Commit 627aede pushed by Xaphiosis
4h 5m 49s master
master
4h 5m 49s
rt spec+proof: prove completeSignal_ccorres Proofs #1302: Commit d7d2a81 pushed by michaelmcinerney
3h 13m 53s rt
rt
3h 13m 53s
manifest-update Proofs #1301: Repository dispatch triggered by seL4-ci
3h 56m 5s
3h 56m 5s
rt spec+proof: prove restart_ccorres Proofs #1300: Commit a2451d5 pushed by lsf37
3h 19m 50s rt
rt
3h 19m 50s
manifest-update Proofs #1299: Repository dispatch triggered by seL4-ci
45s
45s
rt haskell+refine+crefine: prove lemmas related to sysargs_rel Proofs #1298: Commit 847795b pushed by michaelmcinerney
2h 58m 11s rt
rt
2h 58m 11s
rt spec+proof: prove decodeTCBInvocation_ccorres Proofs #1297: Commit 661df38 pushed by michaelmcinerney
3h 14m 48s rt
rt
3h 14m 48s
manifest-update Proofs #1296: Repository dispatch triggered by seL4-ci
2h 48m 57s
2h 48m 57s
manifest-update Proofs #1295: Repository dispatch triggered by seL4-ci
2h 56m 4s
2h 56m 4s
arm+arm-hyp haskell: remove where-clause warning Proofs #1294: Commit 2097b06 pushed by lsf37
3h 30m 55s master
master
3h 30m 55s
manifest-update Proofs #1293: Repository dispatch triggered by seL4-ci
2h 45m 19s
2h 45m 19s
aspec+ainvs+refine: consolidate cap_class/capClass Proofs #1292: Commit a86c56d pushed by lsf37
8m 6s master
master
8m 6s
manifest-update Proofs #1291: Repository dispatch triggered by seL4-ci
28m 4s
28m 4s
rt haskell+refine+crefine: prove finaliseCap_ccorres Proofs #1290: Commit 46c1d1c pushed by lsf37
2h 37m 57s rt
rt
2h 37m 57s
github: add rt PR test workflow to master Proofs #1289: Commit 608c697 pushed by lsf37
3h 12m 58s rt
rt
3h 12m 58s
github: add rt PR test workflow to master Proofs #1288: Commit 64ba2d3 pushed by lsf37
3h 21m 30s master
master
3h 21m 30s
manifest-update Proofs #1287: Repository dispatch triggered by seL4-ci
7m 8s
7m 8s
rt crefine: prove decodeInvocation_ccorres Proofs #1286: Commit 03b49d7 pushed by lsf37
19m 17s rt
rt
19m 17s
refine: add wordBits_word_bits to Bits_R Proofs #1285: Commit 748e983 pushed by michaelmcinerney
2h 38m 48s master
master
2h 38m 48s
refine+crefine: update for Schedule_R arch-split Proofs #1284: Commit e685272 pushed by Xaphiosis
2h 35m 15s master
master
2h 35m 15s