search

PrincetonUniversity / VST

Verified Software Toolchain
https://vst.cs.princeton.edu
Other
425 stars 91 forks source link

sequential safety almost done #688

Closed rinshankaihou closed 1 year ago

rinshankaihou commented 1 year ago

What's left is to

  1. delete matchfunspec from Jsafe;
  2. make state_interp and ext_mpred_pre live on distinct heaplets.