Ownership Types for Verification of Programs with Pointer Arithmetic
Toman et al. have proposed a type system for automatic verification of low-level programs, which combines ownership types and refinement types to enable strong updates of refinement types in the presence of pointer aliases. We extend their type system to support pointer arithmetic, and prove its sou...
Zapisane w:
| Główni autorzy: | , , |
|---|---|
| Format: | Artykuł |
| Wydane: |
2023
|
| Hasła przedmiotowe: | |
| Dostęp online: | https://arxiv.org/abs/2312.06455 http://arxiv.org/abs/2312.06455 |
| Etykiety: |
Nie ma etykietki, Dołącz pierwszą etykiete!
|