Wednesday 21 December 2022
'VESPA: Verified, Efficient, and Secure Parallel Algorithms'.
Provably Bug-Free and Secure Parallel Software.
Almost every software system has bugs, and they regularly lead to catastrophic consequences, such as patients dying, fortunes of money being lost, and hackers invading into systems, stealing confident data and extorting ransoms. The software that runs on modern parallel computers is prone to concurrency bugs, which are easily made but hard to find by traditional testing methods. This project researches methods and tools to develop provably correct parallel software. The proofs themselves are checked by a small and well-tested piece of software, such that it is very unlikely to erroneously accept incorrect proofs.
