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$。通过利用常规共享状态不变量将幽灵信号状态与数据结构状态相关联，可验证需基于任意数据结构上任意条件进行忙等待的程序。此外，我们首次提出有界内存安全证明的完备性阈值研究。具体针对不涉及内存分配/释放的数组迭代堆操作程序，给出了程序验证中首个完备性阈值概念，将无界内存安全证明归约为有界形式。进一步证明，对简单类数组遍历程序可刻画其完备性阈值。最后，我们从理论（扩展至堆操作、树形数据结构等更大程序类别）和实践（突出自动化机会）两个维度提出该技术的规模化研究方向。