In this dissertation we describe two contributions to the state of the art in reasoning about liveness and safety, respectively. Programs for multiprocessor machines commonly perform busy waiting for synchronization. We propose the first separation logic for modularly verifying termination of such programs under fair scheduling. Our logic requires the proof author to associate a ghost signal with each busy-waiting loop and allows such loops to iterate while their corresponding signal $s$ is not set. The proof author further has to define a well-founded order on signals and to prove that if the looping thread holds an obligation to set a signal $s'$, then $s'$ is ordered above $s$. By using conventional shared state invariants to associate the state of ghost signals with the state of data structures, programs busy-waiting for arbitrary conditions over arbitrary data structures can be verified. Moreover, we present the first study of completeness thresholds for bounded memory safety proofs. Specifically, we consider heap-manipulating programs that iterate over arrays without allocating or freeing memory. In this setting, we present the first notion of completeness thresholds for program verification which reduce unbounded memory safety proofs to bounded ones. Furthermore, we demonstrate that we can characterise completeness thresholds for simple classes of array traversing programs. Finally, we suggest avenues of research to scale this technique theoretically, i.e., to larger classes of programs (heap manipulation, tree-like data structures), and practically by highlighting automation opportunities.

翻译：本文贡献了两项分别针对活性与安全性推理的前沿成果。多处理器机器的程序常采用忙等待实现同步，我们提出了首个能在公平调度下模块化验证此类程序终止性的分离逻辑。该逻辑要求证明者为每个忙等待循环关联一个幽灵信号，允许循环在对应信号$s$未被置位时持续迭代；证明者还需定义信号上的良基序，并证明若循环线程持有设置信号$s'$的义务，则$s'$的序高于$s$。通过使用常规共享状态不变量将幽灵信号状态与数据结构状态关联，可验证对任意数据结构中任意条件进行忙等待的程序。此外，我们首次开展了有界内存安全性证明的完备性阈值研究，具体针对不涉及内存分配/释放的数组遍历堆操作程序，提出了程序验证中首个能将无界内存安全性证明简化为有界证明的完备性阈值概念，并证明可为简单类别的数组遍历程序刻画完备性阈值。最终，我们提出了从理论层面（扩展至堆操作、树形结构等更大程序类别）与实践层面（凸显自动化机会）拓展该技术的未来研究方向。