论文标题
在构图上证明超安全性
Proving Hypersafety Compositionally
论文作者
论文摘要
Arity $ n $的超安全性属性是将$ n $ traces traces trace（或更一般而言的$ n $ program的痕迹）相关联的程序属性。经典示例包括确定性，竭力和关联性。已经引入了许多关系程序逻辑来针对此类属性。他们的目的是通过利用相关程序之间的结构相似性来构建更简单的证据。我们提出了一个未开发的互补证明原则，该原则可以建立超陷阱（即超安全性判断）作为证明的统一组成构件，我们使用它来为先前logics中无法实现的证明构图形式开发出逻辑的逻辑（LHC）。我们证明了LHC的声音，并将其应用于许多具有挑战性的例子。
Hypersafety properties of arity $n$ are program properties that relate $n$ traces of a program (or, more generally, traces of $n$ programs). Classic examples include determinism, idempotence, and associativity. A number of relational program logics have been introduced to target this class of properties. Their aim is to construct simpler proofs by capitalizing on structural similarities between the $n$ related programs. We propose an unexplored, complementary proof principle that establishes hyper-triples (i.e. hypersafety judgments) as a unifying compositional building block for proofs, and we use it to develop a Logic for Hyper-triple Composition (LHC), which supports forms of proof compositionality that were not achievable in previous logics. We prove LHC sound and apply it to a number of challenging examples.
