检索结果-内蒙古大学图书馆

30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) Held as Part of the 27th European Joint Conferences on Theory and Practice of Software (ETAPS)

作者： Beutner, Raven CISPA Helmholtz Ctr Informat Secur Saarbrucken Germany

ISBN: (纸本)9783031572487;9783031572494

Hyperproperties relate multiple executions of a program and are commonly used to specify security and information-flow policies. Most existing work has focused on the verification of k-safety properties, i.e., properties that state that all k-tuples of execution traces satisfy a given property. In this paper, we study the automated verification of richer properties that combine universal and existential quantification over executions. Concretely, we consider for all(k)there exists(l) properties, which state that for all k executions, there exist l executions that, together, satisfy a property. This captures important non-k-safety requirements, including hyperliveness properties such as generalized non-interference, opacity, refinement, and robustness. We design an automated constraint-based algorithm for the verification of for all(k)there exists(l) properties. Our algorithm leverages a sound-and-complete program logic and a (parameterized) strongest postcondition computation. We implement our algorithm in a tool called ForEx and report on encouraging experimental results.

关键词： Hyperproperties program logic Hoare logic Symbolic Execution Constraint-based Verification Predicate Transformer Refinement Strongest Postcondition Underapproximation.

来源：评论

学校读者我要写书评

暂无评论

Verifying Contextual Refinement with Ownership Transfer

引用

Journal of Computer Science & Technology 2021年第6期36卷 1342-1366页

作者： Zhao-Hui Li Xin-Yu Feng School of Computer Science and Technology University of Science and Technology of ChinaHefei 230026China Department of Computer Science and Technology Nanjing UniversityNanjing 210023China State Key Laboratory for Novel Software Technology Nanjing UniversityNanjing 210023China

Contextual refinement is a compositional approach to compositional verification of concurrent *** has been much work designing program logics to prove the contextual refinement between the object implementation and its abstract ***,these program logics for contextual refinement verification cannot support objects with resource ownership transfer,which is a common pattern in many concurrent objects,such as the memory management module in OS kernels,which transfers the allocated memory block between the object and *** this paper,we propose a new approach to give abstract and implementation independent specifications to concurrent objects with ownership *** also design a program logic to verify contextual refinement of concurrent objects *** abstract *** have successfully applied our logic to verifying an implementation of the memory management module,where the implementation is an appropriately simplified version of the original version from a real-world preemptive OS kernel.

关键词： contextual refinement program logic concurrent object ownership transfer verification

来源：评论

学校读者我要写书评

暂无评论

The next 700 relational program logics

The next 700 relational program logics

引用

Proceedings of the ACM on programming Languages

作者： Maillard, Kenji Hrit, Ctlin Rivas, Exequiel Van Muylder, Antoine Inria Paris ENS Paris France Université de Paris Paris France

We propose the first framework for defining relational program logics for arbitrary monadic effects. The framework is embedded within a relational dependent type theory and is highly expressive. At the semantic level, we provide an algebraic presentation of relational specifications as a class of relative monads, and link computations and specifications by introducing relational effect observations, which map pairs of monadic computations to relational specifications in a way that respects the algebraic structure. For an arbitrary relational effect observation, we generically define the core of a sound relational program logic, and explain how to complete it to a full-fledged logic for the monadic effect at hand. We show that this generic framework can be used to define relational program logics for effects as diverse as state, input-output, nondeterminism, and discrete probabilities. We, moreover, show that by instantiating our framework with state and unbounded iteration we can embed a variant of Benton's Relational Hoare logic, and also sketch how to reconstruct Relational Hoare Type Theory. Finally, we identify and overcome conceptual challenges that prevented previous relational program logics from properly dealing with control effects, and are the first to provide a relational program logic for exceptions. © 2020 Association for Computing Machinery. All rights reserved.

关键词： Computer circuits Algebra Formal languages Foundations Probability Semantics Specifications Dependent types Exceptions Monads Non determinism program logic program Verification Relative monads Side effect State

来源：评论

学校读者我要写书评

暂无评论

Control-data separation and logical condition propagation for efficient inference on probabilistic programs

引用

JOURNAL OF logicAL AND ALGEBRAIC METHODS IN programMING 2024年 136卷

作者： Hasuo, Ichiro Oyabu, Yuichiro Eberhart, Clovis Suenaga, Kohei Cho, Kenta Katsumata, Shin-ya Natl Inst Informat Hitotsubashi 2-1-2Chiyoda Tokyo 1018430 Japan SOKENDAI Grad Univ Adv Studies Dept Informat Hayama Kanagawa 2400193 Japan Ernst & Young ShinNihon LLC Yurakucho 1-1-2Chiyoda Tokyo 1000006 Japan Kyoto Univ Grad Sch Informat Yoshida Honmachi 36-1 Kyoto Kyoto 6068501 Japan

We present a novel sampling framework for probabilistic programs. The framework combines two recent ideas-control-data separation and logical condition propagation-in a nontrivial manner so that the two ideas boost the benefits of each other. We implemented our algorithm on top of Anglican. The experimental results demonstrate our algorithm's efficiency, especially for programs with while loops and rare observations. (c) 2023 Elsevier Inc. All rights reserved.

关键词： Probabilistic programming Bayesian inference Sampling Static analysis program logic

来源：评论

学校读者我要写书评

暂无评论

Sound and relatively complete belief Hoare logic for statistical hypothesis testing programs

引用

ARTIFICIAL INTELLIGENCE 2024年 326卷

作者： Kawamoto, Yusuke Sato, Tetsuya Suenaga, Kohei AIST Tokyo Japan JST PRESTO Kawaguchi Japan Tokyo Inst Technol Tokyo Japan Kyoto Univ Kyoto Japan

We propose a new approach to formally describing the requirement for statistical inference and checking whether a program uses the statistical method appropriately. Specifically, we define belief Hoare logic (BHL) for formalizing and reasoning about the statistical beliefs acquired via hypothesis testing. This program logic is sound and relatively complete with respect to a Kripke model for hypothesis tests. We demonstrate by examples that BHL is useful for reasoning about practical issues in hypothesis testing. In our framework, we clarify the importance of prior beliefs in acquiring statistical beliefs through hypothesis testing, and discuss the whole picture of the justification of statistical inference inside and outside the program logic.

关键词： Knowledge representation Epistemic logic program logic Kripke model Statistical hypothesis testing

来源：评论

学校读者我要写书评

暂无评论

program logics Based on Algebras with the Composition of Predicate Complement 9

Program Logics Based on Algebras with the Composition of Pre...

引用

9th International Conference on Advanced Computer Information Technologies (ACIT)

作者： Nikitchenko, Mykola Shkilniak, Oksana Shkilniak, Stepan Taras Shevchenko Natl Univ Kyiv Dept Theory & Technol Programming Kiev Ukraine Taras Shevchenko Natl Univ Kyiv Dept Informat Syst Kiev Ukraine

ISBN: (纸本)9781728104492

The formalism of program logics is the main instrument for software verification. Many such logics reflecting different properties of software systems were proposed. Floyd-Hoare logic and its variants are popular for program verification. But this logic is oriented on total pre- and post-conditions (predicates) and becomes unsound in the case of partial predicates. In our previous works we considered different methods to extend Floyd-Hoare logic for partial predicates. One of the methods involves program algebras with the composition of predicate complement. Introduction of this composition permits to modify rules of the logic making them sound, but the obtained logic becomes more complicated because it involves undefinedness conditions. In this paper we continue our research of such logics. We introduce special consequence relation and prove the soundness and completeness theorems for the case of logic of propositional level with the composition of predicate complement.

关键词： software verification program logic Floyd-Hoare logic partial predicate soundness and completeness theorems

来源：评论

学校读者我要写书评

暂无评论

Efficient and Provable Local Capability Revocation using Uninitialized Capabilities

引用

PROCEEDINGS OF THE ACM ON programMING LANGUAGES-PACMPL 2021年第POPL期5卷 1–30页

作者： Georges, Aina Linn Gueneau, Armael Van Strydonck, Thomas Timany, Amin Trieu, Alix Huyghebaert, Sander Devriese, Dominique Birkedal, Lars Aarhus Univ Aarhus Denmark Katholieke Univ Leuven Leuven Belgium Vrije Univ Brussel Brussels Belgium

Capability machines are a special form of CPUs that offer fine-grained privilege separation using a form of authority-carrying values known as capabilities. The CHERI capability machine offers local capabilities, which could be used as a cheap but restricted form of capability revocation. Unfortunately, local capability revocation is unrealistic in practice because large amounts of stack memory need to be cleared as a security precaution. In this paper, we address this shortcoming by introducing uninitialized capabilities: a new form of capabilities that represent read/write authority to a block of memory without exposing the memory's initial contents. We provide a mechanically verified program logic for reasoning about programs on a capability machine with the new feature and we formalize and prove capability safety in the form of a universal contract for untrusted code. We use uninitialized capabilities for making a previously-proposed secure calling convention efficient and prove its security using the program logic. Finally, we report on a proof-of-concept implementation of uninitialized capabilities on the CHERI capability machine.

关键词： capability machines local capabilities uninitialized capabilities capability safety universal contracts program logic capability revocation CHERI

来源：评论

学校读者我要写书评

暂无评论

Abstraction for Conflict-Free Replicated Data Types 2021

Abstraction for Conflict-Free Replicated Data Types

引用

42nd ACM SIGPLAN International Conference on programming Language Design and Implementation (PLDI)

作者： Liang, Hongjin Feng, Xinyu Nanjing Univ State Key Lab Novel Software Technol Nanjing Jiangsu Peoples R China

ISBN: (纸本)9781450383912

Strong eventual consistency (SEC) has been used as a classic notion of correctness for Conflict-Free Replicated Data Types (CRDTs). However, it does not give proper abstractions of functionality, thus is not helpful for modular verification of client programs using CRDTs. We propose a new correctness formulation for CRDTs, called Abstract Converging Consistency (ACC), to specify both data consistency and functional correctness. ACC gives abstract atomic specifications (as an abstraction) to CRDT operations, and establishes consistency between the concrete execution traces and the execution using the abstract atomic operations. The abstraction allows us to verify the CRDT implementation and its client programs separately, resulting in more modular and elegant proofs than monolithic approaches for whole program verification. We give a generic proof method to verify ACC of CRDT implementations, and a rely-guarantee style program logic to verify client programs. Our Abstraction theorem shows that ACC is equivalent to contextual refinement, linking the verification of CRDT implementations and clients together to derive functional correctness of whole programs.

关键词： Replicated Data Types Eventual Consistency Contextual Refinement program logic Modular Verification

来源：评论

学校读者我要写书评

暂无评论

TLC: Temporal logic of Distributed Components

引用

PROCEEDINGS OF THE ACM ON programMING LANGUAGES-PACMPL 2020年第ICFP期4卷 1–30页

作者： Griffin, Jeremiah Lesani, Mohsen Shadab, Narges Yin, Xizhe Univ Calif Riverside Riverside CA 92521 USA

Distributed systems are critical to reliable and scalable computing;however, they are complicated in nature and prone to bugs. To manage this complexity, network middleware has been traditionally built in layered stacks of components. We present a novel approach to compositional verification of distributed stacks to verify each component based on only the specification of lower components. We present TLC (Temporal logic of Components), a novel temporal program logic that offers intuitive inference rules for verification of both safety and liveness properties of functional implementations of distributed components. To support compositional reasoning, we define a novel transformation on the assertion language that lowers the specification of a component to be used as a subcomponent. We prove the soundness of TLC and the lowering transformation with respect to a novel operational semantics for stacks of composed components in partially synchronous networks. We successfully apply TLC to compose and verify a stack of fundamental distributed components.

关键词： Distributed Protocols Temporal logic program logic Composition Operational Semantics

来源：评论

学校读者我要写书评

暂无评论

Intentional Practice as a Method to Reduce the Implementation Gap Between Science and Practice in the Delivery of Trauma-Informed Residential Care

引用

RESIDENTIAL TREATMENT FOR CHILDREN & YOUTH 2020年第1期37卷 20-45页

作者： Raymond, Ivan Life Buoyancy Inst POB 3 Adelaide SA 5154 Australia

Children and young people with backgrounds of trauma, and supported in residential programs (group care, residential treatment, wilderness therapy, and outdoor behavioral healthcare), require interventions underpinned by trauma-informed science. While there is much optimism that trauma-informed services are being integrated into residential care settings, there is evidence of a science to practice gap in how these components are implemented across real-world settings. The purpose of the paper is to introduce 'intentional practice' and growth-focused logic modeling (Life Buoyancy Model;LBM) as a possible method to strengthen the delivery of trauma-informed services at the program level. The paper provides an overview of the modeling and describes how the approach seeks to reduce the science to practice gap in the implementation of trauma-informed service delivery. To aid this process, five core intervention components are proposed to provide a more nuanced understanding of how trauma-informed practice can be implemented. Key considerations are offered for residential care program leaders and program developers to design, refine or review the delivery of locally contextualized program models.

关键词： Intentional practice trauma-informed practice implementation science program logic therapeutic residential care

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：