Mechanised Hypersafety Proofs about Structured Data
Arrays are a fundamental abstraction to represent collections of data. It is often possible to exploit structural properties of the data stored in an array (e.g., repetition or sparsity) to develop a specialised representation optimised for space efficiency. Formally reasoning about correctness of m...
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Association for Computing Machinery
2024
|
| Online Access: | https://hdl.handle.net/1721.1/155467 |