Relational program verification is a variant of program verification where one can reason about two programs and as a special case about two executions of a single program on different inputs. Relational program verification can be used for reasoning about a broad range of properties, including equivalence and refinement, and specialized notions such as continuity, information flow security or relative cost. In a higher-order setting, relational program verification can be achieved using relational refinement type systems, a form of refinement types where assertions have a relational interpretation. Relational refinement type systems excel at relating structurally equivalent terms but provide limited support for relating terms with very different structures.
We present a logic, called Relational Higher Order Logic (RHOL), for proving relational properties of a simply typed $λ$-calculus with inductive types and recursive definitions. RHOL retains the type-directed flavour of relational refinement type systems but achieves greater expressivity through rules which simultaneously reason about the two terms as well as rules which only contemplate one of the two terms. We show that RHOL has strong foundations, by proving an equivalence with higher-order logic (HOL), and leverage this equivalence to derive key meta-theoretical properties: subject reduction, admissibility of a transitivity rule and set-theoretical soundness. Moreover, we define sound embeddings for several existing relational type systems such as relational refinement types and type systems for dependency analysis and relative cost, and we verify examples that were out of reach of prior work.
Relational Hoare logics (RHL) provide rules for reasoning about relations between programs. Several RHLs include a rule we call sequential product that infers a relational correctness judgment from judgments of ordinary Hoare logic (HL). Other rules embody sensible patterns of reasoning and have been found useful in practice, but sequential product is relatively complete on its own (with HL). As a more satisfactory way to evaluate RHLs, a notion of alignment completeness is introduced, in terms of the inductive assertion method and product automata. Alignment completeness results are given to …
Relational Hoare logics extend the applicability of modular, deductive verification to encompass important 2-run properties including dependency requirements such as confidentiality and program relations such as equivalence or similarity between program versions. A considerable number of recent works introduce different relational Hoare logics without yet converging on a core set of proof rules. This paper looks backwards to little known early work. This brings to light some principles that clarify and organize the rules as well as suggesting a new rule and a new notion of completeness.
Hoare-style program logics are a popular and effective technique for software verification. Relational program logics are an instance of this approach that enables reasoning about relationships between the execution of two or more programs. Existing relational program logics have focused on verifying that all runs of a collection of programs do not violate a specified relational behavior. Several important relational properties, including refinement and noninterference, do not fit into this category, as they also mandate the existence of specific desirable executions. This paper presents RHLE,…
TU Dortmund University（多特蒙德工业大学）；University of Bonn（波恩大学）
我们提出了关系线性规划，一个简单的框架结合线性程序（LP）和逻辑程序。关系线性规划（relational linear program，RLP）是一个声明性的LP模板，通过对象、关系和量化变量的逻辑概念定义目标和约束。这使得人们可以表达LP目标和约束关系的不同数量的个人和他们之间的关系，而不列举他们。连同逻辑知识库，有效地由逻辑事实和规则组成的逻辑程序，它归纳出一个基础LP。使用提升线性规划来求解该基础LP。也就是说，如果可能的话，采用地面LP内的对称性来降低其维数，并且使用任何现成的LP求解器来求解简化的程序。与主流LP模板语言（如AMPL）相比，它具有声明式和命令式编程风格的混合，RLP的关系性质允许在关系域上更直观地表示优化问题。我们说明了这一经验的实验近似推理在马尔可夫逻辑网络使用LP松弛，解决马尔可夫决策过程中，集体推理使用LP支持向量机。
Complete Relational Logic for Infinite-Dimensional Quantum Programs with Unbounded Assertions
Max-Planck Institute for Security and Privacy (MPI-SP)（马克斯·普朗克安全与隐私研究所）；IMDEA Software Institute（IMDEA软件研究所）；Key Laboratory of System Software (Chinese Academy of Sciences)（中国科学院系统软件重点实验室）；Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所）；University of Chinese Academy of Sciences（中国科学院大学）；Eidgenössische Technische Hochschule (ETH) Zürich（苏黎世联邦理工学院）；Ludwig-Maximilians-Universität München（慕尼黑大学）；Munich Center for Quantum Science and Technology (MCQST)（慕尼黑量子科学与工程中心）
Dedicated to Tony Hoare. In a paper published in 1972 Hoare articulated the fundamental notions of hiding invariants and simulations. Hiding: invariants on encapsulated data representations need not be mentioned in specifications that comprise the API of a module. Simulation: correctness of a new data representation and implementation can be established by proving simulation between the old and new implementations using a coupling relation defined on the encapsulated state. These results were formalized semantically and for a simple model of state, though the paper claimed this could be extend…
Program synthesis approaches struggle to learn programs with numerical values. An especially difficult problem is learning continuous values over multiple examples, such as intervals. To overcome this limitation, we introduce an inductive logic programming approach which combines relational learning with numerical reasoning. Our approach, which we call NUMSYNTH, uses satisfiability modulo theories solvers to efficiently learn programs with numerical values. Our approach can identify numerical values in linear arithmetic fragments, such as real difference logic, and from infinite domains, such …
Verifying relations between programs arises as a task in various verification contexts such as optimizing transformations, relating new versions of programs with older versions (regression verification), and noninterference. However, relational verification for programs acting on dynamically allocated mutable state is not well supported by existing tools, which provide a high level of automation at the cost of restricting the programs considered. Auto-active tools, on the other hand, require more user interaction but enable verification of a broader class of programs. This article presents Why…
Probabilistic logic programming is a major part of statistical relational artificial intelligence, where approaches from logic and probability are brought together to reason about and learn from relational domains in a setting of uncertainty. However, the behaviour of statistical relational representations across variable domain sizes is complex, and scaling inference and learning to large domains remains a significant challenge. In recent years, connections have emerged between domain size dependence, lifted inference and learning from sampled subpopulations. The asymptotic behaviour of stati…
