seL4/l4v

Issues

• Should we reduce DSpec to sys-init operations only?

  #767 opened 4 days ago by lsf37
  3

• support strongest-postcondition reasoning

  #763 opened 17 days ago by lsf37
  1

• take L4V_PLAT into account in rebuilds

  #762 opened 17 days ago by lsf37
  0

• Can Isabelle's custom functions and data types be combined with the C-parser?

  #756 opened a month ago by riyuejiuzhao
  0

• Enhance C Parser to allow named array bounds

  #754 opened a month ago by Xaphiosis
  3

• Decide on style for `[def]rule_tac ... [and ...] in ...`

  #746 opened 3 months ago by Xaphiosis
  7

• Investigate further use of `none_top/none_bot` in the proofs

  #751 opened 2 months ago by michaelmcinerney
  0

• Some way of blocking `simp` from unifying schematics

  #730 opened 4 months ago by Xaphiosis
  1

• Have wp warn when resulting in a goal with a schematic assumption.

  #729 opened 4 months ago by Xaphiosis
  15

• Sub-term to free variable lifting tactic

  #727 opened 4 months ago by Xaphiosis
  0

• Safer vcg in CRefine

  #726 opened 4 months ago by Xaphiosis
  0

• Methods such as monadic_rewrite_symb_exec_r should warn that discharging side-conditions failed

  #715 opened 4 months ago by Xaphiosis
  0

• should `corres_cases` also do case distinction on `if`?

  #652 opened a year ago by lsf37
  0

• does `ccorres` need a `corres_cases` equivalent?

  #651 opened a year ago by lsf37
  0

• CI artifact upload uses clashing artifact names

  #713 opened 4 months ago by lsf37
  0

• SIMPL: don't print `_'proc`

  #710 opened 5 months ago by lsf37
  0

• Document mysterious useful comments for ctac and ceqv

  #692 opened 8 months ago by Xaphiosis
  0

• Cleanup post-x64 comments

  #691 opened 8 months ago by Xaphiosis
  0

• Cleanup CRefine Wellformed_C

  #690 opened 8 months ago by Xaphiosis
  0

• Remove instances of `UNIV <\inter>` from CRefine

  #688 opened 8 months ago by Xaphiosis
  0

• Investigate adding `projectKOs` to the simp set

  #687 opened 8 months ago by michaelmcinerney
  1

• Problems with the autocorres tool

  #627 opened 9 months ago by goodoldboyyeah
  1

• Questions about the autocorres tool

  #626 opened 9 months ago by ambition-code
  4

• Cannot load theory file "l4v/proof/crefine/autocorres-test/Refine_C.thy"

  #662 opened 9 months ago by LC-John
  4

• Rename Word_Lib and Simpl sessions?

  #546 opened 10 months ago by lsf37
  4

• simpler `corres` and `corressimp` methods

  #634 opened 10 months ago by lsf37
  10

• Make AutoCorres 1.10 release

  #552 opened 10 months ago by lsf37
  1

• Create new verification-tools repo and add to manifest

  #549 opened 10 months ago by lsf37
  1

• Apply contrib queue to new repo

  #550 opened 10 months ago by lsf37
  1

• set up CI for verification-tools repo

  #551 opened 10 months ago by lsf37
  1

• Update release scripts and process

  #548 opened 10 months ago by lsf37
  1

• Adjust directory structure before repo move

  #547 opened 10 months ago by lsf37
  1

• investigate parallelising the haskell translator

  #635 opened a year ago by lsf37
  0

• Investigate greater use of heap projections in `Invariants_H.thy`

  #633 opened a year ago by michaelmcinerney
  0

• Move lemmas to CParser

  #631 opened a year ago by michaelmcinerney
  0

• sel4 verification

  #618 opened a year ago by ambition-code
  3

• restyle Platform.thy for all architectures

  #620 opened a year ago by lsf37
  0

• rename `kernel_base` to `pptrBase`

  #619 opened a year ago by lsf37
  0

• check scheduled workflow runs

  #611 opened a year ago by lsf37
  2

• our bit_simps shadows Word_Lib bit_simps

  #600 opened a year ago by lsf37
  0

• abs_typ_at_lifts should have an arch variant

  #599 opened a year ago by lsf37
  1

• Make `if_1_0_0` lemmas consistent

  #579 opened a year ago by corlewis
  2

• factor out more VCPU lemmas

  #571 opened a year ago by lsf37
  0

• Reduce AutoCorres dependencies

  #545 opened a year ago by lsf37
  0

• Reduce Monad lib dependencies

  #543 opened a year ago by lsf37
  0

• Reduce C parser dependencies

  #544 opened a year ago by lsf37
  1

• 'nslookup' tool missing while executing "./build.sh -b l4v"

  #514 opened 2 years ago by GooTal
  3

• should corres_underlying imply failure preservation?

  #528 opened 2 years ago by lsf37
  0

• `cinit lift: name` does not substitute `name = t` assumptions

  #522 opened 2 years ago by lsf37
  0

• add `crunches` lifting syntax

  #506 opened 2 years ago by lsf37
  2