Concurrent Low-Level System Code Verification

Concurrent program reasoning is hard. There has been many program logics proposed, and they either require special expertise or not reusable systems for arbitrary data structures. Our concern is to come with simple type assertions which are

  • denoted with abstract predicates,
  • simple and,
  • reusable for arbitrary clients.
It is interesting that type assertions usually are capable of asserting properties which are similar to the ones that heavy-weight program logics assert, e.g. memory safety.