Computer Science Thesis Proposal August 11, 2023 9:00am — 10:30am Location: In Person - Traffic21 Classroom, Gates Hillman 6501 Speaker: TRAVIS HANCE , Ph.D. Student, Computer Science Department, Carnegie Mellon University https://www.andrew.cmu.edu/user/thance/ Verifying Concurrent Systems Concurrent software is notoriously difficult to write correctly, so to increase confidence in it, it is often desirable to apply formal verification techniques. One technique that is especially promising for verifying concurrent software is concurrent separation logic (CSL), which uses reasoning principles based on resource ownership. However, even with CSL, verifying complex systems at scale (e.g., those with 1000s of lines of code) remains challenging. The reasons it remains challenging include, The manual proof effort required by many existing CSL frameworks. The inherent complexity of the target systems. Sophisticated systems may have custom, low-level synchronization logic, which may be deeply intertwined with domain logic, in the interest of performance. We posit that a promising way to overcome (1) is, rather than using CSL directly, to use an ownership type system such as Rust’s, taking advantage of its sophisticated but efficient type-checking algorithms. To demonstrate this, we develop a full methodology (from theory to implementation) based around this core idea. We show that it has numerous advantages, and in particular, it is rich enough to support the verification of inherently complex systems as in (2). Thesis Committee: Bryan Parno (Chair) Frank Pfenning Dave Andersen Derek Dreyer (Max Planck Institute for Software Systems) Add event to Google Add event to iCal
