Formal Verification of Concurrent Software
Event details
| Date | 25.08.2022 |
| Hour | 13:30 › 15:30 |
| Speaker | Yugesh Kothari |
| Location | |
| Category | Conferences - Seminars |
EDIC candidacy exam
Exam president: Prof. Martin Odersky
Thesis advisor: Prof. Sanidhya Kashyap
Co-examiner: Prof.George Candea
Abstract
Concurrency is hard. Writing high performance
safe concurrent code is challenging even for seasoned developers.
Moreover, high performance applications are increasingly trying
to leverage kernel customization (via eBPF or kernel modules)
to juice out performance for specific target workloads. Such a
customisable surface increases chances for specification violations
both in terms of safety and liveness. In this thesis, I motivate these
points and make a case for developing techniques for verifying
liveness of concurrent software.
Background papers
Exam president: Prof. Martin Odersky
Thesis advisor: Prof. Sanidhya Kashyap
Co-examiner: Prof.George Candea
Abstract
Concurrency is hard. Writing high performance
safe concurrent code is challenging even for seasoned developers.
Moreover, high performance applications are increasingly trying
to leverage kernel customization (via eBPF or kernel modules)
to juice out performance for specific target workloads. Such a
customisable surface increases chances for specification violations
both in terms of safety and liveness. In this thesis, I motivate these
points and make a case for developing techniques for verifying
liveness of concurrent software.
Background papers
Practical information
- General public
- Free